YES
The TRS could be proven terminating. The proof took 2956 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (912ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor SubtermCriterion (0ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| – Problem 5 was processed with processor SubtermCriterion (0ms).
| – Problem 6 was processed with processor SubtermCriterion (1ms).
| – Problem 7 was processed with processor SubtermCriterion (0ms).
| – Problem 8 was processed with processor SubtermCriterion (1ms).
| – Problem 9 was processed with processor SubtermCriterion (0ms).
| | – Problem 12 was processed with processor SubtermCriterion (0ms).
| – Problem 10 was processed with processor SubtermCriterion (0ms).
| – Problem 11 was processed with processor PolynomialLinearRange4iUR (1273ms).
| | – Problem 13 was processed with processor PolynomialLinearRange4iUR (646ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| proper#(cons(X1, X2)) | → | proper#(X1) | | top#(ok(X)) | → | top#(active(X)) |
| cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) | | proper#(and(X1, X2)) | → | and#(proper(X1), proper(X2)) |
| from#(ok(X)) | → | from#(X) | | active#(first(s(X), cons(Y, Z))) | → | cons#(Y, first(X, Z)) |
| active#(if(X1, X2, X3)) | → | active#(X1) | | active#(add(X1, X2)) | → | add#(active(X1), X2) |
| proper#(and(X1, X2)) | → | proper#(X2) | | first#(mark(X1), X2) | → | first#(X1, X2) |
| top#(mark(X)) | → | proper#(X) | | proper#(from(X)) | → | proper#(X) |
| proper#(add(X1, X2)) | → | proper#(X2) | | active#(first(X1, X2)) | → | active#(X2) |
| top#(mark(X)) | → | top#(proper(X)) | | proper#(cons(X1, X2)) | → | proper#(X2) |
| proper#(first(X1, X2)) | → | first#(proper(X1), proper(X2)) | | proper#(add(X1, X2)) | → | proper#(X1) |
| add#(mark(X1), X2) | → | add#(X1, X2) | | and#(mark(X1), X2) | → | and#(X1, X2) |
| active#(first(X1, X2)) | → | active#(X1) | | proper#(first(X1, X2)) | → | proper#(X2) |
| active#(from(X)) | → | s#(X) | | proper#(s(X)) | → | proper#(X) |
| active#(add(s(X), Y)) | → | add#(X, Y) | | if#(mark(X1), X2, X3) | → | if#(X1, X2, X3) |
| proper#(add(X1, X2)) | → | add#(proper(X1), proper(X2)) | | active#(first(X1, X2)) | → | first#(X1, active(X2)) |
| and#(ok(X1), ok(X2)) | → | and#(X1, X2) | | add#(ok(X1), ok(X2)) | → | add#(X1, X2) |
| proper#(and(X1, X2)) | → | proper#(X1) | | top#(ok(X)) | → | active#(X) |
| active#(first(s(X), cons(Y, Z))) | → | first#(X, Z) | | active#(and(X1, X2)) | → | and#(active(X1), X2) |
| active#(add(s(X), Y)) | → | s#(add(X, Y)) | | active#(from(X)) | → | cons#(X, from(s(X))) |
| proper#(from(X)) | → | from#(proper(X)) | | if#(ok(X1), ok(X2), ok(X3)) | → | if#(X1, X2, X3) |
| first#(X1, mark(X2)) | → | first#(X1, X2) | | active#(add(X1, X2)) | → | active#(X1) |
| proper#(if(X1, X2, X3)) | → | proper#(X1) | | proper#(if(X1, X2, X3)) | → | proper#(X2) |
| s#(ok(X)) | → | s#(X) | | first#(ok(X1), ok(X2)) | → | first#(X1, X2) |
| active#(first(X1, X2)) | → | first#(active(X1), X2) | | proper#(cons(X1, X2)) | → | cons#(proper(X1), proper(X2)) |
| proper#(if(X1, X2, X3)) | → | proper#(X3) | | proper#(s(X)) | → | s#(proper(X)) |
| proper#(first(X1, X2)) | → | proper#(X1) | | active#(if(X1, X2, X3)) | → | if#(active(X1), X2, X3) |
| active#(and(X1, X2)) | → | active#(X1) | | proper#(if(X1, X2, X3)) | → | if#(proper(X1), proper(X2), proper(X3)) |
| 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)))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(add(X1, X2)) | → | add(active(X1), X2) |
| active(first(X1, X2)) | → | first(active(X1), X2) | | active(first(X1, X2)) | → | first(X1, active(X2)) |
| and(mark(X1), X2) | → | mark(and(X1, X2)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| add(mark(X1), X2) | → | mark(add(X1, X2)) | | first(mark(X1), X2) | → | mark(first(X1, X2)) |
| first(X1, mark(X2)) | → | mark(first(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(true) | → | ok(true) | | proper(false) | → | ok(false) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(add(X1, X2)) | → | add(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(first(X1, X2)) | → | first(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| add(ok(X1), ok(X2)) | → | ok(add(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| first(ok(X1), ok(X2)) | → | ok(first(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| from(ok(X)) | → | ok(from(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, cons, nil, top
Strategy
The following SCCs where found
| active#(first(X1, X2)) → active#(X2) | active#(if(X1, X2, X3)) → active#(X1) |
| active#(add(X1, X2)) → active#(X1) | active#(and(X1, X2)) → active#(X1) |
| active#(first(X1, X2)) → active#(X1) |
| add#(mark(X1), X2) → add#(X1, X2) | add#(ok(X1), ok(X2)) → add#(X1, X2) |
| proper#(cons(X1, X2)) → proper#(X1) | proper#(if(X1, X2, X3)) → proper#(X1) |
| proper#(cons(X1, X2)) → proper#(X2) | proper#(if(X1, X2, X3)) → proper#(X2) |
| proper#(add(X1, X2)) → proper#(X1) | proper#(and(X1, X2)) → proper#(X1) |
| proper#(first(X1, X2)) → proper#(X2) | proper#(s(X)) → proper#(X) |
| proper#(and(X1, X2)) → proper#(X2) | proper#(first(X1, X2)) → proper#(X1) |
| proper#(if(X1, X2, X3)) → proper#(X3) | proper#(from(X)) → proper#(X) |
| proper#(add(X1, X2)) → proper#(X2) |
| cons#(ok(X1), ok(X2)) → cons#(X1, X2) |
| if#(mark(X1), X2, X3) → if#(X1, X2, X3) | if#(ok(X1), ok(X2), ok(X3)) → if#(X1, X2, X3) |
| and#(ok(X1), ok(X2)) → and#(X1, X2) | and#(mark(X1), X2) → and#(X1, X2) |
| top#(mark(X)) → top#(proper(X)) | top#(ok(X)) → top#(active(X)) |
| first#(ok(X1), ok(X2)) → first#(X1, X2) | first#(mark(X1), X2) → first#(X1, X2) |
| first#(X1, mark(X2)) → first#(X1, X2) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| and#(ok(X1), ok(X2)) | → | and#(X1, X2) | | and#(mark(X1), 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)))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(add(X1, X2)) | → | add(active(X1), X2) |
| active(first(X1, X2)) | → | first(active(X1), X2) | | active(first(X1, X2)) | → | first(X1, active(X2)) |
| and(mark(X1), X2) | → | mark(and(X1, X2)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| add(mark(X1), X2) | → | mark(add(X1, X2)) | | first(mark(X1), X2) | → | mark(first(X1, X2)) |
| first(X1, mark(X2)) | → | mark(first(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(true) | → | ok(true) | | proper(false) | → | ok(false) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(add(X1, X2)) | → | add(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(first(X1, X2)) | → | first(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| add(ok(X1), ok(X2)) | → | ok(add(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| first(ok(X1), ok(X2)) | → | ok(first(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| from(ok(X)) | → | ok(from(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| and#(ok(X1), ok(X2)) | → | and#(X1, X2) | | and#(mark(X1), X2) | → | and#(X1, X2) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
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)))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(add(X1, X2)) | → | add(active(X1), X2) |
| active(first(X1, X2)) | → | first(active(X1), X2) | | active(first(X1, X2)) | → | first(X1, active(X2)) |
| and(mark(X1), X2) | → | mark(and(X1, X2)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| add(mark(X1), X2) | → | mark(add(X1, X2)) | | first(mark(X1), X2) | → | mark(first(X1, X2)) |
| first(X1, mark(X2)) | → | mark(first(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(true) | → | ok(true) | | proper(false) | → | ok(false) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(add(X1, X2)) | → | add(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(first(X1, X2)) | → | first(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| add(ok(X1), ok(X2)) | → | ok(add(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| first(ok(X1), ok(X2)) | → | ok(first(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| from(ok(X)) | → | ok(from(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| add#(mark(X1), X2) | → | add#(X1, X2) | | add#(ok(X1), ok(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)))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(add(X1, X2)) | → | add(active(X1), X2) |
| active(first(X1, X2)) | → | first(active(X1), X2) | | active(first(X1, X2)) | → | first(X1, active(X2)) |
| and(mark(X1), X2) | → | mark(and(X1, X2)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| add(mark(X1), X2) | → | mark(add(X1, X2)) | | first(mark(X1), X2) | → | mark(first(X1, X2)) |
| first(X1, mark(X2)) | → | mark(first(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(true) | → | ok(true) | | proper(false) | → | ok(false) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(add(X1, X2)) | → | add(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(first(X1, X2)) | → | first(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| add(ok(X1), ok(X2)) | → | ok(add(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| first(ok(X1), ok(X2)) | → | ok(first(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| from(ok(X)) | → | ok(from(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| add#(mark(X1), X2) | → | add#(X1, X2) | | add#(ok(X1), ok(X2)) | → | add#(X1, X2) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| if#(mark(X1), X2, X3) | → | if#(X1, X2, X3) | | if#(ok(X1), ok(X2), ok(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)))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(add(X1, X2)) | → | add(active(X1), X2) |
| active(first(X1, X2)) | → | first(active(X1), X2) | | active(first(X1, X2)) | → | first(X1, active(X2)) |
| and(mark(X1), X2) | → | mark(and(X1, X2)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| add(mark(X1), X2) | → | mark(add(X1, X2)) | | first(mark(X1), X2) | → | mark(first(X1, X2)) |
| first(X1, mark(X2)) | → | mark(first(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(true) | → | ok(true) | | proper(false) | → | ok(false) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(add(X1, X2)) | → | add(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(first(X1, X2)) | → | first(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| add(ok(X1), ok(X2)) | → | ok(add(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| first(ok(X1), ok(X2)) | → | ok(first(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| from(ok(X)) | → | ok(from(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| if#(mark(X1), X2, X3) | → | if#(X1, X2, X3) | | if#(ok(X1), ok(X2), ok(X3)) | → | if#(X1, X2, X3) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| active#(first(X1, X2)) | → | active#(X2) | | active#(if(X1, X2, X3)) | → | active#(X1) |
| active#(add(X1, X2)) | → | active#(X1) | | active#(and(X1, X2)) | → | active#(X1) |
| active#(first(X1, X2)) | → | active#(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)))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(add(X1, X2)) | → | add(active(X1), X2) |
| active(first(X1, X2)) | → | first(active(X1), X2) | | active(first(X1, X2)) | → | first(X1, active(X2)) |
| and(mark(X1), X2) | → | mark(and(X1, X2)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| add(mark(X1), X2) | → | mark(add(X1, X2)) | | first(mark(X1), X2) | → | mark(first(X1, X2)) |
| first(X1, mark(X2)) | → | mark(first(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(true) | → | ok(true) | | proper(false) | → | ok(false) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(add(X1, X2)) | → | add(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(first(X1, X2)) | → | first(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| add(ok(X1), ok(X2)) | → | ok(add(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| first(ok(X1), ok(X2)) | → | ok(first(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| from(ok(X)) | → | ok(from(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| active#(first(X1, X2)) | → | active#(X2) | | active#(if(X1, X2, X3)) | → | active#(X1) |
| active#(add(X1, X2)) | → | active#(X1) | | active#(and(X1, X2)) | → | active#(X1) |
| active#(first(X1, X2)) | → | active#(X1) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| proper#(cons(X1, X2)) | → | proper#(X1) | | proper#(if(X1, X2, X3)) | → | proper#(X1) |
| proper#(cons(X1, X2)) | → | proper#(X2) | | proper#(if(X1, X2, X3)) | → | proper#(X2) |
| proper#(add(X1, X2)) | → | proper#(X1) | | proper#(and(X1, X2)) | → | proper#(X1) |
| proper#(first(X1, X2)) | → | proper#(X2) | | proper#(s(X)) | → | proper#(X) |
| proper#(and(X1, X2)) | → | proper#(X2) | | proper#(if(X1, X2, X3)) | → | proper#(X3) |
| proper#(first(X1, X2)) | → | proper#(X1) | | proper#(from(X)) | → | proper#(X) |
| proper#(add(X1, X2)) | → | proper#(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)))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(add(X1, X2)) | → | add(active(X1), X2) |
| active(first(X1, X2)) | → | first(active(X1), X2) | | active(first(X1, X2)) | → | first(X1, active(X2)) |
| and(mark(X1), X2) | → | mark(and(X1, X2)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| add(mark(X1), X2) | → | mark(add(X1, X2)) | | first(mark(X1), X2) | → | mark(first(X1, X2)) |
| first(X1, mark(X2)) | → | mark(first(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(true) | → | ok(true) | | proper(false) | → | ok(false) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(add(X1, X2)) | → | add(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(first(X1, X2)) | → | first(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| add(ok(X1), ok(X2)) | → | ok(add(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| first(ok(X1), ok(X2)) | → | ok(first(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| from(ok(X)) | → | ok(from(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| proper#(cons(X1, X2)) | → | proper#(X1) | | proper#(if(X1, X2, X3)) | → | proper#(X1) |
| proper#(cons(X1, X2)) | → | proper#(X2) | | proper#(if(X1, X2, X3)) | → | proper#(X2) |
| proper#(add(X1, X2)) | → | proper#(X1) | | proper#(and(X1, X2)) | → | proper#(X1) |
| proper#(first(X1, X2)) | → | proper#(X2) | | proper#(s(X)) | → | proper#(X) |
| proper#(and(X1, X2)) | → | proper#(X2) | | proper#(if(X1, X2, X3)) | → | proper#(X3) |
| proper#(first(X1, X2)) | → | proper#(X1) | | proper#(from(X)) | → | proper#(X) |
| proper#(add(X1, X2)) | → | proper#(X2) |
Problem 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
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)))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(add(X1, X2)) | → | add(active(X1), X2) |
| active(first(X1, X2)) | → | first(active(X1), X2) | | active(first(X1, X2)) | → | first(X1, active(X2)) |
| and(mark(X1), X2) | → | mark(and(X1, X2)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| add(mark(X1), X2) | → | mark(add(X1, X2)) | | first(mark(X1), X2) | → | mark(first(X1, X2)) |
| first(X1, mark(X2)) | → | mark(first(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(true) | → | ok(true) | | proper(false) | → | ok(false) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(add(X1, X2)) | → | add(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(first(X1, X2)) | → | first(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| add(ok(X1), ok(X2)) | → | ok(add(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| first(ok(X1), ok(X2)) | → | ok(first(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| from(ok(X)) | → | ok(from(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
Problem 9: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| first#(ok(X1), ok(X2)) | → | first#(X1, X2) | | first#(mark(X1), 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)))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(add(X1, X2)) | → | add(active(X1), X2) |
| active(first(X1, X2)) | → | first(active(X1), X2) | | active(first(X1, X2)) | → | first(X1, active(X2)) |
| and(mark(X1), X2) | → | mark(and(X1, X2)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| add(mark(X1), X2) | → | mark(add(X1, X2)) | | first(mark(X1), X2) | → | mark(first(X1, X2)) |
| first(X1, mark(X2)) | → | mark(first(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(true) | → | ok(true) | | proper(false) | → | ok(false) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(add(X1, X2)) | → | add(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(first(X1, X2)) | → | first(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| add(ok(X1), ok(X2)) | → | ok(add(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| first(ok(X1), ok(X2)) | → | ok(first(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| from(ok(X)) | → | ok(from(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| first#(ok(X1), ok(X2)) | → | first#(X1, X2) | | first#(mark(X1), X2) | → | first#(X1, X2) |
Problem 12: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| 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)))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(add(X1, X2)) | → | add(active(X1), X2) |
| active(first(X1, X2)) | → | first(active(X1), X2) | | active(first(X1, X2)) | → | first(X1, active(X2)) |
| and(mark(X1), X2) | → | mark(and(X1, X2)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| add(mark(X1), X2) | → | mark(add(X1, X2)) | | first(mark(X1), X2) | → | mark(first(X1, X2)) |
| first(X1, mark(X2)) | → | mark(first(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(true) | → | ok(true) | | proper(false) | → | ok(false) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(add(X1, X2)) | → | add(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(first(X1, X2)) | → | first(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| add(ok(X1), ok(X2)) | → | ok(add(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| first(ok(X1), ok(X2)) | → | ok(first(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| from(ok(X)) | → | ok(from(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, top, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| first#(X1, mark(X2)) | → | first#(X1, X2) |
Problem 10: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons#(ok(X1), ok(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)))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(add(X1, X2)) | → | add(active(X1), X2) |
| active(first(X1, X2)) | → | first(active(X1), X2) | | active(first(X1, X2)) | → | first(X1, active(X2)) |
| and(mark(X1), X2) | → | mark(and(X1, X2)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| add(mark(X1), X2) | → | mark(add(X1, X2)) | | first(mark(X1), X2) | → | mark(first(X1, X2)) |
| first(X1, mark(X2)) | → | mark(first(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(true) | → | ok(true) | | proper(false) | → | ok(false) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(add(X1, X2)) | → | add(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(first(X1, X2)) | → | first(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| add(ok(X1), ok(X2)) | → | ok(add(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| first(ok(X1), ok(X2)) | → | ok(first(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| from(ok(X)) | → | ok(from(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
Problem 11: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| top#(mark(X)) | → | top#(proper(X)) | | top#(ok(X)) | → | top#(active(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)))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(add(X1, X2)) | → | add(active(X1), X2) |
| active(first(X1, X2)) | → | first(active(X1), X2) | | active(first(X1, X2)) | → | first(X1, active(X2)) |
| and(mark(X1), X2) | → | mark(and(X1, X2)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| add(mark(X1), X2) | → | mark(add(X1, X2)) | | first(mark(X1), X2) | → | mark(first(X1, X2)) |
| first(X1, mark(X2)) | → | mark(first(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(true) | → | ok(true) | | proper(false) | → | ok(false) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(add(X1, X2)) | → | add(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(first(X1, X2)) | → | first(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| add(ok(X1), ok(X2)) | → | ok(add(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| first(ok(X1), ok(X2)) | → | ok(first(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| from(ok(X)) | → | ok(from(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, cons, nil, top
Strategy
Polynomial Interpretation
- 0: 1
- active(x): x
- add(x,y): y + x + 2
- and(x,y): y + x + 1
- cons(x,y): 0
- false: 1
- first(x,y): y + 2x + 1
- from(x): 1
- if(x,y,z): 3z + y + x + 2
- mark(x): x + 1
- nil: 1
- ok(x): x
- proper(x): x
- s(x): 0
- top(x): 0
- top#(x): 2x
- true: 0
Improved Usable rules
| proper(false) | → | ok(false) | | and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(and(false, Y)) | → | mark(false) |
| first(X1, mark(X2)) | → | mark(first(X1, X2)) | | active(first(0, X)) | → | mark(nil) |
| proper(add(X1, X2)) | → | add(proper(X1), proper(X2)) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| add(mark(X1), X2) | → | mark(add(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| active(first(X1, X2)) | → | first(active(X1), X2) | | proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) |
| active(add(X1, X2)) | → | add(active(X1), X2) | | proper(s(X)) | → | s(proper(X)) |
| active(and(true, X)) | → | mark(X) | | active(from(X)) | → | mark(cons(X, from(s(X)))) |
| first(ok(X1), ok(X2)) | → | ok(first(X1, X2)) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| proper(first(X1, X2)) | → | first(proper(X1), proper(X2)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) | | first(mark(X1), X2) | → | mark(first(X1, X2)) |
| s(ok(X)) | → | ok(s(X)) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| from(ok(X)) | → | ok(from(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| active(if(false, X, Y)) | → | mark(Y) | | proper(true) | → | ok(true) |
| add(ok(X1), ok(X2)) | → | ok(add(X1, X2)) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | active(add(0, X)) | → | mark(X) |
| and(mark(X1), X2) | → | mark(and(X1, X2)) | | proper(0) | → | ok(0) |
| active(if(true, X, Y)) | → | mark(X) | | proper(from(X)) | → | from(proper(X)) |
| active(first(X1, X2)) | → | first(X1, active(X2)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| top#(mark(X)) | → | top#(proper(X)) |
Problem 13: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| top#(ok(X)) | → | top#(active(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)))) | | active(and(X1, X2)) | → | and(active(X1), X2) |
| active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) | | active(add(X1, X2)) | → | add(active(X1), X2) |
| active(first(X1, X2)) | → | first(active(X1), X2) | | active(first(X1, X2)) | → | first(X1, active(X2)) |
| and(mark(X1), X2) | → | mark(and(X1, X2)) | | if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
| add(mark(X1), X2) | → | mark(add(X1, X2)) | | first(mark(X1), X2) | → | mark(first(X1, X2)) |
| first(X1, mark(X2)) | → | mark(first(X1, X2)) | | proper(and(X1, X2)) | → | and(proper(X1), proper(X2)) |
| proper(true) | → | ok(true) | | proper(false) | → | ok(false) |
| proper(if(X1, X2, X3)) | → | if(proper(X1), proper(X2), proper(X3)) | | proper(add(X1, X2)) | → | add(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(first(X1, X2)) | → | first(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) | | if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) |
| add(ok(X1), ok(X2)) | → | ok(add(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| first(ok(X1), ok(X2)) | → | ok(first(X1, X2)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| from(ok(X)) | → | ok(from(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: true, mark, from, add, and, 0, s, if, active, false, ok, proper, first, top, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- active(x): x + 2
- add(x,y): x
- and(x,y): y
- cons(x,y): 0
- false: 3
- first(x,y): x
- from(x): 0
- if(x,y,z): z
- mark(x): 0
- nil: 2
- ok(x): 2x + 3
- proper(x): 0
- s(x): 0
- top(x): 0
- top#(x): x
- true: 1
Improved Usable rules
| if(ok(X1), ok(X2), ok(X3)) | → | ok(if(X1, X2, X3)) | | and(ok(X1), ok(X2)) | → | ok(and(X1, X2)) |
| first(mark(X1), X2) | → | mark(first(X1, X2)) | | active(if(X1, X2, X3)) | → | if(active(X1), X2, X3) |
| active(and(false, Y)) | → | mark(false) | | active(add(s(X), Y)) | → | mark(s(add(X, Y))) |
| active(first(0, X)) | → | mark(nil) | | first(X1, mark(X2)) | → | mark(first(X1, X2)) |
| active(if(false, X, Y)) | → | mark(Y) | | active(first(s(X), cons(Y, Z))) | → | mark(cons(Y, first(X, Z))) |
| add(ok(X1), ok(X2)) | → | ok(add(X1, X2)) | | add(mark(X1), X2) | → | mark(add(X1, X2)) |
| active(first(X1, X2)) | → | first(active(X1), X2) | | active(add(X1, X2)) | → | add(active(X1), X2) |
| active(add(0, X)) | → | mark(X) | | and(mark(X1), X2) | → | mark(and(X1, X2)) |
| active(and(true, X)) | → | mark(X) | | active(from(X)) | → | mark(cons(X, from(s(X)))) |
| first(ok(X1), ok(X2)) | → | ok(first(X1, X2)) | | active(if(true, X, Y)) | → | mark(X) |
| active(and(X1, X2)) | → | and(active(X1), X2) | | active(first(X1, X2)) | → | first(X1, active(X2)) |
| if(mark(X1), X2, X3) | → | mark(if(X1, X2, X3)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| top#(ok(X)) | → | top#(active(X)) |