YES
The TRS could be proven terminating. The proof took 24001 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (677ms).
| – Problem 2 was processed with processor SubtermCriterion (2ms).
| | – Problem 8 was processed with processor SubtermCriterion (0ms).
| – Problem 3 was processed with processor SubtermCriterion (2ms).
| | – Problem 9 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor SubtermCriterion (13ms).
| | – Problem 10 was processed with processor SubtermCriterion (2ms).
| | | – Problem 12 was processed with processor PolynomialLinearRange4 (41ms).
| | | | – Problem 14 was processed with processor PolynomialLinearRange4 (25ms).
| – Problem 5 was processed with processor SubtermCriterion (2ms).
| | – Problem 11 was processed with processor SubtermCriterion (0ms).
| – Problem 6 was processed with processor SubtermCriterion (2ms).
| – Problem 7 was processed with processor PolynomialLinearRange4 (375ms).
| | – Problem 13 was processed with processor PolynomialLinearRange4 (529ms).
| | | – Problem 15 was processed with processor PolynomialLinearRange4 (333ms).
| | | | – Problem 16 was processed with processor PolynomialLinearRange4 (284ms).
| | | | | – Problem 17 was processed with processor PolynomialLinearRange4 (240ms).
| | | | | | – Problem 18 was processed with processor PolynomialLinearRange4 (258ms).
| | | | | | | – Problem 19 was processed with processor PolynomialLinearRange4 (221ms).
| | | | | | | | – Problem 20 was processed with processor PolynomialLinearRange4 (220ms).
| | | | | | | | | – Problem 21 was processed with processor PolynomialLinearRange4 (202ms).
| | | | | | | | | | – Problem 22 was processed with processor PolynomialLinearRange4 (30ms).
| | | | | | | | | | | – Problem 23 was processed with processor ReductionPairSAT (106ms).
| | | | | | | | | | | | – Problem 24 was processed with processor DependencyGraph (0ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| geq#(active(X1), X2) | → | geq#(X1, X2) | | mark#(geq(X1, X2)) | → | active#(geq(X1, X2)) |
| active#(geq(s(X), s(Y))) | → | mark#(geq(X, Y)) | | minus#(X1, mark(X2)) | → | minus#(X1, X2) |
| if#(X1, X2, active(X3)) | → | if#(X1, X2, X3) | | active#(geq(X, 0)) | → | mark#(true) |
| mark#(s(X)) | → | s#(mark(X)) | | active#(if(true, X, Y)) | → | mark#(X) |
| geq#(X1, mark(X2)) | → | geq#(X1, X2) | | active#(geq(0, s(Y))) | → | mark#(false) |
| minus#(X1, active(X2)) | → | minus#(X1, X2) | | active#(div(0, s(Y))) | → | mark#(0) |
| geq#(mark(X1), X2) | → | geq#(X1, X2) | | active#(div(s(X), s(Y))) | → | geq#(X, Y) |
| active#(div(s(X), s(Y))) | → | div#(minus(X, Y), s(Y)) | | mark#(s(X)) | → | mark#(X) |
| mark#(minus(X1, X2)) | → | active#(minus(X1, X2)) | | active#(minus(s(X), s(Y))) | → | mark#(minus(X, Y)) |
| active#(minus(0, Y)) | → | mark#(0) | | mark#(div(X1, X2)) | → | mark#(X1) |
| active#(div(s(X), s(Y))) | → | s#(div(minus(X, Y), s(Y))) | | mark#(true) | → | active#(true) |
| div#(X1, active(X2)) | → | div#(X1, X2) | | active#(div(s(X), s(Y))) | → | s#(Y) |
| active#(geq(s(X), s(Y))) | → | geq#(X, Y) | | active#(minus(s(X), s(Y))) | → | minus#(X, Y) |
| active#(div(s(X), s(Y))) | → | if#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0) | | if#(X1, mark(X2), X3) | → | if#(X1, X2, X3) |
| if#(X1, X2, mark(X3)) | → | if#(X1, X2, X3) | | div#(mark(X1), X2) | → | div#(X1, X2) |
| if#(mark(X1), X2, X3) | → | if#(X1, X2, X3) | | mark#(if(X1, X2, X3)) | → | mark#(X1) |
| div#(active(X1), X2) | → | div#(X1, X2) | | minus#(active(X1), X2) | → | minus#(X1, X2) |
| mark#(false) | → | active#(false) | | mark#(if(X1, X2, X3)) | → | active#(if(mark(X1), X2, X3)) |
| mark#(minus(X1, X2)) | → | minus#(X1, X2) | | active#(if(false, X, Y)) | → | mark#(Y) |
| mark#(div(X1, X2)) | → | div#(mark(X1), X2) | | mark#(geq(X1, X2)) | → | geq#(X1, X2) |
| if#(X1, active(X2), X3) | → | if#(X1, X2, X3) | | active#(div(s(X), s(Y))) | → | minus#(X, Y) |
| minus#(mark(X1), X2) | → | minus#(X1, X2) | | div#(X1, mark(X2)) | → | div#(X1, X2) |
| mark#(if(X1, X2, X3)) | → | if#(mark(X1), X2, X3) | | mark#(0) | → | active#(0) |
| mark#(s(X)) | → | active#(s(mark(X))) | | active#(div(s(X), s(Y))) | → | mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) |
| geq#(X1, active(X2)) | → | geq#(X1, X2) | | mark#(div(X1, X2)) | → | active#(div(mark(X1), X2)) |
| if#(active(X1), X2, X3) | → | if#(X1, X2, X3) | | s#(mark(X)) | → | s#(X) |
| s#(active(X)) | → | s#(X) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, 0, minus, s, if, div, active, true, false, mark
Strategy
The following SCCs where found
| minus#(mark(X1), X2) → minus#(X1, X2) | minus#(X1, active(X2)) → minus#(X1, X2) |
| minus#(X1, mark(X2)) → minus#(X1, X2) | minus#(active(X1), X2) → minus#(X1, X2) |
| if#(X1, mark(X2), X3) → if#(X1, X2, X3) | if#(X1, X2, mark(X3)) → if#(X1, X2, X3) |
| if#(mark(X1), X2, X3) → if#(X1, X2, X3) | if#(X1, active(X2), X3) → if#(X1, X2, X3) |
| if#(X1, X2, active(X3)) → if#(X1, X2, X3) | if#(active(X1), X2, X3) → if#(X1, X2, X3) |
| s#(mark(X)) → s#(X) | s#(active(X)) → s#(X) |
| div#(X1, mark(X2)) → div#(X1, X2) | div#(X1, active(X2)) → div#(X1, X2) |
| div#(mark(X1), X2) → div#(X1, X2) | div#(active(X1), X2) → div#(X1, X2) |
| geq#(mark(X1), X2) → geq#(X1, X2) | geq#(active(X1), X2) → geq#(X1, X2) |
| geq#(X1, active(X2)) → geq#(X1, X2) | geq#(X1, mark(X2)) → geq#(X1, X2) |
| mark#(if(X1, X2, X3)) → active#(if(mark(X1), X2, X3)) | mark#(s(X)) → active#(s(mark(X))) |
| active#(div(s(X), s(Y))) → mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | active#(if(false, X, Y)) → mark#(Y) |
| mark#(geq(X1, X2)) → active#(geq(X1, X2)) | active#(geq(s(X), s(Y))) → mark#(geq(X, Y)) |
| mark#(div(X1, X2)) → active#(div(mark(X1), X2)) | active#(if(true, X, Y)) → mark#(X) |
| mark#(if(X1, X2, X3)) → mark#(X1) | mark#(s(X)) → mark#(X) |
| mark#(minus(X1, X2)) → active#(minus(X1, X2)) | active#(minus(s(X), s(Y))) → mark#(minus(X, Y)) |
| mark#(div(X1, X2)) → mark#(X1) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| geq#(mark(X1), X2) | → | geq#(X1, X2) | | geq#(active(X1), X2) | → | geq#(X1, X2) |
| geq#(X1, active(X2)) | → | geq#(X1, X2) | | geq#(X1, mark(X2)) | → | geq#(X1, X2) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, 0, minus, s, if, div, active, true, false, mark
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| geq#(active(X1), X2) | → | geq#(X1, X2) | | geq#(mark(X1), X2) | → | geq#(X1, X2) |
Problem 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| geq#(X1, active(X2)) | → | geq#(X1, X2) | | geq#(X1, mark(X2)) | → | geq#(X1, X2) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, minus, 0, s, if, div, false, true, active, mark
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| geq#(X1, active(X2)) | → | geq#(X1, X2) | | geq#(X1, mark(X2)) | → | geq#(X1, X2) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| div#(X1, mark(X2)) | → | div#(X1, X2) | | div#(X1, active(X2)) | → | div#(X1, X2) |
| div#(mark(X1), X2) | → | div#(X1, X2) | | div#(active(X1), X2) | → | div#(X1, X2) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, 0, minus, s, if, div, active, true, false, mark
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| div#(mark(X1), X2) | → | div#(X1, X2) | | div#(active(X1), X2) | → | div#(X1, X2) |
Problem 9: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| div#(X1, mark(X2)) | → | div#(X1, X2) | | div#(X1, active(X2)) | → | div#(X1, X2) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, minus, 0, s, if, div, false, true, active, mark
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| div#(X1, mark(X2)) | → | div#(X1, X2) | | div#(X1, active(X2)) | → | div#(X1, X2) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| if#(X1, mark(X2), X3) | → | if#(X1, X2, X3) | | if#(X1, X2, mark(X3)) | → | if#(X1, X2, X3) |
| if#(mark(X1), X2, X3) | → | if#(X1, X2, X3) | | if#(X1, active(X2), X3) | → | if#(X1, X2, X3) |
| if#(X1, X2, active(X3)) | → | if#(X1, X2, X3) | | if#(active(X1), X2, X3) | → | if#(X1, X2, X3) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, 0, minus, s, if, div, active, true, false, mark
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| if#(mark(X1), X2, X3) | → | if#(X1, X2, X3) | | if#(active(X1), X2, X3) | → | if#(X1, X2, X3) |
Problem 10: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| if#(X1, mark(X2), X3) | → | if#(X1, X2, X3) | | if#(X1, X2, mark(X3)) | → | if#(X1, X2, X3) |
| if#(X1, active(X2), X3) | → | if#(X1, X2, X3) | | if#(X1, X2, active(X3)) | → | if#(X1, X2, X3) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, minus, 0, s, if, div, false, true, active, mark
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| if#(X1, mark(X2), X3) | → | if#(X1, X2, X3) | | if#(X1, active(X2), X3) | → | if#(X1, X2, X3) |
Problem 12: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| if#(X1, X2, mark(X3)) | → | if#(X1, X2, X3) | | if#(X1, X2, active(X3)) | → | if#(X1, X2, X3) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, 0, minus, s, if, div, active, true, false, mark
Strategy
Polynomial Interpretation
- 0: 0
- active(x): 2x + 1
- div(x,y): 0
- false: 0
- geq(x,y): 0
- if(x,y,z): 0
- if#(x,y,z): 2z + x
- mark(x): x
- minus(x,y): 0
- s(x): 0
- true: 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| if#(X1, X2, active(X3)) | → | if#(X1, X2, X3) |
Problem 14: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| if#(X1, X2, mark(X3)) | → | if#(X1, X2, X3) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, minus, 0, s, if, div, false, true, active, mark
Strategy
Polynomial Interpretation
- 0: 0
- active(x): 0
- div(x,y): 0
- false: 0
- geq(x,y): 0
- if(x,y,z): 0
- if#(x,y,z): 2z + y + x + 1
- mark(x): 2x + 1
- minus(x,y): 0
- s(x): 0
- true: 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| if#(X1, X2, mark(X3)) | → | if#(X1, X2, X3) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| minus#(mark(X1), X2) | → | minus#(X1, X2) | | minus#(X1, active(X2)) | → | minus#(X1, X2) |
| minus#(X1, mark(X2)) | → | minus#(X1, X2) | | minus#(active(X1), X2) | → | minus#(X1, X2) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, 0, minus, s, if, div, active, true, false, mark
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| minus#(mark(X1), X2) | → | minus#(X1, X2) | | minus#(active(X1), X2) | → | minus#(X1, X2) |
Problem 11: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| minus#(X1, active(X2)) | → | minus#(X1, X2) | | minus#(X1, mark(X2)) | → | minus#(X1, X2) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, minus, 0, s, if, div, false, true, active, mark
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| minus#(X1, active(X2)) | → | minus#(X1, X2) | | minus#(X1, mark(X2)) | → | minus#(X1, X2) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| s#(mark(X)) | → | s#(X) | | s#(active(X)) | → | s#(X) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, 0, minus, s, if, div, active, true, false, mark
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| s#(mark(X)) | → | s#(X) | | s#(active(X)) | → | s#(X) |
Problem 7: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(s(X)) | → | active#(s(mark(X))) | | mark#(if(X1, X2, X3)) | → | active#(if(mark(X1), X2, X3)) |
| active#(if(false, X, Y)) | → | mark#(Y) | | active#(div(s(X), s(Y))) | → | mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) |
| mark#(geq(X1, X2)) | → | active#(geq(X1, X2)) | | active#(geq(s(X), s(Y))) | → | mark#(geq(X, Y)) |
| mark#(div(X1, X2)) | → | active#(div(mark(X1), X2)) | | active#(if(true, X, Y)) | → | mark#(X) |
| mark#(if(X1, X2, X3)) | → | mark#(X1) | | mark#(s(X)) | → | mark#(X) |
| mark#(minus(X1, X2)) | → | active#(minus(X1, X2)) | | active#(minus(s(X), s(Y))) | → | mark#(minus(X, Y)) |
| mark#(div(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, 0, minus, s, if, div, active, true, false, mark
Strategy
Polynomial Interpretation
- 0: 0
- active(x): 0
- active#(x): x
- div(x,y): 2
- false: 0
- geq(x,y): 2
- if(x,y,z): 2
- mark(x): 0
- mark#(x): 2
- minus(x,y): 2
- s(x): 0
- true: 0
Standard Usable rules
| mark(minus(X1, X2)) | → | active(minus(X1, X2)) | | minus(X1, active(X2)) | → | minus(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| mark(s(X)) | → | active(s(mark(X))) | | div(X1, mark(X2)) | → | div(X1, X2) |
| active(div(0, s(Y))) | → | mark(0) | | mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) |
| minus(mark(X1), X2) | → | minus(X1, X2) | | active(minus(0, Y)) | → | mark(0) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | minus(X1, mark(X2)) | → | minus(X1, X2) |
| geq(mark(X1), X2) | → | geq(X1, X2) | | mark(true) | → | active(true) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | div(X1, active(X2)) | → | div(X1, X2) |
| if(X1, X2, mark(X3)) | → | if(X1, X2, X3) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| mark(0) | → | active(0) | | s(active(X)) | → | s(X) |
| active(geq(X, 0)) | → | mark(true) | | minus(active(X1), X2) | → | minus(X1, X2) |
| if(X1, active(X2), X3) | → | if(X1, X2, X3) | | div(mark(X1), X2) | → | div(X1, X2) |
| if(mark(X1), X2, X3) | → | if(X1, X2, X3) | | active(geq(0, s(Y))) | → | mark(false) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| mark(div(X1, X2)) | → | active(div(mark(X1), X2)) | | active(if(false, X, Y)) | → | mark(Y) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | if(X1, mark(X2), X3) | → | if(X1, X2, X3) |
| mark(false) | → | active(false) | | s(mark(X)) | → | s(X) |
| active(if(true, X, Y)) | → | mark(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(s(X)) | → | active#(s(mark(X))) |
Problem 13: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(if(X1, X2, X3)) | → | active#(if(mark(X1), X2, X3)) | | active#(div(s(X), s(Y))) | → | mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) |
| active#(if(false, X, Y)) | → | mark#(Y) | | mark#(geq(X1, X2)) | → | active#(geq(X1, X2)) |
| active#(geq(s(X), s(Y))) | → | mark#(geq(X, Y)) | | mark#(if(X1, X2, X3)) | → | mark#(X1) |
| mark#(s(X)) | → | mark#(X) | | mark#(minus(X1, X2)) | → | active#(minus(X1, X2)) |
| mark#(div(X1, X2)) | → | active#(div(mark(X1), X2)) | | active#(minus(s(X), s(Y))) | → | mark#(minus(X, Y)) |
| mark#(div(X1, X2)) | → | mark#(X1) | | active#(if(true, X, Y)) | → | mark#(X) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, minus, 0, s, if, div, false, true, active, mark
Strategy
Polynomial Interpretation
- 0: 0
- active(x): x
- active#(x): 2x
- div(x,y): 2x + 1
- false: 0
- geq(x,y): 0
- if(x,y,z): 2z + y + 2x
- mark(x): x
- mark#(x): 2x
- minus(x,y): 0
- s(x): x
- true: 0
Standard Usable rules
| mark(minus(X1, X2)) | → | active(minus(X1, X2)) | | minus(X1, active(X2)) | → | minus(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| mark(s(X)) | → | active(s(mark(X))) | | div(X1, mark(X2)) | → | div(X1, X2) |
| active(div(0, s(Y))) | → | mark(0) | | mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) |
| minus(mark(X1), X2) | → | minus(X1, X2) | | active(minus(0, Y)) | → | mark(0) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | minus(X1, mark(X2)) | → | minus(X1, X2) |
| geq(mark(X1), X2) | → | geq(X1, X2) | | mark(true) | → | active(true) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | div(X1, active(X2)) | → | div(X1, X2) |
| if(X1, X2, mark(X3)) | → | if(X1, X2, X3) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| mark(0) | → | active(0) | | s(active(X)) | → | s(X) |
| active(geq(X, 0)) | → | mark(true) | | minus(active(X1), X2) | → | minus(X1, X2) |
| if(X1, active(X2), X3) | → | if(X1, X2, X3) | | div(mark(X1), X2) | → | div(X1, X2) |
| if(mark(X1), X2, X3) | → | if(X1, X2, X3) | | active(geq(0, s(Y))) | → | mark(false) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| mark(div(X1, X2)) | → | active(div(mark(X1), X2)) | | active(if(false, X, Y)) | → | mark(Y) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | if(X1, mark(X2), X3) | → | if(X1, X2, X3) |
| mark(false) | → | active(false) | | s(mark(X)) | → | s(X) |
| active(if(true, X, Y)) | → | mark(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(div(X1, X2)) | → | mark#(X1) |
Problem 15: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(if(X1, X2, X3)) | → | active#(if(mark(X1), X2, X3)) | | active#(if(false, X, Y)) | → | mark#(Y) |
| active#(div(s(X), s(Y))) | → | mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | mark#(geq(X1, X2)) | → | active#(geq(X1, X2)) |
| active#(geq(s(X), s(Y))) | → | mark#(geq(X, Y)) | | mark#(if(X1, X2, X3)) | → | mark#(X1) |
| mark#(s(X)) | → | mark#(X) | | mark#(div(X1, X2)) | → | active#(div(mark(X1), X2)) |
| mark#(minus(X1, X2)) | → | active#(minus(X1, X2)) | | active#(minus(s(X), s(Y))) | → | mark#(minus(X, Y)) |
| active#(if(true, X, Y)) | → | mark#(X) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, 0, minus, s, if, div, active, true, false, mark
Strategy
Polynomial Interpretation
- 0: 0
- active(x): x
- active#(x): x
- div(x,y): x
- false: 0
- geq(x,y): 0
- if(x,y,z): 2z + y + 2x
- mark(x): x
- mark#(x): x
- minus(x,y): x
- s(x): x + 2
- true: 0
Standard Usable rules
| mark(minus(X1, X2)) | → | active(minus(X1, X2)) | | minus(X1, active(X2)) | → | minus(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| mark(s(X)) | → | active(s(mark(X))) | | div(X1, mark(X2)) | → | div(X1, X2) |
| active(div(0, s(Y))) | → | mark(0) | | mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) |
| minus(mark(X1), X2) | → | minus(X1, X2) | | active(minus(0, Y)) | → | mark(0) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | minus(X1, mark(X2)) | → | minus(X1, X2) |
| geq(mark(X1), X2) | → | geq(X1, X2) | | mark(true) | → | active(true) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | div(X1, active(X2)) | → | div(X1, X2) |
| if(X1, X2, mark(X3)) | → | if(X1, X2, X3) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| mark(0) | → | active(0) | | s(active(X)) | → | s(X) |
| active(geq(X, 0)) | → | mark(true) | | minus(active(X1), X2) | → | minus(X1, X2) |
| if(X1, active(X2), X3) | → | if(X1, X2, X3) | | div(mark(X1), X2) | → | div(X1, X2) |
| if(mark(X1), X2, X3) | → | if(X1, X2, X3) | | active(geq(0, s(Y))) | → | mark(false) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| mark(div(X1, X2)) | → | active(div(mark(X1), X2)) | | active(if(false, X, Y)) | → | mark(Y) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | if(X1, mark(X2), X3) | → | if(X1, X2, X3) |
| mark(false) | → | active(false) | | s(mark(X)) | → | s(X) |
| active(if(true, X, Y)) | → | mark(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(s(X)) | → | mark#(X) | | active#(minus(s(X), s(Y))) | → | mark#(minus(X, Y)) |
Problem 16: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(if(X1, X2, X3)) | → | active#(if(mark(X1), X2, X3)) | | active#(div(s(X), s(Y))) | → | mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) |
| active#(if(false, X, Y)) | → | mark#(Y) | | mark#(geq(X1, X2)) | → | active#(geq(X1, X2)) |
| active#(geq(s(X), s(Y))) | → | mark#(geq(X, Y)) | | mark#(if(X1, X2, X3)) | → | mark#(X1) |
| mark#(minus(X1, X2)) | → | active#(minus(X1, X2)) | | mark#(div(X1, X2)) | → | active#(div(mark(X1), X2)) |
| active#(if(true, X, Y)) | → | mark#(X) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, minus, 0, s, if, div, false, true, active, mark
Strategy
Polynomial Interpretation
- 0: 2
- active(x): 3
- active#(x): 2x
- div(x,y): 1
- false: 3
- geq(x,y): 1
- if(x,y,z): 1
- mark(x): 3
- mark#(x): 2
- minus(x,y): 0
- s(x): 1
- true: 2
Standard Usable rules
| mark(minus(X1, X2)) | → | active(minus(X1, X2)) | | minus(X1, active(X2)) | → | minus(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| mark(s(X)) | → | active(s(mark(X))) | | div(X1, mark(X2)) | → | div(X1, X2) |
| active(div(0, s(Y))) | → | mark(0) | | mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) |
| minus(mark(X1), X2) | → | minus(X1, X2) | | active(minus(0, Y)) | → | mark(0) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | minus(X1, mark(X2)) | → | minus(X1, X2) |
| geq(mark(X1), X2) | → | geq(X1, X2) | | mark(true) | → | active(true) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | div(X1, active(X2)) | → | div(X1, X2) |
| if(X1, X2, mark(X3)) | → | if(X1, X2, X3) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| mark(0) | → | active(0) | | s(active(X)) | → | s(X) |
| active(geq(X, 0)) | → | mark(true) | | minus(active(X1), X2) | → | minus(X1, X2) |
| if(X1, active(X2), X3) | → | if(X1, X2, X3) | | div(mark(X1), X2) | → | div(X1, X2) |
| if(mark(X1), X2, X3) | → | if(X1, X2, X3) | | active(geq(0, s(Y))) | → | mark(false) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| mark(div(X1, X2)) | → | active(div(mark(X1), X2)) | | active(if(false, X, Y)) | → | mark(Y) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | if(X1, mark(X2), X3) | → | if(X1, X2, X3) |
| mark(false) | → | active(false) | | s(mark(X)) | → | s(X) |
| active(if(true, X, Y)) | → | mark(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(minus(X1, X2)) | → | active#(minus(X1, X2)) |
Problem 17: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(if(X1, X2, X3)) | → | active#(if(mark(X1), X2, X3)) | | active#(if(false, X, Y)) | → | mark#(Y) |
| active#(div(s(X), s(Y))) | → | mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | mark#(geq(X1, X2)) | → | active#(geq(X1, X2)) |
| active#(geq(s(X), s(Y))) | → | mark#(geq(X, Y)) | | mark#(if(X1, X2, X3)) | → | mark#(X1) |
| mark#(div(X1, X2)) | → | active#(div(mark(X1), X2)) | | active#(if(true, X, Y)) | → | mark#(X) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, 0, minus, s, if, div, active, true, false, mark
Strategy
Polynomial Interpretation
- 0: 0
- active(x): x
- active#(x): x
- div(x,y): 2
- false: 0
- geq(x,y): 2
- if(x,y,z): z + y + x
- mark(x): x
- mark#(x): x
- minus(x,y): 0
- s(x): 0
- true: 2
Standard Usable rules
| mark(minus(X1, X2)) | → | active(minus(X1, X2)) | | minus(X1, active(X2)) | → | minus(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| mark(s(X)) | → | active(s(mark(X))) | | div(X1, mark(X2)) | → | div(X1, X2) |
| active(div(0, s(Y))) | → | mark(0) | | mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) |
| minus(mark(X1), X2) | → | minus(X1, X2) | | active(minus(0, Y)) | → | mark(0) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | minus(X1, mark(X2)) | → | minus(X1, X2) |
| geq(mark(X1), X2) | → | geq(X1, X2) | | mark(true) | → | active(true) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | div(X1, active(X2)) | → | div(X1, X2) |
| if(X1, X2, mark(X3)) | → | if(X1, X2, X3) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| mark(0) | → | active(0) | | s(active(X)) | → | s(X) |
| active(geq(X, 0)) | → | mark(true) | | minus(active(X1), X2) | → | minus(X1, X2) |
| if(X1, active(X2), X3) | → | if(X1, X2, X3) | | div(mark(X1), X2) | → | div(X1, X2) |
| if(mark(X1), X2, X3) | → | if(X1, X2, X3) | | active(geq(0, s(Y))) | → | mark(false) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| mark(div(X1, X2)) | → | active(div(mark(X1), X2)) | | active(if(false, X, Y)) | → | mark(Y) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | if(X1, mark(X2), X3) | → | if(X1, X2, X3) |
| mark(false) | → | active(false) | | s(mark(X)) | → | s(X) |
| active(if(true, X, Y)) | → | mark(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| active#(if(true, X, Y)) | → | mark#(X) |
Problem 18: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(if(X1, X2, X3)) | → | active#(if(mark(X1), X2, X3)) | | active#(div(s(X), s(Y))) | → | mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) |
| active#(if(false, X, Y)) | → | mark#(Y) | | mark#(geq(X1, X2)) | → | active#(geq(X1, X2)) |
| active#(geq(s(X), s(Y))) | → | mark#(geq(X, Y)) | | mark#(if(X1, X2, X3)) | → | mark#(X1) |
| mark#(div(X1, X2)) | → | active#(div(mark(X1), X2)) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, minus, 0, s, if, div, false, true, active, mark
Strategy
Polynomial Interpretation
- 0: 0
- active(x): x
- active#(x): x
- div(x,y): 2
- false: 2
- geq(x,y): 2
- if(x,y,z): z + y + x
- mark(x): x
- mark#(x): x
- minus(x,y): 0
- s(x): 0
- true: 2
Standard Usable rules
| mark(minus(X1, X2)) | → | active(minus(X1, X2)) | | minus(X1, active(X2)) | → | minus(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| mark(s(X)) | → | active(s(mark(X))) | | div(X1, mark(X2)) | → | div(X1, X2) |
| active(div(0, s(Y))) | → | mark(0) | | mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) |
| minus(mark(X1), X2) | → | minus(X1, X2) | | active(minus(0, Y)) | → | mark(0) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | minus(X1, mark(X2)) | → | minus(X1, X2) |
| geq(mark(X1), X2) | → | geq(X1, X2) | | mark(true) | → | active(true) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | div(X1, active(X2)) | → | div(X1, X2) |
| if(X1, X2, mark(X3)) | → | if(X1, X2, X3) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| mark(0) | → | active(0) | | s(active(X)) | → | s(X) |
| active(geq(X, 0)) | → | mark(true) | | minus(active(X1), X2) | → | minus(X1, X2) |
| if(X1, active(X2), X3) | → | if(X1, X2, X3) | | div(mark(X1), X2) | → | div(X1, X2) |
| if(mark(X1), X2, X3) | → | if(X1, X2, X3) | | active(geq(0, s(Y))) | → | mark(false) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| mark(div(X1, X2)) | → | active(div(mark(X1), X2)) | | active(if(false, X, Y)) | → | mark(Y) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | if(X1, mark(X2), X3) | → | if(X1, X2, X3) |
| mark(false) | → | active(false) | | s(mark(X)) | → | s(X) |
| active(if(true, X, Y)) | → | mark(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| active#(if(false, X, Y)) | → | mark#(Y) |
Problem 19: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(if(X1, X2, X3)) | → | active#(if(mark(X1), X2, X3)) | | active#(div(s(X), s(Y))) | → | mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) |
| mark#(geq(X1, X2)) | → | active#(geq(X1, X2)) | | active#(geq(s(X), s(Y))) | → | mark#(geq(X, Y)) |
| mark#(if(X1, X2, X3)) | → | mark#(X1) | | mark#(div(X1, X2)) | → | active#(div(mark(X1), X2)) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, 0, minus, s, if, div, active, true, false, mark
Strategy
Polynomial Interpretation
- 0: 0
- active(x): 0
- active#(x): x
- div(x,y): 1
- false: 3
- geq(x,y): 1
- if(x,y,z): 0
- mark(x): 0
- mark#(x): 1
- minus(x,y): 1
- s(x): 0
- true: 3
Standard Usable rules
| mark(minus(X1, X2)) | → | active(minus(X1, X2)) | | minus(X1, active(X2)) | → | minus(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| mark(s(X)) | → | active(s(mark(X))) | | div(X1, mark(X2)) | → | div(X1, X2) |
| active(div(0, s(Y))) | → | mark(0) | | mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) |
| minus(mark(X1), X2) | → | minus(X1, X2) | | active(minus(0, Y)) | → | mark(0) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | minus(X1, mark(X2)) | → | minus(X1, X2) |
| geq(mark(X1), X2) | → | geq(X1, X2) | | mark(true) | → | active(true) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | div(X1, active(X2)) | → | div(X1, X2) |
| if(X1, X2, mark(X3)) | → | if(X1, X2, X3) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| mark(0) | → | active(0) | | s(active(X)) | → | s(X) |
| active(geq(X, 0)) | → | mark(true) | | minus(active(X1), X2) | → | minus(X1, X2) |
| if(X1, active(X2), X3) | → | if(X1, X2, X3) | | div(mark(X1), X2) | → | div(X1, X2) |
| if(mark(X1), X2, X3) | → | if(X1, X2, X3) | | active(geq(0, s(Y))) | → | mark(false) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| mark(div(X1, X2)) | → | active(div(mark(X1), X2)) | | active(if(false, X, Y)) | → | mark(Y) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | if(X1, mark(X2), X3) | → | if(X1, X2, X3) |
| mark(false) | → | active(false) | | s(mark(X)) | → | s(X) |
| active(if(true, X, Y)) | → | mark(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(if(X1, X2, X3)) | → | active#(if(mark(X1), X2, X3)) |
Problem 20: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| active#(div(s(X), s(Y))) | → | mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | mark#(geq(X1, X2)) | → | active#(geq(X1, X2)) |
| active#(geq(s(X), s(Y))) | → | mark#(geq(X, Y)) | | mark#(if(X1, X2, X3)) | → | mark#(X1) |
| mark#(div(X1, X2)) | → | active#(div(mark(X1), X2)) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, minus, 0, s, if, div, false, true, active, mark
Strategy
Polynomial Interpretation
- 0: 0
- active(x): x
- active#(x): 0
- div(x,y): 3y + 1
- false: 0
- geq(x,y): 0
- if(x,y,z): z + 2y + x
- mark(x): x
- mark#(x): 2x
- minus(x,y): 0
- s(x): 0
- true: 0
Standard Usable rules
| mark(minus(X1, X2)) | → | active(minus(X1, X2)) | | minus(X1, active(X2)) | → | minus(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| mark(s(X)) | → | active(s(mark(X))) | | div(X1, mark(X2)) | → | div(X1, X2) |
| active(div(0, s(Y))) | → | mark(0) | | mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) |
| minus(mark(X1), X2) | → | minus(X1, X2) | | active(minus(0, Y)) | → | mark(0) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | minus(X1, mark(X2)) | → | minus(X1, X2) |
| geq(mark(X1), X2) | → | geq(X1, X2) | | mark(true) | → | active(true) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | div(X1, active(X2)) | → | div(X1, X2) |
| if(X1, X2, mark(X3)) | → | if(X1, X2, X3) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| mark(0) | → | active(0) | | s(active(X)) | → | s(X) |
| active(geq(X, 0)) | → | mark(true) | | minus(active(X1), X2) | → | minus(X1, X2) |
| if(X1, active(X2), X3) | → | if(X1, X2, X3) | | div(mark(X1), X2) | → | div(X1, X2) |
| if(mark(X1), X2, X3) | → | if(X1, X2, X3) | | active(geq(0, s(Y))) | → | mark(false) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| mark(div(X1, X2)) | → | active(div(mark(X1), X2)) | | active(if(false, X, Y)) | → | mark(Y) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | if(X1, mark(X2), X3) | → | if(X1, X2, X3) |
| mark(false) | → | active(false) | | s(mark(X)) | → | s(X) |
| active(if(true, X, Y)) | → | mark(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(div(X1, X2)) | → | active#(div(mark(X1), X2)) |
Problem 21: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| active#(div(s(X), s(Y))) | → | mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | mark#(geq(X1, X2)) | → | active#(geq(X1, X2)) |
| active#(geq(s(X), s(Y))) | → | mark#(geq(X, Y)) | | mark#(if(X1, X2, X3)) | → | mark#(X1) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, 0, minus, s, if, div, active, true, false, mark
Strategy
Polynomial Interpretation
- 0: 0
- active(x): 3x + 1
- active#(x): 2x
- div(x,y): 1
- false: 0
- geq(x,y): 0
- if(x,y,z): 2y
- mark(x): 2x + 1
- mark#(x): 0
- minus(x,y): 2y + x + 1
- s(x): 0
- true: 0
Standard Usable rules
| if(X1, active(X2), X3) | → | if(X1, X2, X3) | | minus(X1, active(X2)) | → | minus(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| if(mark(X1), X2, X3) | → | if(X1, X2, X3) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | geq(X1, mark(X2)) | → | geq(X1, X2) |
| geq(active(X1), X2) | → | geq(X1, X2) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | minus(X1, mark(X2)) | → | minus(X1, X2) |
| geq(mark(X1), X2) | → | geq(X1, X2) | | if(X1, mark(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | div(X1, active(X2)) | → | div(X1, X2) |
| if(X1, X2, mark(X3)) | → | if(X1, X2, X3) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | minus(active(X1), X2) | → | minus(X1, X2) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| active#(div(s(X), s(Y))) | → | mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) |
Problem 22: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(geq(X1, X2)) | → | active#(geq(X1, X2)) | | active#(geq(s(X), s(Y))) | → | mark#(geq(X, Y)) |
| mark#(if(X1, X2, X3)) | → | mark#(X1) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, minus, 0, s, if, div, false, true, active, mark
Strategy
Polynomial Interpretation
- 0: 0
- active(x): x
- active#(x): x
- div(x,y): 0
- false: 0
- geq(x,y): 2y + 2x
- if(x,y,z): 3z + 2x + 1
- mark(x): x
- mark#(x): 2x
- minus(x,y): 0
- s(x): 2x
- true: 0
Standard Usable rules
| geq(X1, active(X2)) | → | geq(X1, X2) | | geq(X1, mark(X2)) | → | geq(X1, X2) |
| geq(active(X1), X2) | → | geq(X1, X2) | | geq(mark(X1), X2) | → | geq(X1, X2) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(if(X1, X2, X3)) | → | mark#(X1) |
Problem 23: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| mark#(geq(X1, X2)) | → | active#(geq(X1, X2)) | | active#(geq(s(X), s(Y))) | → | mark#(geq(X, Y)) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, 0, minus, s, if, div, active, true, false, mark
Strategy
Function Precedence
active = mark < active# < geq = minus = 0 = s = if = div = false = true = mark#
Argument Filtering
geq: collapses to 2
minus: all arguments are removed from minus
0: all arguments are removed from 0
s: 1
if: all arguments are removed from if
div: all arguments are removed from div
false: all arguments are removed from false
true: all arguments are removed from true
active: collapses to 1
mark: 1
active#: collapses to 1
mark#: 1
Status
minus: multiset
0: multiset
s: lexicographic with permutation 1 → 1
if: multiset
div: multiset
false: multiset
true: multiset
mark: multiset
mark#: lexicographic with permutation 1 → 1
Usable Rules
| geq(X1, active(X2)) → geq(X1, X2) | geq(X1, mark(X2)) → geq(X1, X2) |
| geq(active(X1), X2) → geq(X1, X2) | geq(mark(X1), X2) → geq(X1, X2) |
The dependency pairs and usable rules are stronlgy conservative!
Eliminated dependency pairs
The following dependency pairs (at least) can be eliminated according to the given precedence.
| mark#(geq(X1, X2)) → active#(geq(X1, X2)) |
Problem 24: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| active#(geq(s(X), s(Y))) | → | mark#(geq(X, Y)) |
Rewrite Rules
| active(minus(0, Y)) | → | mark(0) | | active(minus(s(X), s(Y))) | → | mark(minus(X, Y)) |
| active(geq(X, 0)) | → | mark(true) | | active(geq(0, s(Y))) | → | mark(false) |
| active(geq(s(X), s(Y))) | → | mark(geq(X, Y)) | | active(div(0, s(Y))) | → | mark(0) |
| active(div(s(X), s(Y))) | → | mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)) | | active(if(true, X, Y)) | → | mark(X) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(minus(X1, X2)) | → | active(minus(X1, X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(geq(X1, X2)) | → | active(geq(X1, X2)) | | mark(true) | → | active(true) |
| mark(false) | → | active(false) | | mark(div(X1, X2)) | → | active(div(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | minus(mark(X1), X2) | → | minus(X1, X2) |
| minus(X1, mark(X2)) | → | minus(X1, X2) | | minus(active(X1), X2) | → | minus(X1, X2) |
| minus(X1, active(X2)) | → | minus(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | geq(mark(X1), X2) | → | geq(X1, X2) |
| geq(X1, mark(X2)) | → | geq(X1, X2) | | geq(active(X1), X2) | → | geq(X1, X2) |
| geq(X1, active(X2)) | → | geq(X1, X2) | | div(mark(X1), X2) | → | div(X1, X2) |
| div(X1, mark(X2)) | → | div(X1, X2) | | div(active(X1), X2) | → | div(X1, X2) |
| div(X1, active(X2)) | → | div(X1, X2) | | if(mark(X1), X2, X3) | → | if(X1, X2, X3) |
| if(X1, mark(X2), X3) | → | if(X1, X2, X3) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| if(active(X1), X2, X3) | → | if(X1, X2, X3) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
Original Signature
Termination of terms over the following signature is verified: geq, minus, 0, s, if, div, false, true, active, mark
Strategy
There are no SCCs!