YES
The TRS could be proven terminating. The proof took 29341 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (921ms).
| – Problem 2 was processed with processor SubtermCriterion (2ms).
| | – Problem 10 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor SubtermCriterion (3ms).
| | – Problem 11 was processed with processor SubtermCriterion (0ms).
| – Problem 4 was processed with processor PolynomialLinearRange4 (264ms).
| | – Problem 16 was processed with processor PolynomialLinearRange4 (417ms).
| | | – Problem 18 was processed with processor PolynomialLinearRange4 (201ms).
| | | | – Problem 19 was processed with processor PolynomialLinearRange4 (186ms).
| | | | | – Problem 20 was processed with processor PolynomialLinearRange4 (194ms).
| | | | | | – Problem 21 was processed with processor PolynomialLinearRange4 (187ms).
| | | | | | | – Problem 22 was processed with processor PolynomialLinearRange4 (197ms).
| | | | | | | | – Problem 23 was processed with processor PolynomialLinearRange4 (160ms).
| | | | | | | | | – Problem 24 was processed with processor PolynomialLinearRange4 (170ms).
| | | | | | | | | | – Problem 25 was processed with processor PolynomialLinearRange4 (134ms).
| | | | | | | | | | | – Problem 26 was processed with processor ReductionPairSAT (3064ms).
| | | | | | | | | | | | – Problem 27 was processed with processor ReductionPairSAT (2459ms).
| | | | | | | | | | | | | – Problem 28 was processed with processor DependencyGraph (0ms).
| – Problem 5 was processed with processor SubtermCriterion (2ms).
| | – Problem 12 was processed with processor SubtermCriterion (1ms).
| – Problem 6 was processed with processor SubtermCriterion (3ms).
| – Problem 7 was processed with processor SubtermCriterion (2ms).
| | – Problem 13 was processed with processor SubtermCriterion (0ms).
| – Problem 8 was processed with processor SubtermCriterion (2ms).
| | – Problem 14 was processed with processor SubtermCriterion (0ms).
| | | – Problem 15 was processed with processor PolynomialLinearRange4 (21ms).
| | | | – Problem 17 was processed with processor PolynomialLinearRange4 (127ms).
| – Problem 9 was processed with processor SubtermCriterion (2ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| active#(first(0, X)) | → | mark#(nil) | | active#(and(false, Y)) | → | mark#(false) |
| add#(X1, mark(X2)) | → | add#(X1, X2) | | active#(add(s(X), Y)) | → | mark#(s(add(X, Y))) |
| if#(X1, X2, active(X3)) | → | if#(X1, X2, X3) | | active#(first(s(X), cons(Y, Z))) | → | cons#(Y, first(X, Z)) |
| first#(X1, active(X2)) | → | first#(X1, X2) | | active#(if(true, X, Y)) | → | mark#(X) |
| active#(first(s(X), cons(Y, Z))) | → | mark#(cons(Y, first(X, Z))) | | first#(mark(X1), X2) | → | first#(X1, X2) |
| mark#(add(X1, X2)) | → | mark#(X1) | | mark#(true) | → | active#(true) |
| mark#(and(X1, X2)) | → | and#(mark(X1), X2) | | active#(add(0, X)) | → | mark#(X) |
| add#(mark(X1), X2) | → | add#(X1, X2) | | and#(mark(X1), X2) | → | and#(X1, X2) |
| active#(from(X)) | → | mark#(cons(X, from(s(X)))) | | mark#(s(X)) | → | active#(s(X)) |
| active#(from(X)) | → | s#(X) | | mark#(and(X1, X2)) | → | mark#(X1) |
| cons#(X1, active(X2)) | → | cons#(X1, X2) | | active#(add(s(X), Y)) | → | add#(X, Y) |
| if#(X1, mark(X2), X3) | → | if#(X1, X2, X3) | | first#(active(X1), X2) | → | first#(X1, X2) |
| from#(active(X)) | → | from#(X) | | if#(X1, X2, mark(X3)) | → | if#(X1, X2, X3) |
| add#(active(X1), X2) | → | add#(X1, X2) | | mark#(first(X1, X2)) | → | mark#(X1) |
| if#(mark(X1), X2, X3) | → | if#(X1, X2, X3) | | mark#(if(X1, X2, X3)) | → | mark#(X1) |
| and#(active(X1), X2) | → | and#(X1, X2) | | mark#(false) | → | active#(false) |
| mark#(add(X1, X2)) | → | active#(add(mark(X1), X2)) | | mark#(if(X1, X2, X3)) | → | active#(if(mark(X1), X2, X3)) |
| active#(if(false, X, Y)) | → | mark#(Y) | | and#(X1, active(X2)) | → | and#(X1, X2) |
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | mark#(add(X1, X2)) | → | add#(mark(X1), X2) |
| mark#(cons(X1, X2)) | → | cons#(X1, X2) | | if#(X1, active(X2), X3) | → | if#(X1, X2, X3) |
| from#(mark(X)) | → | from#(X) | | active#(and(true, X)) | → | mark#(X) |
| mark#(from(X)) | → | from#(X) | | active#(first(s(X), cons(Y, Z))) | → | first#(X, Z) |
| mark#(nil) | → | active#(nil) | | active#(add(s(X), Y)) | → | s#(add(X, Y)) |
| active#(from(X)) | → | cons#(X, from(s(X))) | | mark#(and(X1, X2)) | → | active#(and(mark(X1), X2)) |
| add#(X1, active(X2)) | → | add#(X1, X2) | | cons#(X1, mark(X2)) | → | cons#(X1, X2) |
| mark#(first(X1, X2)) | → | first#(mark(X1), mark(X2)) | | and#(X1, mark(X2)) | → | and#(X1, X2) |
| first#(X1, mark(X2)) | → | first#(X1, X2) | | mark#(if(X1, X2, X3)) | → | if#(mark(X1), X2, X3) |
| mark#(first(X1, X2)) | → | mark#(X2) | | mark#(0) | → | active#(0) |
| mark#(first(X1, X2)) | → | active#(first(mark(X1), mark(X2))) | | mark#(from(X)) | → | active#(from(X)) |
| cons#(active(X1), X2) | → | cons#(X1, X2) | | mark#(cons(X1, X2)) | → | active#(cons(X1, X2)) |
| if#(active(X1), X2, X3) | → | if#(X1, X2, X3) | | mark#(s(X)) | → | s#(X) |
| s#(mark(X)) | → | s#(X) | | s#(active(X)) | → | s#(X) |
| active#(from(X)) | → | from#(s(X)) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
The following SCCs where found
| from#(active(X)) → from#(X) | from#(mark(X)) → from#(X) |
| mark#(first(X1, X2)) → mark#(X2) | mark#(if(X1, X2, X3)) → active#(if(mark(X1), X2, X3)) |
| mark#(add(X1, X2)) → active#(add(mark(X1), X2)) | active#(if(false, X, Y)) → mark#(Y) |
| mark#(first(X1, X2)) → active#(first(mark(X1), mark(X2))) | active#(add(s(X), Y)) → mark#(s(add(X, Y))) |
| active#(add(0, X)) → mark#(X) | mark#(from(X)) → active#(from(X)) |
| active#(from(X)) → mark#(cons(X, from(s(X)))) | active#(and(true, X)) → mark#(X) |
| mark#(s(X)) → active#(s(X)) | mark#(cons(X1, X2)) → active#(cons(X1, X2)) |
| active#(if(true, X, Y)) → mark#(X) | mark#(and(X1, X2)) → mark#(X1) |
| active#(first(s(X), cons(Y, Z))) → mark#(cons(Y, first(X, Z))) | mark#(and(X1, X2)) → active#(and(mark(X1), X2)) |
| mark#(first(X1, X2)) → mark#(X1) | mark#(if(X1, X2, X3)) → mark#(X1) |
| mark#(add(X1, X2)) → mark#(X1) |
| s#(mark(X)) → s#(X) | s#(active(X)) → s#(X) |
| cons#(X1, active(X2)) → cons#(X1, X2) | cons#(mark(X1), X2) → cons#(X1, X2) |
| cons#(X1, mark(X2)) → cons#(X1, X2) | cons#(active(X1), X2) → cons#(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) |
| and#(active(X1), X2) → and#(X1, X2) | and#(X1, active(X2)) → and#(X1, X2) |
| and#(mark(X1), X2) → and#(X1, X2) | and#(X1, mark(X2)) → and#(X1, X2) |
| first#(active(X1), X2) → first#(X1, X2) | first#(mark(X1), X2) → first#(X1, X2) |
| first#(X1, mark(X2)) → first#(X1, X2) | first#(X1, active(X2)) → first#(X1, X2) |
| add#(active(X1), X2) → add#(X1, X2) | add#(X1, mark(X2)) → add#(X1, X2) |
| add#(X1, active(X2)) → add#(X1, X2) | add#(mark(X1), X2) → add#(X1, X2) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons#(X1, active(X2)) | → | cons#(X1, X2) | | cons#(mark(X1), X2) | → | cons#(X1, X2) |
| cons#(X1, mark(X2)) | → | cons#(X1, X2) | | cons#(active(X1), X2) | → | cons#(X1, X2) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | cons#(active(X1), X2) | → | cons#(X1, X2) |
Problem 10: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons#(X1, active(X2)) | → | cons#(X1, X2) | | cons#(X1, mark(X2)) | → | cons#(X1, X2) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| cons#(X1, active(X2)) | → | cons#(X1, X2) | | cons#(X1, mark(X2)) | → | cons#(X1, X2) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| and#(active(X1), X2) | → | and#(X1, X2) | | and#(X1, active(X2)) | → | and#(X1, X2) |
| and#(mark(X1), X2) | → | and#(X1, X2) | | and#(X1, mark(X2)) | → | and#(X1, X2) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| and#(active(X1), X2) | → | and#(X1, X2) | | and#(mark(X1), X2) | → | and#(X1, X2) |
Problem 11: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| and#(X1, active(X2)) | → | and#(X1, X2) | | and#(X1, mark(X2)) | → | and#(X1, X2) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| and#(X1, active(X2)) | → | and#(X1, X2) | | and#(X1, mark(X2)) | → | and#(X1, X2) |
Problem 4: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(first(X1, X2)) | → | mark#(X2) | | mark#(add(X1, X2)) | → | active#(add(mark(X1), X2)) |
| mark#(if(X1, X2, X3)) | → | active#(if(mark(X1), X2, X3)) | | active#(if(false, X, Y)) | → | mark#(Y) |
| mark#(first(X1, X2)) | → | active#(first(mark(X1), mark(X2))) | | active#(add(s(X), Y)) | → | mark#(s(add(X, Y))) |
| active#(add(0, X)) | → | mark#(X) | | mark#(from(X)) | → | active#(from(X)) |
| active#(from(X)) | → | mark#(cons(X, from(s(X)))) | | active#(and(true, X)) | → | mark#(X) |
| mark#(s(X)) | → | active#(s(X)) | | mark#(cons(X1, X2)) | → | active#(cons(X1, X2)) |
| active#(if(true, X, Y)) | → | mark#(X) | | mark#(and(X1, X2)) | → | mark#(X1) |
| active#(first(s(X), cons(Y, Z))) | → | mark#(cons(Y, first(X, Z))) | | mark#(and(X1, X2)) | → | active#(and(mark(X1), X2)) |
| mark#(first(X1, X2)) | → | mark#(X1) | | mark#(if(X1, X2, X3)) | → | mark#(X1) |
| mark#(add(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- active(x): x
- active#(x): x
- add(x,y): 2y + 2x
- and(x,y): 2y + x + 2
- cons(x,y): y
- false: 1
- first(x,y): 2y + 2x + 2
- from(x): 2
- if(x,y,z): 2z + y + 2x
- mark(x): x
- mark#(x): x
- nil: 0
- s(x): x
- true: 0
Standard Usable rules
| cons(active(X1), X2) | → | cons(X1, X2) | | from(mark(X)) | → | from(X) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | active(and(false, Y)) | → | mark(false) |
| active(first(0, X)) | → | mark(nil) | | mark(cons(X1, X2)) | → | active(cons(X1, X2)) |
| mark(s(X)) | → | active(s(X)) | | if(active(X1), X2, X3) | → | if(X1, X2, X3) |
| and(active(X1), X2) | → | and(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| first(X1, mark(X2)) | → | first(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| mark(true) | → | active(true) | | first(active(X1), X2) | → | first(X1, X2) |
| mark(and(X1, X2)) | → | active(and(mark(X1), X2)) | | first(X1, active(X2)) | → | first(X1, X2) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | add(X1, active(X2)) | → | add(X1, X2) |
| active(and(true, X)) | → | mark(X) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | add(mark(X1), X2) | → | add(X1, X2) |
| mark(nil) | → | active(nil) | | s(active(X)) | → | s(X) |
| mark(0) | → | active(0) | | from(active(X)) | → | from(X) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(mark(X1), X2, X3) | → | if(X1, X2, X3) | | first(mark(X1), X2) | → | first(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | if(X1, mark(X2), X3) | → | if(X1, X2, X3) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | mark(false) | → | active(false) |
| active(add(0, X)) | → | mark(X) | | s(mark(X)) | → | s(X) |
| and(X1, active(X2)) | → | and(X1, X2) | | 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#(first(X1, X2)) | → | mark#(X2) | | active#(if(false, X, Y)) | → | mark#(Y) |
| active#(and(true, X)) | → | mark#(X) | | mark#(and(X1, X2)) | → | mark#(X1) |
| mark#(first(X1, X2)) | → | mark#(X1) |
Problem 16: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(add(X1, X2)) | → | active#(add(mark(X1), X2)) | | mark#(if(X1, X2, X3)) | → | active#(if(mark(X1), X2, X3)) |
| mark#(first(X1, X2)) | → | active#(first(mark(X1), mark(X2))) | | active#(add(s(X), Y)) | → | mark#(s(add(X, Y))) |
| active#(add(0, X)) | → | mark#(X) | | mark#(from(X)) | → | active#(from(X)) |
| active#(from(X)) | → | mark#(cons(X, from(s(X)))) | | mark#(s(X)) | → | active#(s(X)) |
| mark#(cons(X1, X2)) | → | active#(cons(X1, X2)) | | active#(if(true, X, Y)) | → | mark#(X) |
| active#(first(s(X), cons(Y, Z))) | → | mark#(cons(Y, first(X, Z))) | | mark#(and(X1, X2)) | → | active#(and(mark(X1), X2)) |
| mark#(if(X1, X2, X3)) | → | mark#(X1) | | mark#(add(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Polynomial Interpretation
- 0: 1
- active(x): x
- active#(x): 2x
- add(x,y): 2y + x
- and(x,y): 3y + x
- cons(x,y): 0
- false: 2
- first(x,y): 2x
- from(x): x
- if(x,y,z): 2z + 2y + x
- mark(x): x
- mark#(x): 2x
- nil: 2
- s(x): 0
- true: 0
Standard Usable rules
| cons(active(X1), X2) | → | cons(X1, X2) | | from(mark(X)) | → | from(X) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | active(and(false, Y)) | → | mark(false) |
| active(first(0, X)) | → | mark(nil) | | mark(cons(X1, X2)) | → | active(cons(X1, X2)) |
| mark(s(X)) | → | active(s(X)) | | if(active(X1), X2, X3) | → | if(X1, X2, X3) |
| and(active(X1), X2) | → | and(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| first(X1, mark(X2)) | → | first(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| mark(true) | → | active(true) | | first(active(X1), X2) | → | first(X1, X2) |
| mark(and(X1, X2)) | → | active(and(mark(X1), X2)) | | first(X1, active(X2)) | → | first(X1, X2) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | add(X1, active(X2)) | → | add(X1, X2) |
| active(and(true, X)) | → | mark(X) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | add(mark(X1), X2) | → | add(X1, X2) |
| mark(nil) | → | active(nil) | | s(active(X)) | → | s(X) |
| mark(0) | → | active(0) | | from(active(X)) | → | from(X) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(mark(X1), X2, X3) | → | if(X1, X2, X3) | | first(mark(X1), X2) | → | first(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | if(X1, mark(X2), X3) | → | if(X1, X2, X3) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | mark(false) | → | active(false) |
| active(add(0, X)) | → | mark(X) | | s(mark(X)) | → | s(X) |
| and(X1, active(X2)) | → | and(X1, X2) | | 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#(add(0, X)) | → | mark#(X) |
Problem 18: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(add(X1, X2)) | → | active#(add(mark(X1), X2)) | | mark#(if(X1, X2, X3)) | → | active#(if(mark(X1), X2, X3)) |
| mark#(first(X1, X2)) | → | active#(first(mark(X1), mark(X2))) | | active#(add(s(X), Y)) | → | mark#(s(add(X, Y))) |
| mark#(from(X)) | → | active#(from(X)) | | active#(from(X)) | → | mark#(cons(X, from(s(X)))) |
| mark#(s(X)) | → | active#(s(X)) | | mark#(cons(X1, X2)) | → | active#(cons(X1, X2)) |
| active#(if(true, X, Y)) | → | mark#(X) | | active#(first(s(X), cons(Y, Z))) | → | mark#(cons(Y, first(X, Z))) |
| mark#(and(X1, X2)) | → | active#(and(mark(X1), X2)) | | mark#(if(X1, X2, X3)) | → | mark#(X1) |
| mark#(add(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- active(x): x
- active#(x): x
- add(x,y): y + x
- and(x,y): y
- cons(x,y): y
- false: 0
- first(x,y): 0
- from(x): 2
- if(x,y,z): 2z + 2y + 2x
- mark(x): x
- mark#(x): x
- nil: 0
- s(x): 0
- true: 1
Standard Usable rules
| cons(active(X1), X2) | → | cons(X1, X2) | | from(mark(X)) | → | from(X) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | active(and(false, Y)) | → | mark(false) |
| active(first(0, X)) | → | mark(nil) | | mark(cons(X1, X2)) | → | active(cons(X1, X2)) |
| mark(s(X)) | → | active(s(X)) | | if(active(X1), X2, X3) | → | if(X1, X2, X3) |
| and(active(X1), X2) | → | and(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| first(X1, mark(X2)) | → | first(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| mark(true) | → | active(true) | | first(active(X1), X2) | → | first(X1, X2) |
| mark(and(X1, X2)) | → | active(and(mark(X1), X2)) | | first(X1, active(X2)) | → | first(X1, X2) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | add(X1, active(X2)) | → | add(X1, X2) |
| active(and(true, X)) | → | mark(X) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | add(mark(X1), X2) | → | add(X1, X2) |
| mark(nil) | → | active(nil) | | s(active(X)) | → | s(X) |
| mark(0) | → | active(0) | | from(active(X)) | → | from(X) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(mark(X1), X2, X3) | → | if(X1, X2, X3) | | first(mark(X1), X2) | → | first(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | if(X1, mark(X2), X3) | → | if(X1, X2, X3) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | mark(false) | → | active(false) |
| active(add(0, X)) | → | mark(X) | | s(mark(X)) | → | s(X) |
| and(X1, active(X2)) | → | and(X1, X2) | | 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 19: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(if(X1, X2, X3)) | → | active#(if(mark(X1), X2, X3)) | | mark#(add(X1, X2)) | → | active#(add(mark(X1), X2)) |
| active#(first(s(X), cons(Y, Z))) | → | mark#(cons(Y, first(X, Z))) | | mark#(first(X1, X2)) | → | active#(first(mark(X1), mark(X2))) |
| mark#(and(X1, X2)) | → | active#(and(mark(X1), X2)) | | active#(add(s(X), Y)) | → | mark#(s(add(X, Y))) |
| mark#(if(X1, X2, X3)) | → | mark#(X1) | | mark#(from(X)) | → | active#(from(X)) |
| active#(from(X)) | → | mark#(cons(X, from(s(X)))) | | mark#(add(X1, X2)) | → | mark#(X1) |
| mark#(s(X)) | → | active#(s(X)) | | mark#(cons(X1, X2)) | → | active#(cons(X1, X2)) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Polynomial Interpretation
- 0: 3
- active(x): 0
- active#(x): x + 1
- add(x,y): 1
- and(x,y): 0
- cons(x,y): 1
- false: 0
- first(x,y): 1
- from(x): 1
- if(x,y,z): 1
- mark(x): 0
- mark#(x): 2
- nil: 3
- s(x): 1
- true: 3
Standard Usable rules
| cons(active(X1), X2) | → | cons(X1, X2) | | from(mark(X)) | → | from(X) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | active(and(false, Y)) | → | mark(false) |
| active(first(0, X)) | → | mark(nil) | | mark(cons(X1, X2)) | → | active(cons(X1, X2)) |
| mark(s(X)) | → | active(s(X)) | | if(active(X1), X2, X3) | → | if(X1, X2, X3) |
| and(active(X1), X2) | → | and(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| first(X1, mark(X2)) | → | first(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| mark(true) | → | active(true) | | first(active(X1), X2) | → | first(X1, X2) |
| mark(and(X1, X2)) | → | active(and(mark(X1), X2)) | | first(X1, active(X2)) | → | first(X1, X2) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | add(X1, active(X2)) | → | add(X1, X2) |
| active(and(true, X)) | → | mark(X) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | add(mark(X1), X2) | → | add(X1, X2) |
| mark(nil) | → | active(nil) | | s(active(X)) | → | s(X) |
| mark(0) | → | active(0) | | from(active(X)) | → | from(X) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(mark(X1), X2, X3) | → | if(X1, X2, X3) | | first(mark(X1), X2) | → | first(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | if(X1, mark(X2), X3) | → | if(X1, X2, X3) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | mark(false) | → | active(false) |
| active(add(0, X)) | → | mark(X) | | s(mark(X)) | → | s(X) |
| and(X1, active(X2)) | → | and(X1, X2) | | 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#(and(X1, X2)) | → | active#(and(mark(X1), X2)) |
Problem 20: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(add(X1, X2)) | → | active#(add(mark(X1), X2)) | | mark#(if(X1, X2, X3)) | → | active#(if(mark(X1), X2, X3)) |
| active#(first(s(X), cons(Y, Z))) | → | mark#(cons(Y, first(X, Z))) | | mark#(first(X1, X2)) | → | active#(first(mark(X1), mark(X2))) |
| active#(add(s(X), Y)) | → | mark#(s(add(X, Y))) | | mark#(if(X1, X2, X3)) | → | mark#(X1) |
| mark#(from(X)) | → | active#(from(X)) | | active#(from(X)) | → | mark#(cons(X, from(s(X)))) |
| mark#(add(X1, X2)) | → | mark#(X1) | | mark#(s(X)) | → | active#(s(X)) |
| mark#(cons(X1, X2)) | → | active#(cons(X1, X2)) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Polynomial Interpretation
- 0: 3
- active(x): 1
- active#(x): x
- add(x,y): 1
- and(x,y): 1
- cons(x,y): 0
- false: 2
- first(x,y): 1
- from(x): 1
- if(x,y,z): 1
- mark(x): 1
- mark#(x): 1
- nil: 2
- s(x): 1
- true: 3
Standard Usable rules
| cons(active(X1), X2) | → | cons(X1, X2) | | from(mark(X)) | → | from(X) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | active(and(false, Y)) | → | mark(false) |
| active(first(0, X)) | → | mark(nil) | | mark(cons(X1, X2)) | → | active(cons(X1, X2)) |
| mark(s(X)) | → | active(s(X)) | | if(active(X1), X2, X3) | → | if(X1, X2, X3) |
| and(active(X1), X2) | → | and(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| and(X1, mark(X2)) | → | and(X1, X2) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| mark(true) | → | active(true) | | first(active(X1), X2) | → | first(X1, X2) |
| mark(and(X1, X2)) | → | active(and(mark(X1), X2)) | | first(X1, active(X2)) | → | first(X1, X2) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | add(X1, active(X2)) | → | add(X1, X2) |
| active(and(true, X)) | → | mark(X) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | add(mark(X1), X2) | → | add(X1, X2) |
| mark(nil) | → | active(nil) | | mark(0) | → | active(0) |
| s(active(X)) | → | s(X) | | from(active(X)) | → | from(X) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(mark(X1), X2, X3) | → | if(X1, X2, X3) | | add(active(X1), X2) | → | add(X1, X2) |
| first(mark(X1), X2) | → | first(X1, X2) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | if(X1, mark(X2), X3) | → | if(X1, X2, X3) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | mark(false) | → | active(false) |
| active(add(0, X)) | → | mark(X) | | s(mark(X)) | → | s(X) |
| and(X1, active(X2)) | → | and(X1, X2) | | 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#(cons(X1, X2)) | → | active#(cons(X1, X2)) |
Problem 21: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(if(X1, X2, X3)) | → | active#(if(mark(X1), X2, X3)) | | mark#(add(X1, X2)) | → | active#(add(mark(X1), X2)) |
| active#(first(s(X), cons(Y, Z))) | → | mark#(cons(Y, first(X, Z))) | | mark#(first(X1, X2)) | → | active#(first(mark(X1), mark(X2))) |
| active#(add(s(X), Y)) | → | mark#(s(add(X, Y))) | | mark#(if(X1, X2, X3)) | → | mark#(X1) |
| mark#(from(X)) | → | active#(from(X)) | | active#(from(X)) | → | mark#(cons(X, from(s(X)))) |
| mark#(add(X1, X2)) | → | mark#(X1) | | mark#(s(X)) | → | active#(s(X)) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Polynomial Interpretation
- 0: 3
- active(x): 0
- active#(x): x
- add(x,y): 1
- and(x,y): 1
- cons(x,y): 1
- false: 1
- first(x,y): 1
- from(x): 1
- if(x,y,z): 0
- mark(x): 0
- mark#(x): 1
- nil: 3
- s(x): 0
- true: 3
Standard Usable rules
| cons(active(X1), X2) | → | cons(X1, X2) | | from(mark(X)) | → | from(X) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | active(and(false, Y)) | → | mark(false) |
| active(first(0, X)) | → | mark(nil) | | mark(cons(X1, X2)) | → | active(cons(X1, X2)) |
| mark(s(X)) | → | active(s(X)) | | if(active(X1), X2, X3) | → | if(X1, X2, X3) |
| and(active(X1), X2) | → | and(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| and(X1, mark(X2)) | → | and(X1, X2) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| mark(true) | → | active(true) | | first(active(X1), X2) | → | first(X1, X2) |
| mark(and(X1, X2)) | → | active(and(mark(X1), X2)) | | first(X1, active(X2)) | → | first(X1, X2) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | add(X1, active(X2)) | → | add(X1, X2) |
| active(and(true, X)) | → | mark(X) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | add(mark(X1), X2) | → | add(X1, X2) |
| mark(nil) | → | active(nil) | | mark(0) | → | active(0) |
| s(active(X)) | → | s(X) | | from(active(X)) | → | from(X) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(mark(X1), X2, X3) | → | if(X1, X2, X3) | | add(active(X1), X2) | → | add(X1, X2) |
| first(mark(X1), X2) | → | first(X1, X2) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | if(X1, mark(X2), X3) | → | if(X1, X2, X3) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | mark(false) | → | active(false) |
| active(add(0, X)) | → | mark(X) | | s(mark(X)) | → | s(X) |
| and(X1, active(X2)) | → | and(X1, X2) | | 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)) | | mark#(s(X)) | → | active#(s(X)) |
Problem 22: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(add(X1, X2)) | → | active#(add(mark(X1), X2)) | | active#(first(s(X), cons(Y, Z))) | → | mark#(cons(Y, first(X, Z))) |
| mark#(first(X1, X2)) | → | active#(first(mark(X1), mark(X2))) | | active#(add(s(X), Y)) | → | mark#(s(add(X, Y))) |
| mark#(if(X1, X2, X3)) | → | mark#(X1) | | mark#(from(X)) | → | active#(from(X)) |
| active#(from(X)) | → | mark#(cons(X, from(s(X)))) | | mark#(add(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- active(x): x
- active#(x): 0
- add(x,y): 2y + 2x
- and(x,y): y + x
- cons(x,y): 0
- false: 2
- first(x,y): 1
- from(x): 1
- if(x,y,z): z + 2y + x
- mark(x): x
- mark#(x): 2x
- nil: 0
- s(x): 0
- true: 3
Standard Usable rules
| cons(active(X1), X2) | → | cons(X1, X2) | | from(mark(X)) | → | from(X) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | active(and(false, Y)) | → | mark(false) |
| active(first(0, X)) | → | mark(nil) | | mark(cons(X1, X2)) | → | active(cons(X1, X2)) |
| mark(s(X)) | → | active(s(X)) | | if(active(X1), X2, X3) | → | if(X1, X2, X3) |
| and(active(X1), X2) | → | and(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| and(X1, mark(X2)) | → | and(X1, X2) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| first(X1, mark(X2)) | → | first(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| mark(true) | → | active(true) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| first(active(X1), X2) | → | first(X1, X2) | | if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
| first(X1, active(X2)) | → | first(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| active(and(true, X)) | → | mark(X) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | add(mark(X1), X2) | → | add(X1, X2) |
| mark(nil) | → | active(nil) | | mark(0) | → | active(0) |
| s(active(X)) | → | s(X) | | from(active(X)) | → | from(X) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(mark(X1), X2, X3) | → | if(X1, X2, X3) | | add(active(X1), X2) | → | add(X1, X2) |
| first(mark(X1), X2) | → | first(X1, X2) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | if(X1, mark(X2), X3) | → | if(X1, X2, X3) |
| mark(false) | → | active(false) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| active(add(0, X)) | → | mark(X) | | s(mark(X)) | → | s(X) |
| and(X1, active(X2)) | → | and(X1, X2) | | 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#(first(X1, X2)) | → | active#(first(mark(X1), mark(X2))) | | mark#(from(X)) | → | active#(from(X)) |
Problem 23: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(add(X1, X2)) | → | active#(add(mark(X1), X2)) | | active#(first(s(X), cons(Y, Z))) | → | mark#(cons(Y, first(X, Z))) |
| active#(add(s(X), Y)) | → | mark#(s(add(X, Y))) | | mark#(if(X1, X2, X3)) | → | mark#(X1) |
| active#(from(X)) | → | mark#(cons(X, from(s(X)))) | | mark#(add(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Polynomial Interpretation
- 0: 3
- active(x): 3
- active#(x): x
- add(x,y): 0
- and(x,y): 1
- cons(x,y): 1
- false: 3
- first(x,y): 0
- from(x): 1
- if(x,y,z): 0
- mark(x): 3
- mark#(x): 0
- nil: 3
- s(x): 1
- true: 1
Standard Usable rules
| cons(active(X1), X2) | → | cons(X1, X2) | | from(mark(X)) | → | from(X) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | active(and(false, Y)) | → | mark(false) |
| active(first(0, X)) | → | mark(nil) | | mark(cons(X1, X2)) | → | active(cons(X1, X2)) |
| mark(s(X)) | → | active(s(X)) | | if(active(X1), X2, X3) | → | if(X1, X2, X3) |
| and(active(X1), X2) | → | and(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| and(X1, mark(X2)) | → | and(X1, X2) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| first(X1, mark(X2)) | → | first(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| mark(true) | → | active(true) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| first(active(X1), X2) | → | first(X1, X2) | | if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
| first(X1, active(X2)) | → | first(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| active(and(true, X)) | → | mark(X) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | add(mark(X1), X2) | → | add(X1, X2) |
| mark(nil) | → | active(nil) | | mark(0) | → | active(0) |
| s(active(X)) | → | s(X) | | from(active(X)) | → | from(X) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(mark(X1), X2, X3) | → | if(X1, X2, X3) | | add(active(X1), X2) | → | add(X1, X2) |
| first(mark(X1), X2) | → | first(X1, X2) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | if(X1, mark(X2), X3) | → | if(X1, X2, X3) |
| mark(false) | → | active(false) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| active(add(0, X)) | → | mark(X) | | s(mark(X)) | → | s(X) |
| and(X1, active(X2)) | → | and(X1, X2) | | 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#(from(X)) | → | mark#(cons(X, from(s(X)))) |
Problem 24: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(add(X1, X2)) | → | active#(add(mark(X1), X2)) | | active#(first(s(X), cons(Y, Z))) | → | mark#(cons(Y, first(X, Z))) |
| active#(add(s(X), Y)) | → | mark#(s(add(X, Y))) | | mark#(if(X1, X2, X3)) | → | mark#(X1) |
| mark#(add(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Polynomial Interpretation
- 0: 3
- active(x): 0
- active#(x): x
- add(x,y): 0
- and(x,y): 2
- cons(x,y): 2
- false: 2
- first(x,y): 2
- from(x): 3
- if(x,y,z): 0
- mark(x): 0
- mark#(x): 0
- nil: 3
- s(x): 0
- true: 2
Standard Usable rules
| cons(active(X1), X2) | → | cons(X1, X2) | | from(mark(X)) | → | from(X) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | active(and(false, Y)) | → | mark(false) |
| active(first(0, X)) | → | mark(nil) | | mark(cons(X1, X2)) | → | active(cons(X1, X2)) |
| mark(s(X)) | → | active(s(X)) | | if(active(X1), X2, X3) | → | if(X1, X2, X3) |
| and(active(X1), X2) | → | and(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| and(X1, mark(X2)) | → | and(X1, X2) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| first(X1, mark(X2)) | → | first(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| mark(true) | → | active(true) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| first(active(X1), X2) | → | first(X1, X2) | | if(X1, X2, active(X3)) | → | if(X1, X2, X3) |
| first(X1, active(X2)) | → | first(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| active(and(true, X)) | → | mark(X) | | if(X1, X2, mark(X3)) | → | if(X1, X2, X3) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | add(mark(X1), X2) | → | add(X1, X2) |
| mark(nil) | → | active(nil) | | mark(0) | → | active(0) |
| s(active(X)) | → | s(X) | | from(active(X)) | → | from(X) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(mark(X1), X2, X3) | → | if(X1, X2, X3) | | add(active(X1), X2) | → | add(X1, X2) |
| first(mark(X1), X2) | → | first(X1, X2) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | if(X1, mark(X2), X3) | → | if(X1, X2, X3) |
| mark(false) | → | active(false) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| active(add(0, X)) | → | mark(X) | | s(mark(X)) | → | s(X) |
| and(X1, active(X2)) | → | and(X1, X2) | | 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#(first(s(X), cons(Y, Z))) | → | mark#(cons(Y, first(X, Z))) |
Problem 25: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(add(X1, X2)) | → | active#(add(mark(X1), X2)) | | active#(add(s(X), Y)) | → | mark#(s(add(X, Y))) |
| mark#(if(X1, X2, X3)) | → | mark#(X1) | | mark#(add(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Polynomial Interpretation
- 0: 2
- active(x): x
- active#(x): x
- add(x,y): 2y + x
- and(x,y): 2y
- cons(x,y): 0
- false: 0
- first(x,y): x
- from(x): 0
- if(x,y,z): 2z + y + x + 2
- mark(x): x
- mark#(x): x
- nil: 0
- s(x): 2
- true: 0
Standard Usable rules
| cons(active(X1), X2) | → | cons(X1, X2) | | from(mark(X)) | → | from(X) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | active(and(false, Y)) | → | mark(false) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | active(first(0, X)) | → | mark(nil) |
| mark(s(X)) | → | active(s(X)) | | if(active(X1), X2, X3) | → | if(X1, X2, X3) |
| add(X1, mark(X2)) | → | add(X1, X2) | | and(active(X1), X2) | → | and(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| and(X1, mark(X2)) | → | and(X1, X2) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| mark(true) | → | active(true) | | first(active(X1), X2) | → | first(X1, X2) |
| mark(and(X1, X2)) | → | active(and(mark(X1), X2)) | | first(X1, active(X2)) | → | first(X1, X2) |
| if(X1, X2, active(X3)) | → | if(X1, X2, X3) | | add(X1, active(X2)) | → | add(X1, X2) |
| if(X1, X2, mark(X3)) | → | if(X1, X2, X3) | | active(and(true, X)) | → | mark(X) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | add(mark(X1), X2) | → | add(X1, X2) |
| mark(nil) | → | active(nil) | | mark(0) | → | active(0) |
| s(active(X)) | → | s(X) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(active(X)) | → | from(X) | | if(X1, active(X2), X3) | → | if(X1, X2, X3) |
| if(mark(X1), X2, X3) | → | if(X1, X2, X3) | | first(mark(X1), X2) | → | first(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(if(false, X, Y)) | → | mark(Y) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | if(X1, mark(X2), X3) | → | if(X1, X2, X3) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | mark(false) | → | active(false) |
| active(add(0, X)) | → | mark(X) | | s(mark(X)) | → | s(X) |
| and(X1, active(X2)) | → | and(X1, X2) | | 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)) | → | mark#(X1) |
Problem 26: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| mark#(add(X1, X2)) | → | active#(add(mark(X1), X2)) | | active#(add(s(X), Y)) | → | mark#(s(add(X, Y))) |
| mark#(add(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Function Precedence
true < mark = false < and < first < nil < from = add = mark# = 0 = s = if = active = active# = cons
Argument Filtering
true: all arguments are removed from true
mark: collapses to 1
from: all arguments are removed from from
add: 1 2
mark#: collapses to 1
and: 1 2
0: all arguments are removed from 0
s: collapses to 1
if: 1 2 3
active: collapses to 1
false: all arguments are removed from false
active#: collapses to 1
first: all arguments are removed from first
cons: all arguments are removed from cons
nil: all arguments are removed from nil
Status
true: multiset
from: multiset
add: lexicographic with permutation 1 → 1 2 → 2
and: lexicographic with permutation 1 → 2 2 → 1
0: multiset
if: lexicographic with permutation 1 → 3 2 → 2 3 → 1
false: multiset
first: multiset
cons: multiset
nil: multiset
Usable Rules
| cons(active(X1), X2) → cons(X1, X2) | from(mark(X)) → from(X) |
| mark(first(X1, X2)) → active(first(mark(X1), mark(X2))) | mark(add(X1, X2)) → active(add(mark(X1), X2)) |
| mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3)) | active(and(false, Y)) → mark(false) |
| mark(cons(X1, X2)) → active(cons(X1, X2)) | active(first(0, X)) → mark(nil) |
| mark(s(X)) → active(s(X)) | if(active(X1), X2, X3) → if(X1, X2, X3) |
| add(X1, mark(X2)) → add(X1, X2) | and(active(X1), X2) → and(X1, X2) |
| cons(X1, mark(X2)) → cons(X1, X2) | first(X1, mark(X2)) → first(X1, X2) |
| and(X1, mark(X2)) → and(X1, X2) | active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z))) |
| mark(true) → active(true) | first(active(X1), X2) → first(X1, X2) |
| mark(and(X1, X2)) → active(and(mark(X1), X2)) | first(X1, active(X2)) → first(X1, X2) |
| if(X1, X2, active(X3)) → if(X1, X2, X3) | add(X1, active(X2)) → add(X1, X2) |
| if(X1, X2, mark(X3)) → if(X1, X2, X3) | active(and(true, X)) → mark(X) |
| active(from(X)) → mark(cons(X, from(s(X)))) | add(mark(X1), X2) → add(X1, X2) |
| mark(nil) → active(nil) | mark(0) → active(0) |
| s(active(X)) → s(X) | cons(X1, active(X2)) → cons(X1, X2) |
| from(active(X)) → from(X) | if(X1, active(X2), X3) → if(X1, X2, X3) |
| if(mark(X1), X2, X3) → if(X1, X2, X3) | first(mark(X1), X2) → first(X1, X2) |
| add(active(X1), X2) → add(X1, X2) | active(add(s(X), Y)) → mark(s(add(X, Y))) |
| active(if(false, X, Y)) → mark(Y) | mark(from(X)) → active(from(X)) |
| and(mark(X1), X2) → and(X1, X2) | if(X1, mark(X2), X3) → if(X1, X2, X3) |
| cons(mark(X1), X2) → cons(X1, X2) | mark(false) → active(false) |
| active(add(0, X)) → mark(X) | s(mark(X)) → s(X) |
| and(X1, active(X2)) → and(X1, X2) | active(if(true, X, Y)) → mark(X) |
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#(add(X1, X2)) → mark#(X1) |
Problem 27: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| mark#(add(X1, X2)) | → | active#(add(mark(X1), X2)) | | active#(add(s(X), Y)) | → | mark#(s(add(X, Y))) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Function Precedence
active < mark = from = add = mark# = and = 0 = if = false = active# = first < true = s = cons = nil
Argument Filtering
true: all arguments are removed from true
mark: all arguments are removed from mark
from: all arguments are removed from from
add: all arguments are removed from add
mark#: collapses to 1
and: all arguments are removed from and
0: all arguments are removed from 0
s: all arguments are removed from s
if: all arguments are removed from if
active: collapses to 1
false: all arguments are removed from false
active#: all arguments are removed from active#
first: all arguments are removed from first
cons: all arguments are removed from cons
nil: all arguments are removed from nil
Status
true: multiset
mark: multiset
from: multiset
add: multiset
and: multiset
0: multiset
s: multiset
if: multiset
false: multiset
active#: multiset
first: multiset
cons: multiset
nil: multiset
Usable Rules
| cons(active(X1), X2) → cons(X1, X2) | from(mark(X)) → from(X) |
| mark(first(X1, X2)) → active(first(mark(X1), mark(X2))) | mark(add(X1, X2)) → active(add(mark(X1), X2)) |
| mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3)) | active(and(false, Y)) → mark(false) |
| mark(cons(X1, X2)) → active(cons(X1, X2)) | active(first(0, X)) → mark(nil) |
| mark(s(X)) → active(s(X)) | if(active(X1), X2, X3) → if(X1, X2, X3) |
| add(X1, mark(X2)) → add(X1, X2) | and(active(X1), X2) → and(X1, X2) |
| cons(X1, mark(X2)) → cons(X1, X2) | first(X1, mark(X2)) → first(X1, X2) |
| and(X1, mark(X2)) → and(X1, X2) | active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z))) |
| mark(true) → active(true) | first(active(X1), X2) → first(X1, X2) |
| mark(and(X1, X2)) → active(and(mark(X1), X2)) | first(X1, active(X2)) → first(X1, X2) |
| if(X1, X2, active(X3)) → if(X1, X2, X3) | add(X1, active(X2)) → add(X1, X2) |
| if(X1, X2, mark(X3)) → if(X1, X2, X3) | active(and(true, X)) → mark(X) |
| active(from(X)) → mark(cons(X, from(s(X)))) | add(mark(X1), X2) → add(X1, X2) |
| mark(nil) → active(nil) | mark(0) → active(0) |
| s(active(X)) → s(X) | cons(X1, active(X2)) → cons(X1, X2) |
| from(active(X)) → from(X) | if(X1, active(X2), X3) → if(X1, X2, X3) |
| if(mark(X1), X2, X3) → if(X1, X2, X3) | first(mark(X1), X2) → first(X1, X2) |
| add(active(X1), X2) → add(X1, X2) | active(add(s(X), Y)) → mark(s(add(X, Y))) |
| active(if(false, X, Y)) → mark(Y) | mark(from(X)) → active(from(X)) |
| and(mark(X1), X2) → and(X1, X2) | if(X1, mark(X2), X3) → if(X1, X2, X3) |
| cons(mark(X1), X2) → cons(X1, X2) | mark(false) → active(false) |
| active(add(0, X)) → mark(X) | s(mark(X)) → s(X) |
| and(X1, active(X2)) → and(X1, X2) | active(if(true, X, Y)) → mark(X) |
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.
| active#(add(s(X), Y)) → mark#(s(add(X, Y))) |
Problem 28: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(add(X1, X2)) | → | active#(add(mark(X1), X2)) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
There are no SCCs!
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| first#(active(X1), X2) | → | first#(X1, X2) | | first#(mark(X1), X2) | → | first#(X1, X2) |
| first#(X1, mark(X2)) | → | first#(X1, X2) | | first#(X1, active(X2)) | → | first#(X1, X2) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| first#(active(X1), X2) | → | first#(X1, X2) | | first#(mark(X1), X2) | → | first#(X1, X2) |
Problem 12: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| first#(X1, active(X2)) | → | first#(X1, X2) | | first#(X1, mark(X2)) | → | first#(X1, X2) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| first#(X1, mark(X2)) | → | first#(X1, X2) | | first#(X1, active(X2)) | → | first#(X1, X2) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| from#(active(X)) | → | from#(X) | | from#(mark(X)) | → | from#(X) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| from#(active(X)) | → | from#(X) | | from#(mark(X)) | → | from#(X) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| add#(active(X1), X2) | → | add#(X1, X2) | | add#(X1, mark(X2)) | → | add#(X1, X2) |
| add#(X1, active(X2)) | → | add#(X1, X2) | | add#(mark(X1), X2) | → | add#(X1, X2) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| add#(active(X1), X2) | → | add#(X1, X2) | | add#(mark(X1), X2) | → | add#(X1, X2) |
Problem 13: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| add#(X1, mark(X2)) | → | add#(X1, X2) | | add#(X1, active(X2)) | → | add#(X1, X2) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| add#(X1, mark(X2)) | → | add#(X1, X2) | | add#(X1, active(X2)) | → | add#(X1, X2) |
Problem 8: 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(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
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 14: 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(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
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 15: 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(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- active(x): 2x
- add(x,y): 0
- and(x,y): 0
- cons(x,y): 0
- false: 0
- first(x,y): 0
- from(x): 0
- if(x,y,z): 0
- if#(x,y,z): z + 1
- mark(x): x + 1
- nil: 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 17: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| if#(X1, X2, active(X3)) | → | if#(X1, X2, X3) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- active(x): x + 2
- add(x,y): 0
- and(x,y): 0
- cons(x,y): 0
- false: 0
- first(x,y): 0
- from(x): 0
- if(x,y,z): 0
- if#(x,y,z): z + y + x
- mark(x): 0
- nil: 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 9: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| s#(mark(X)) | → | s#(X) | | s#(active(X)) | → | s#(X) |
Rewrite Rules
| active(and(true, X)) | → | mark(X) | | active(and(false, Y)) | → | mark(false) |
| active(if(true, X, Y)) | → | mark(X) | | active(if(false, X, Y)) | → | mark(Y) |
| active(add(0, X)) | → | mark(X) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(true) | → | active(true) | | mark(false) | → | active(false) |
| mark(if(X1, X2, X3)) | → | active(if(mark(X1), X2, X3)) | | mark(add(X1, X2)) | → | active(add(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(first(X1, X2)) | → | active(first(mark(X1), mark(X2))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(from(X)) | → | active(from(X)) |
| and(mark(X1), X2) | → | and(X1, X2) | | and(X1, mark(X2)) | → | and(X1, X2) |
| and(active(X1), X2) | → | and(X1, X2) | | and(X1, active(X2)) | → | and(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) |
| add(mark(X1), X2) | → | add(X1, X2) | | add(X1, mark(X2)) | → | add(X1, X2) |
| add(active(X1), X2) | → | add(X1, X2) | | add(X1, active(X2)) | → | add(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| first(mark(X1), X2) | → | first(X1, X2) | | first(X1, mark(X2)) | → | first(X1, X2) |
| first(active(X1), X2) | → | first(X1, X2) | | first(X1, active(X2)) | → | first(X1, X2) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, first, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| s#(mark(X)) | → | s#(X) | | s#(active(X)) | → | s#(X) |