TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60246 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (13732ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (7ms), PolynomialLinearRange4iUR (1666ms), DependencyGraph (6ms), PolynomialLinearRange4iUR (2501ms), DependencyGraph (7ms), PolynomialLinearRange8NegiUR (7500ms), DependencyGraph (78ms), ReductionPairSAT (23640ms), DependencyGraph (6ms), ReductionPairSAT (9957ms)].
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor SubtermCriterion (2ms).
| – Problem 5 was processed with processor SubtermCriterion (3ms).
| – Problem 6 was processed with processor SubtermCriterion (1ms).
| | – Problem 17 was processed with processor PolynomialLinearRange4iUR (74ms).
| – Problem 7 was processed with processor SubtermCriterion (2ms).
| | – Problem 18 was processed with processor ReductionPairSAT (70ms).
| – Problem 8 was processed with processor SubtermCriterion (1ms).
| – Problem 9 was processed with processor SubtermCriterion (3ms).
| – Problem 10 was processed with processor SubtermCriterion (1ms).
| – Problem 11 was processed with processor SubtermCriterion (1ms).
| – Problem 12 was processed with processor SubtermCriterion (3ms).
| | – Problem 19 was processed with processor PolynomialLinearRange4iUR (108ms).
| – Problem 13 was processed with processor SubtermCriterion (2ms).
| | – Problem 20 was processed with processor ReductionPairSAT (74ms).
| – Problem 14 was processed with processor SubtermCriterion (2ms).
| | – Problem 21 was processed with processor ReductionPairSAT (49ms).
| – Problem 15 was processed with processor SubtermCriterion (2ms).
| – Problem 16 was processed with processor SubtermCriterion (5ms).
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| top#(mark(X)) | → | top#(proper(X)) | | top#(ok(X)) | → | top#(active(X)) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) | | active(2ndsneg(0, Z)) | → | mark(rnil) |
| active(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(negrecip(Y), 2ndspos(N, Z))) | | active(pi(X)) | → | mark(2ndspos(X, from(0))) |
| active(plus(0, Y)) | → | mark(Y) | | active(plus(s(X), Y)) | → | mark(s(plus(X, Y))) |
| active(times(0, Y)) | → | mark(0) | | active(times(s(X), Y)) | → | mark(plus(Y, times(X, Y))) |
| active(square(X)) | → | mark(times(X, X)) | | active(s(X)) | → | s(active(X)) |
| active(posrecip(X)) | → | posrecip(active(X)) | | active(negrecip(X)) | → | negrecip(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(rcons(X1, X2)) | → | rcons(active(X1), X2) |
| active(rcons(X1, X2)) | → | rcons(X1, active(X2)) | | active(from(X)) | → | from(active(X)) |
| active(2ndspos(X1, X2)) | → | 2ndspos(active(X1), X2) | | active(2ndspos(X1, X2)) | → | 2ndspos(X1, active(X2)) |
| active(2ndsneg(X1, X2)) | → | 2ndsneg(active(X1), X2) | | active(2ndsneg(X1, X2)) | → | 2ndsneg(X1, active(X2)) |
| active(pi(X)) | → | pi(active(X)) | | active(plus(X1, X2)) | → | plus(active(X1), X2) |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | | active(times(X1, X2)) | → | times(active(X1), X2) |
| active(times(X1, X2)) | → | times(X1, active(X2)) | | active(square(X)) | → | square(active(X)) |
| s(mark(X)) | → | mark(s(X)) | | posrecip(mark(X)) | → | mark(posrecip(X)) |
| negrecip(mark(X)) | → | mark(negrecip(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| rcons(mark(X1), X2) | → | mark(rcons(X1, X2)) | | rcons(X1, mark(X2)) | → | mark(rcons(X1, X2)) |
| from(mark(X)) | → | mark(from(X)) | | 2ndspos(mark(X1), X2) | → | mark(2ndspos(X1, X2)) |
| 2ndspos(X1, mark(X2)) | → | mark(2ndspos(X1, X2)) | | 2ndsneg(mark(X1), X2) | → | mark(2ndsneg(X1, X2)) |
| 2ndsneg(X1, mark(X2)) | → | mark(2ndsneg(X1, X2)) | | pi(mark(X)) | → | mark(pi(X)) |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) |
| times(mark(X1), X2) | → | mark(times(X1, X2)) | | times(X1, mark(X2)) | → | mark(times(X1, X2)) |
| square(mark(X)) | → | mark(square(X)) | | proper(0) | → | ok(0) |
| proper(s(X)) | → | s(proper(X)) | | proper(posrecip(X)) | → | posrecip(proper(X)) |
| proper(negrecip(X)) | → | negrecip(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(rnil) | → | ok(rnil) |
| proper(rcons(X1, X2)) | → | rcons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(2ndspos(X1, X2)) | → | 2ndspos(proper(X1), proper(X2)) | | proper(2ndsneg(X1, X2)) | → | 2ndsneg(proper(X1), proper(X2)) |
| proper(pi(X)) | → | pi(proper(X)) | | proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) |
| proper(times(X1, X2)) | → | times(proper(X1), proper(X2)) | | proper(square(X)) | → | square(proper(X)) |
| s(ok(X)) | → | ok(s(X)) | | posrecip(ok(X)) | → | ok(posrecip(X)) |
| negrecip(ok(X)) | → | ok(negrecip(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| rcons(ok(X1), ok(X2)) | → | ok(rcons(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| 2ndspos(ok(X1), ok(X2)) | → | ok(2ndspos(X1, X2)) | | 2ndsneg(ok(X1), ok(X2)) | → | ok(2ndsneg(X1, X2)) |
| pi(ok(X)) | → | ok(pi(X)) | | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) |
| times(ok(X1), ok(X2)) | → | ok(times(X1, X2)) | | square(ok(X)) | → | ok(square(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: plus, posrecip, negrecip, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, proper, square, pi, top, nil, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| proper#(2ndsneg(X1, X2)) | → | proper#(X1) | | proper#(cons(X1, X2)) | → | proper#(X1) |
| active#(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | posrecip#(Y) | | proper#(square(X)) | → | proper#(X) |
| active#(pi(X)) | → | from#(0) | | active#(2ndsneg(X1, X2)) | → | active#(X2) |
| active#(times(X1, X2)) | → | times#(X1, active(X2)) | | rcons#(ok(X1), ok(X2)) | → | rcons#(X1, X2) |
| active#(2ndspos(X1, X2)) | → | 2ndspos#(X1, active(X2)) | | top#(mark(X)) | → | proper#(X) |
| active#(posrecip(X)) | → | posrecip#(active(X)) | | 2ndspos#(X1, mark(X2)) | → | 2ndspos#(X1, X2) |
| active#(2ndsneg(X1, X2)) | → | 2ndsneg#(X1, active(X2)) | | active#(pi(X)) | → | pi#(active(X)) |
| negrecip#(ok(X)) | → | negrecip#(X) | | rcons#(mark(X1), X2) | → | rcons#(X1, X2) |
| active#(square(X)) | → | times#(X, X) | | times#(mark(X1), X2) | → | times#(X1, X2) |
| negrecip#(mark(X)) | → | negrecip#(X) | | 2ndspos#(mark(X1), X2) | → | 2ndspos#(X1, X2) |
| proper#(2ndsneg(X1, X2)) | → | 2ndsneg#(proper(X1), proper(X2)) | | proper#(2ndspos(X1, X2)) | → | proper#(X1) |
| proper#(2ndsneg(X1, X2)) | → | proper#(X2) | | active#(negrecip(X)) | → | active#(X) |
| active#(plus(X1, X2)) | → | active#(X2) | | active#(2ndspos(X1, X2)) | → | 2ndspos#(active(X1), X2) |
| plus#(mark(X1), X2) | → | plus#(X1, X2) | | active#(rcons(X1, X2)) | → | rcons#(X1, active(X2)) |
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | pi#(ok(X)) | → | pi#(X) |
| active#(posrecip(X)) | → | active#(X) | | 2ndsneg#(ok(X1), ok(X2)) | → | 2ndsneg#(X1, X2) |
| from#(mark(X)) | → | from#(X) | | proper#(pi(X)) | → | pi#(proper(X)) |
| top#(ok(X)) | → | active#(X) | | proper#(posrecip(X)) | → | proper#(X) |
| times#(ok(X1), ok(X2)) | → | times#(X1, X2) | | square#(mark(X)) | → | square#(X) |
| proper#(from(X)) | → | from#(proper(X)) | | times#(X1, mark(X2)) | → | times#(X1, X2) |
| active#(pi(X)) | → | 2ndspos#(X, from(0)) | | proper#(rcons(X1, X2)) | → | proper#(X1) |
| active#(plus(s(X), Y)) | → | plus#(X, Y) | | plus#(ok(X1), ok(X2)) | → | plus#(X1, X2) |
| posrecip#(mark(X)) | → | posrecip#(X) | | active#(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | negrecip#(Y) |
| proper#(2ndspos(X1, X2)) | → | 2ndspos#(proper(X1), proper(X2)) | | active#(times(s(X), Y)) | → | plus#(Y, times(X, Y)) |
| proper#(negrecip(X)) | → | proper#(X) | | active#(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | 2ndspos#(N, Z) |
| active#(s(X)) | → | s#(active(X)) | | proper#(posrecip(X)) | → | posrecip#(proper(X)) |
| s#(ok(X)) | → | s#(X) | | 2ndsneg#(X1, mark(X2)) | → | 2ndsneg#(X1, X2) |
| proper#(s(X)) | → | s#(proper(X)) | | active#(2ndsneg(X1, X2)) | → | active#(X1) |
| rcons#(X1, mark(X2)) | → | rcons#(X1, X2) | | active#(from(X)) | → | from#(s(X)) |
| active#(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | rcons#(posrecip(Y), 2ndsneg(N, Z)) | | top#(ok(X)) | → | top#(active(X)) |
| active#(square(X)) | → | square#(active(X)) | | active#(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | rcons#(negrecip(Y), 2ndspos(N, Z)) |
| cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) | | active#(rcons(X1, X2)) | → | rcons#(active(X1), X2) |
| proper#(times(X1, X2)) | → | proper#(X2) | | proper#(negrecip(X)) | → | negrecip#(proper(X)) |
| from#(ok(X)) | → | from#(X) | | proper#(2ndspos(X1, X2)) | → | proper#(X2) |
| active#(cons(X1, X2)) | → | cons#(active(X1), X2) | | active#(rcons(X1, X2)) | → | active#(X2) |
| pi#(mark(X)) | → | pi#(X) | | active#(2ndspos(X1, X2)) | → | active#(X1) |
| plus#(X1, mark(X2)) | → | plus#(X1, X2) | | posrecip#(ok(X)) | → | posrecip#(X) |
| proper#(plus(X1, X2)) | → | proper#(X1) | | active#(rcons(X1, X2)) | → | active#(X1) |
| proper#(from(X)) | → | proper#(X) | | proper#(plus(X1, X2)) | → | plus#(proper(X1), proper(X2)) |
| top#(mark(X)) | → | top#(proper(X)) | | proper#(cons(X1, X2)) | → | proper#(X2) |
| active#(2ndsneg(X1, X2)) | → | 2ndsneg#(active(X1), X2) | | active#(from(X)) | → | s#(X) |
| proper#(rcons(X1, X2)) | → | rcons#(proper(X1), proper(X2)) | | proper#(s(X)) | → | proper#(X) |
| proper#(square(X)) | → | square#(proper(X)) | | active#(plus(X1, X2)) | → | active#(X1) |
| proper#(times(X1, X2)) | → | times#(proper(X1), proper(X2)) | | active#(times(X1, X2)) | → | active#(X2) |
| active#(plus(s(X), Y)) | → | s#(plus(X, Y)) | | active#(cons(X1, X2)) | → | active#(X1) |
| active#(from(X)) | → | from#(active(X)) | | active#(pi(X)) | → | active#(X) |
| active#(times(s(X), Y)) | → | times#(X, Y) | | active#(times(X1, X2)) | → | times#(active(X1), X2) |
| active#(from(X)) | → | cons#(X, from(s(X))) | | 2ndsneg#(mark(X1), X2) | → | 2ndsneg#(X1, X2) |
| proper#(pi(X)) | → | proper#(X) | | proper#(plus(X1, X2)) | → | proper#(X2) |
| active#(from(X)) | → | active#(X) | | active#(negrecip(X)) | → | negrecip#(active(X)) |
| active#(2ndspos(X1, X2)) | → | active#(X2) | | proper#(rcons(X1, X2)) | → | proper#(X2) |
| active#(times(X1, X2)) | → | active#(X1) | | s#(mark(X)) | → | s#(X) |
| active#(plus(X1, X2)) | → | plus#(X1, active(X2)) | | square#(ok(X)) | → | square#(X) |
| proper#(times(X1, X2)) | → | proper#(X1) | | proper#(cons(X1, X2)) | → | cons#(proper(X1), proper(X2)) |
| active#(square(X)) | → | active#(X) | | active#(s(X)) | → | active#(X) |
| active#(plus(X1, X2)) | → | plus#(active(X1), X2) | | 2ndspos#(ok(X1), ok(X2)) | → | 2ndspos#(X1, X2) |
| active#(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | 2ndsneg#(N, Z) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) | | active(2ndsneg(0, Z)) | → | mark(rnil) |
| active(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(negrecip(Y), 2ndspos(N, Z))) | | active(pi(X)) | → | mark(2ndspos(X, from(0))) |
| active(plus(0, Y)) | → | mark(Y) | | active(plus(s(X), Y)) | → | mark(s(plus(X, Y))) |
| active(times(0, Y)) | → | mark(0) | | active(times(s(X), Y)) | → | mark(plus(Y, times(X, Y))) |
| active(square(X)) | → | mark(times(X, X)) | | active(s(X)) | → | s(active(X)) |
| active(posrecip(X)) | → | posrecip(active(X)) | | active(negrecip(X)) | → | negrecip(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(rcons(X1, X2)) | → | rcons(active(X1), X2) |
| active(rcons(X1, X2)) | → | rcons(X1, active(X2)) | | active(from(X)) | → | from(active(X)) |
| active(2ndspos(X1, X2)) | → | 2ndspos(active(X1), X2) | | active(2ndspos(X1, X2)) | → | 2ndspos(X1, active(X2)) |
| active(2ndsneg(X1, X2)) | → | 2ndsneg(active(X1), X2) | | active(2ndsneg(X1, X2)) | → | 2ndsneg(X1, active(X2)) |
| active(pi(X)) | → | pi(active(X)) | | active(plus(X1, X2)) | → | plus(active(X1), X2) |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | | active(times(X1, X2)) | → | times(active(X1), X2) |
| active(times(X1, X2)) | → | times(X1, active(X2)) | | active(square(X)) | → | square(active(X)) |
| s(mark(X)) | → | mark(s(X)) | | posrecip(mark(X)) | → | mark(posrecip(X)) |
| negrecip(mark(X)) | → | mark(negrecip(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| rcons(mark(X1), X2) | → | mark(rcons(X1, X2)) | | rcons(X1, mark(X2)) | → | mark(rcons(X1, X2)) |
| from(mark(X)) | → | mark(from(X)) | | 2ndspos(mark(X1), X2) | → | mark(2ndspos(X1, X2)) |
| 2ndspos(X1, mark(X2)) | → | mark(2ndspos(X1, X2)) | | 2ndsneg(mark(X1), X2) | → | mark(2ndsneg(X1, X2)) |
| 2ndsneg(X1, mark(X2)) | → | mark(2ndsneg(X1, X2)) | | pi(mark(X)) | → | mark(pi(X)) |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) |
| times(mark(X1), X2) | → | mark(times(X1, X2)) | | times(X1, mark(X2)) | → | mark(times(X1, X2)) |
| square(mark(X)) | → | mark(square(X)) | | proper(0) | → | ok(0) |
| proper(s(X)) | → | s(proper(X)) | | proper(posrecip(X)) | → | posrecip(proper(X)) |
| proper(negrecip(X)) | → | negrecip(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(rnil) | → | ok(rnil) |
| proper(rcons(X1, X2)) | → | rcons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(2ndspos(X1, X2)) | → | 2ndspos(proper(X1), proper(X2)) | | proper(2ndsneg(X1, X2)) | → | 2ndsneg(proper(X1), proper(X2)) |
| proper(pi(X)) | → | pi(proper(X)) | | proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) |
| proper(times(X1, X2)) | → | times(proper(X1), proper(X2)) | | proper(square(X)) | → | square(proper(X)) |
| s(ok(X)) | → | ok(s(X)) | | posrecip(ok(X)) | → | ok(posrecip(X)) |
| negrecip(ok(X)) | → | ok(negrecip(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| rcons(ok(X1), ok(X2)) | → | ok(rcons(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| 2ndspos(ok(X1), ok(X2)) | → | ok(2ndspos(X1, X2)) | | 2ndsneg(ok(X1), ok(X2)) | → | ok(2ndsneg(X1, X2)) |
| pi(ok(X)) | → | ok(pi(X)) | | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) |
| times(ok(X1), ok(X2)) | → | ok(times(X1, X2)) | | square(ok(X)) | → | ok(square(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: plus, posrecip, negrecip, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, square, proper, pi, cons, nil, top
Strategy
The following SCCs where found
| times#(ok(X1), ok(X2)) → times#(X1, X2) | times#(X1, mark(X2)) → times#(X1, X2) |
| times#(mark(X1), X2) → times#(X1, X2) |
| negrecip#(ok(X)) → negrecip#(X) | negrecip#(mark(X)) → negrecip#(X) |
| s#(mark(X)) → s#(X) | s#(ok(X)) → s#(X) |
| 2ndspos#(mark(X1), X2) → 2ndspos#(X1, X2) | 2ndspos#(X1, mark(X2)) → 2ndspos#(X1, X2) |
| 2ndspos#(ok(X1), ok(X2)) → 2ndspos#(X1, X2) |
| cons#(mark(X1), X2) → cons#(X1, X2) | cons#(ok(X1), ok(X2)) → cons#(X1, X2) |
| plus#(ok(X1), ok(X2)) → plus#(X1, X2) | plus#(X1, mark(X2)) → plus#(X1, X2) |
| plus#(mark(X1), X2) → plus#(X1, X2) |
| square#(ok(X)) → square#(X) | square#(mark(X)) → square#(X) |
| active#(from(X)) → active#(X) | active#(2ndspos(X1, X2)) → active#(X2) |
| active#(2ndsneg(X1, X2)) → active#(X2) | active#(posrecip(X)) → active#(X) |
| active#(pi(X)) → active#(X) | active#(times(X1, X2)) → active#(X1) |
| active#(plus(X1, X2)) → active#(X1) | active#(rcons(X1, X2)) → active#(X2) |
| active#(square(X)) → active#(X) | active#(s(X)) → active#(X) |
| active#(2ndspos(X1, X2)) → active#(X1) | active#(times(X1, X2)) → active#(X2) |
| active#(negrecip(X)) → active#(X) | active#(plus(X1, X2)) → active#(X2) |
| active#(2ndsneg(X1, X2)) → active#(X1) | active#(rcons(X1, X2)) → active#(X1) |
| active#(cons(X1, X2)) → active#(X1) |
| rcons#(ok(X1), ok(X2)) → rcons#(X1, X2) | rcons#(mark(X1), X2) → rcons#(X1, X2) |
| rcons#(X1, mark(X2)) → rcons#(X1, X2) |
| pi#(mark(X)) → pi#(X) | pi#(ok(X)) → pi#(X) |
| proper#(2ndsneg(X1, X2)) → proper#(X1) | proper#(cons(X1, X2)) → proper#(X1) |
| proper#(cons(X1, X2)) → proper#(X2) | proper#(square(X)) → proper#(X) |
| proper#(negrecip(X)) → proper#(X) | proper#(times(X1, X2)) → proper#(X2) |
| proper#(rcons(X1, X2)) → proper#(X2) | proper#(2ndspos(X1, X2)) → proper#(X2) |
| proper#(posrecip(X)) → proper#(X) | proper#(s(X)) → proper#(X) |
| proper#(times(X1, X2)) → proper#(X1) | proper#(2ndspos(X1, X2)) → proper#(X1) |
| proper#(2ndsneg(X1, X2)) → proper#(X2) | proper#(plus(X1, X2)) → proper#(X1) |
| proper#(pi(X)) → proper#(X) | proper#(rcons(X1, X2)) → proper#(X1) |
| proper#(plus(X1, X2)) → proper#(X2) | proper#(from(X)) → proper#(X) |
| posrecip#(mark(X)) → posrecip#(X) | posrecip#(ok(X)) → posrecip#(X) |
| from#(mark(X)) → from#(X) | from#(ok(X)) → from#(X) |
| top#(mark(X)) → top#(proper(X)) | top#(ok(X)) → top#(active(X)) |
| 2ndsneg#(X1, mark(X2)) → 2ndsneg#(X1, X2) | 2ndsneg#(mark(X1), X2) → 2ndsneg#(X1, X2) |
| 2ndsneg#(ok(X1), ok(X2)) → 2ndsneg#(X1, X2) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| pi#(mark(X)) | → | pi#(X) | | pi#(ok(X)) | → | pi#(X) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) | | active(2ndsneg(0, Z)) | → | mark(rnil) |
| active(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(negrecip(Y), 2ndspos(N, Z))) | | active(pi(X)) | → | mark(2ndspos(X, from(0))) |
| active(plus(0, Y)) | → | mark(Y) | | active(plus(s(X), Y)) | → | mark(s(plus(X, Y))) |
| active(times(0, Y)) | → | mark(0) | | active(times(s(X), Y)) | → | mark(plus(Y, times(X, Y))) |
| active(square(X)) | → | mark(times(X, X)) | | active(s(X)) | → | s(active(X)) |
| active(posrecip(X)) | → | posrecip(active(X)) | | active(negrecip(X)) | → | negrecip(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(rcons(X1, X2)) | → | rcons(active(X1), X2) |
| active(rcons(X1, X2)) | → | rcons(X1, active(X2)) | | active(from(X)) | → | from(active(X)) |
| active(2ndspos(X1, X2)) | → | 2ndspos(active(X1), X2) | | active(2ndspos(X1, X2)) | → | 2ndspos(X1, active(X2)) |
| active(2ndsneg(X1, X2)) | → | 2ndsneg(active(X1), X2) | | active(2ndsneg(X1, X2)) | → | 2ndsneg(X1, active(X2)) |
| active(pi(X)) | → | pi(active(X)) | | active(plus(X1, X2)) | → | plus(active(X1), X2) |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | | active(times(X1, X2)) | → | times(active(X1), X2) |
| active(times(X1, X2)) | → | times(X1, active(X2)) | | active(square(X)) | → | square(active(X)) |
| s(mark(X)) | → | mark(s(X)) | | posrecip(mark(X)) | → | mark(posrecip(X)) |
| negrecip(mark(X)) | → | mark(negrecip(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| rcons(mark(X1), X2) | → | mark(rcons(X1, X2)) | | rcons(X1, mark(X2)) | → | mark(rcons(X1, X2)) |
| from(mark(X)) | → | mark(from(X)) | | 2ndspos(mark(X1), X2) | → | mark(2ndspos(X1, X2)) |
| 2ndspos(X1, mark(X2)) | → | mark(2ndspos(X1, X2)) | | 2ndsneg(mark(X1), X2) | → | mark(2ndsneg(X1, X2)) |
| 2ndsneg(X1, mark(X2)) | → | mark(2ndsneg(X1, X2)) | | pi(mark(X)) | → | mark(pi(X)) |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) |
| times(mark(X1), X2) | → | mark(times(X1, X2)) | | times(X1, mark(X2)) | → | mark(times(X1, X2)) |
| square(mark(X)) | → | mark(square(X)) | | proper(0) | → | ok(0) |
| proper(s(X)) | → | s(proper(X)) | | proper(posrecip(X)) | → | posrecip(proper(X)) |
| proper(negrecip(X)) | → | negrecip(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(rnil) | → | ok(rnil) |
| proper(rcons(X1, X2)) | → | rcons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(2ndspos(X1, X2)) | → | 2ndspos(proper(X1), proper(X2)) | | proper(2ndsneg(X1, X2)) | → | 2ndsneg(proper(X1), proper(X2)) |
| proper(pi(X)) | → | pi(proper(X)) | | proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) |
| proper(times(X1, X2)) | → | times(proper(X1), proper(X2)) | | proper(square(X)) | → | square(proper(X)) |
| s(ok(X)) | → | ok(s(X)) | | posrecip(ok(X)) | → | ok(posrecip(X)) |
| negrecip(ok(X)) | → | ok(negrecip(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| rcons(ok(X1), ok(X2)) | → | ok(rcons(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| 2ndspos(ok(X1), ok(X2)) | → | ok(2ndspos(X1, X2)) | | 2ndsneg(ok(X1), ok(X2)) | → | ok(2ndsneg(X1, X2)) |
| pi(ok(X)) | → | ok(pi(X)) | | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) |
| times(ok(X1), ok(X2)) | → | ok(times(X1, X2)) | | square(ok(X)) | → | ok(square(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: plus, posrecip, negrecip, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, square, proper, pi, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| pi#(mark(X)) | → | pi#(X) | | pi#(ok(X)) | → | pi#(X) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| square#(ok(X)) | → | square#(X) | | square#(mark(X)) | → | square#(X) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) | | active(2ndsneg(0, Z)) | → | mark(rnil) |
| active(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(negrecip(Y), 2ndspos(N, Z))) | | active(pi(X)) | → | mark(2ndspos(X, from(0))) |
| active(plus(0, Y)) | → | mark(Y) | | active(plus(s(X), Y)) | → | mark(s(plus(X, Y))) |
| active(times(0, Y)) | → | mark(0) | | active(times(s(X), Y)) | → | mark(plus(Y, times(X, Y))) |
| active(square(X)) | → | mark(times(X, X)) | | active(s(X)) | → | s(active(X)) |
| active(posrecip(X)) | → | posrecip(active(X)) | | active(negrecip(X)) | → | negrecip(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(rcons(X1, X2)) | → | rcons(active(X1), X2) |
| active(rcons(X1, X2)) | → | rcons(X1, active(X2)) | | active(from(X)) | → | from(active(X)) |
| active(2ndspos(X1, X2)) | → | 2ndspos(active(X1), X2) | | active(2ndspos(X1, X2)) | → | 2ndspos(X1, active(X2)) |
| active(2ndsneg(X1, X2)) | → | 2ndsneg(active(X1), X2) | | active(2ndsneg(X1, X2)) | → | 2ndsneg(X1, active(X2)) |
| active(pi(X)) | → | pi(active(X)) | | active(plus(X1, X2)) | → | plus(active(X1), X2) |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | | active(times(X1, X2)) | → | times(active(X1), X2) |
| active(times(X1, X2)) | → | times(X1, active(X2)) | | active(square(X)) | → | square(active(X)) |
| s(mark(X)) | → | mark(s(X)) | | posrecip(mark(X)) | → | mark(posrecip(X)) |
| negrecip(mark(X)) | → | mark(negrecip(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| rcons(mark(X1), X2) | → | mark(rcons(X1, X2)) | | rcons(X1, mark(X2)) | → | mark(rcons(X1, X2)) |
| from(mark(X)) | → | mark(from(X)) | | 2ndspos(mark(X1), X2) | → | mark(2ndspos(X1, X2)) |
| 2ndspos(X1, mark(X2)) | → | mark(2ndspos(X1, X2)) | | 2ndsneg(mark(X1), X2) | → | mark(2ndsneg(X1, X2)) |
| 2ndsneg(X1, mark(X2)) | → | mark(2ndsneg(X1, X2)) | | pi(mark(X)) | → | mark(pi(X)) |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) |
| times(mark(X1), X2) | → | mark(times(X1, X2)) | | times(X1, mark(X2)) | → | mark(times(X1, X2)) |
| square(mark(X)) | → | mark(square(X)) | | proper(0) | → | ok(0) |
| proper(s(X)) | → | s(proper(X)) | | proper(posrecip(X)) | → | posrecip(proper(X)) |
| proper(negrecip(X)) | → | negrecip(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(rnil) | → | ok(rnil) |
| proper(rcons(X1, X2)) | → | rcons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(2ndspos(X1, X2)) | → | 2ndspos(proper(X1), proper(X2)) | | proper(2ndsneg(X1, X2)) | → | 2ndsneg(proper(X1), proper(X2)) |
| proper(pi(X)) | → | pi(proper(X)) | | proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) |
| proper(times(X1, X2)) | → | times(proper(X1), proper(X2)) | | proper(square(X)) | → | square(proper(X)) |
| s(ok(X)) | → | ok(s(X)) | | posrecip(ok(X)) | → | ok(posrecip(X)) |
| negrecip(ok(X)) | → | ok(negrecip(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| rcons(ok(X1), ok(X2)) | → | ok(rcons(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| 2ndspos(ok(X1), ok(X2)) | → | ok(2ndspos(X1, X2)) | | 2ndsneg(ok(X1), ok(X2)) | → | ok(2ndsneg(X1, X2)) |
| pi(ok(X)) | → | ok(pi(X)) | | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) |
| times(ok(X1), ok(X2)) | → | ok(times(X1, X2)) | | square(ok(X)) | → | ok(square(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: plus, posrecip, negrecip, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, square, proper, pi, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| square#(ok(X)) | → | square#(X) | | square#(mark(X)) | → | square#(X) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| posrecip#(mark(X)) | → | posrecip#(X) | | posrecip#(ok(X)) | → | posrecip#(X) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) | | active(2ndsneg(0, Z)) | → | mark(rnil) |
| active(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(negrecip(Y), 2ndspos(N, Z))) | | active(pi(X)) | → | mark(2ndspos(X, from(0))) |
| active(plus(0, Y)) | → | mark(Y) | | active(plus(s(X), Y)) | → | mark(s(plus(X, Y))) |
| active(times(0, Y)) | → | mark(0) | | active(times(s(X), Y)) | → | mark(plus(Y, times(X, Y))) |
| active(square(X)) | → | mark(times(X, X)) | | active(s(X)) | → | s(active(X)) |
| active(posrecip(X)) | → | posrecip(active(X)) | | active(negrecip(X)) | → | negrecip(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(rcons(X1, X2)) | → | rcons(active(X1), X2) |
| active(rcons(X1, X2)) | → | rcons(X1, active(X2)) | | active(from(X)) | → | from(active(X)) |
| active(2ndspos(X1, X2)) | → | 2ndspos(active(X1), X2) | | active(2ndspos(X1, X2)) | → | 2ndspos(X1, active(X2)) |
| active(2ndsneg(X1, X2)) | → | 2ndsneg(active(X1), X2) | | active(2ndsneg(X1, X2)) | → | 2ndsneg(X1, active(X2)) |
| active(pi(X)) | → | pi(active(X)) | | active(plus(X1, X2)) | → | plus(active(X1), X2) |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | | active(times(X1, X2)) | → | times(active(X1), X2) |
| active(times(X1, X2)) | → | times(X1, active(X2)) | | active(square(X)) | → | square(active(X)) |
| s(mark(X)) | → | mark(s(X)) | | posrecip(mark(X)) | → | mark(posrecip(X)) |
| negrecip(mark(X)) | → | mark(negrecip(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| rcons(mark(X1), X2) | → | mark(rcons(X1, X2)) | | rcons(X1, mark(X2)) | → | mark(rcons(X1, X2)) |
| from(mark(X)) | → | mark(from(X)) | | 2ndspos(mark(X1), X2) | → | mark(2ndspos(X1, X2)) |
| 2ndspos(X1, mark(X2)) | → | mark(2ndspos(X1, X2)) | | 2ndsneg(mark(X1), X2) | → | mark(2ndsneg(X1, X2)) |
| 2ndsneg(X1, mark(X2)) | → | mark(2ndsneg(X1, X2)) | | pi(mark(X)) | → | mark(pi(X)) |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) |
| times(mark(X1), X2) | → | mark(times(X1, X2)) | | times(X1, mark(X2)) | → | mark(times(X1, X2)) |
| square(mark(X)) | → | mark(square(X)) | | proper(0) | → | ok(0) |
| proper(s(X)) | → | s(proper(X)) | | proper(posrecip(X)) | → | posrecip(proper(X)) |
| proper(negrecip(X)) | → | negrecip(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(rnil) | → | ok(rnil) |
| proper(rcons(X1, X2)) | → | rcons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(2ndspos(X1, X2)) | → | 2ndspos(proper(X1), proper(X2)) | | proper(2ndsneg(X1, X2)) | → | 2ndsneg(proper(X1), proper(X2)) |
| proper(pi(X)) | → | pi(proper(X)) | | proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) |
| proper(times(X1, X2)) | → | times(proper(X1), proper(X2)) | | proper(square(X)) | → | square(proper(X)) |
| s(ok(X)) | → | ok(s(X)) | | posrecip(ok(X)) | → | ok(posrecip(X)) |
| negrecip(ok(X)) | → | ok(negrecip(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| rcons(ok(X1), ok(X2)) | → | ok(rcons(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| 2ndspos(ok(X1), ok(X2)) | → | ok(2ndspos(X1, X2)) | | 2ndsneg(ok(X1), ok(X2)) | → | ok(2ndsneg(X1, X2)) |
| pi(ok(X)) | → | ok(pi(X)) | | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) |
| times(ok(X1), ok(X2)) | → | ok(times(X1, X2)) | | square(ok(X)) | → | ok(square(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: plus, posrecip, negrecip, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, square, proper, pi, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| posrecip#(mark(X)) | → | posrecip#(X) | | posrecip#(ok(X)) | → | posrecip#(X) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| 2ndspos#(mark(X1), X2) | → | 2ndspos#(X1, X2) | | 2ndspos#(X1, mark(X2)) | → | 2ndspos#(X1, X2) |
| 2ndspos#(ok(X1), ok(X2)) | → | 2ndspos#(X1, X2) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) | | active(2ndsneg(0, Z)) | → | mark(rnil) |
| active(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(negrecip(Y), 2ndspos(N, Z))) | | active(pi(X)) | → | mark(2ndspos(X, from(0))) |
| active(plus(0, Y)) | → | mark(Y) | | active(plus(s(X), Y)) | → | mark(s(plus(X, Y))) |
| active(times(0, Y)) | → | mark(0) | | active(times(s(X), Y)) | → | mark(plus(Y, times(X, Y))) |
| active(square(X)) | → | mark(times(X, X)) | | active(s(X)) | → | s(active(X)) |
| active(posrecip(X)) | → | posrecip(active(X)) | | active(negrecip(X)) | → | negrecip(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(rcons(X1, X2)) | → | rcons(active(X1), X2) |
| active(rcons(X1, X2)) | → | rcons(X1, active(X2)) | | active(from(X)) | → | from(active(X)) |
| active(2ndspos(X1, X2)) | → | 2ndspos(active(X1), X2) | | active(2ndspos(X1, X2)) | → | 2ndspos(X1, active(X2)) |
| active(2ndsneg(X1, X2)) | → | 2ndsneg(active(X1), X2) | | active(2ndsneg(X1, X2)) | → | 2ndsneg(X1, active(X2)) |
| active(pi(X)) | → | pi(active(X)) | | active(plus(X1, X2)) | → | plus(active(X1), X2) |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | | active(times(X1, X2)) | → | times(active(X1), X2) |
| active(times(X1, X2)) | → | times(X1, active(X2)) | | active(square(X)) | → | square(active(X)) |
| s(mark(X)) | → | mark(s(X)) | | posrecip(mark(X)) | → | mark(posrecip(X)) |
| negrecip(mark(X)) | → | mark(negrecip(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| rcons(mark(X1), X2) | → | mark(rcons(X1, X2)) | | rcons(X1, mark(X2)) | → | mark(rcons(X1, X2)) |
| from(mark(X)) | → | mark(from(X)) | | 2ndspos(mark(X1), X2) | → | mark(2ndspos(X1, X2)) |
| 2ndspos(X1, mark(X2)) | → | mark(2ndspos(X1, X2)) | | 2ndsneg(mark(X1), X2) | → | mark(2ndsneg(X1, X2)) |
| 2ndsneg(X1, mark(X2)) | → | mark(2ndsneg(X1, X2)) | | pi(mark(X)) | → | mark(pi(X)) |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) |
| times(mark(X1), X2) | → | mark(times(X1, X2)) | | times(X1, mark(X2)) | → | mark(times(X1, X2)) |
| square(mark(X)) | → | mark(square(X)) | | proper(0) | → | ok(0) |
| proper(s(X)) | → | s(proper(X)) | | proper(posrecip(X)) | → | posrecip(proper(X)) |
| proper(negrecip(X)) | → | negrecip(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(rnil) | → | ok(rnil) |
| proper(rcons(X1, X2)) | → | rcons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(2ndspos(X1, X2)) | → | 2ndspos(proper(X1), proper(X2)) | | proper(2ndsneg(X1, X2)) | → | 2ndsneg(proper(X1), proper(X2)) |
| proper(pi(X)) | → | pi(proper(X)) | | proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) |
| proper(times(X1, X2)) | → | times(proper(X1), proper(X2)) | | proper(square(X)) | → | square(proper(X)) |
| s(ok(X)) | → | ok(s(X)) | | posrecip(ok(X)) | → | ok(posrecip(X)) |
| negrecip(ok(X)) | → | ok(negrecip(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| rcons(ok(X1), ok(X2)) | → | ok(rcons(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| 2ndspos(ok(X1), ok(X2)) | → | ok(2ndspos(X1, X2)) | | 2ndsneg(ok(X1), ok(X2)) | → | ok(2ndsneg(X1, X2)) |
| pi(ok(X)) | → | ok(pi(X)) | | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) |
| times(ok(X1), ok(X2)) | → | ok(times(X1, X2)) | | square(ok(X)) | → | ok(square(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: plus, posrecip, negrecip, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, square, proper, pi, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| 2ndspos#(mark(X1), X2) | → | 2ndspos#(X1, X2) | | 2ndspos#(ok(X1), ok(X2)) | → | 2ndspos#(X1, X2) |
Problem 17: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| 2ndspos#(X1, mark(X2)) | → | 2ndspos#(X1, X2) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) | | active(2ndsneg(0, Z)) | → | mark(rnil) |
| active(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(negrecip(Y), 2ndspos(N, Z))) | | active(pi(X)) | → | mark(2ndspos(X, from(0))) |
| active(plus(0, Y)) | → | mark(Y) | | active(plus(s(X), Y)) | → | mark(s(plus(X, Y))) |
| active(times(0, Y)) | → | mark(0) | | active(times(s(X), Y)) | → | mark(plus(Y, times(X, Y))) |
| active(square(X)) | → | mark(times(X, X)) | | active(s(X)) | → | s(active(X)) |
| active(posrecip(X)) | → | posrecip(active(X)) | | active(negrecip(X)) | → | negrecip(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(rcons(X1, X2)) | → | rcons(active(X1), X2) |
| active(rcons(X1, X2)) | → | rcons(X1, active(X2)) | | active(from(X)) | → | from(active(X)) |
| active(2ndspos(X1, X2)) | → | 2ndspos(active(X1), X2) | | active(2ndspos(X1, X2)) | → | 2ndspos(X1, active(X2)) |
| active(2ndsneg(X1, X2)) | → | 2ndsneg(active(X1), X2) | | active(2ndsneg(X1, X2)) | → | 2ndsneg(X1, active(X2)) |
| active(pi(X)) | → | pi(active(X)) | | active(plus(X1, X2)) | → | plus(active(X1), X2) |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | | active(times(X1, X2)) | → | times(active(X1), X2) |
| active(times(X1, X2)) | → | times(X1, active(X2)) | | active(square(X)) | → | square(active(X)) |
| s(mark(X)) | → | mark(s(X)) | | posrecip(mark(X)) | → | mark(posrecip(X)) |
| negrecip(mark(X)) | → | mark(negrecip(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| rcons(mark(X1), X2) | → | mark(rcons(X1, X2)) | | rcons(X1, mark(X2)) | → | mark(rcons(X1, X2)) |
| from(mark(X)) | → | mark(from(X)) | | 2ndspos(mark(X1), X2) | → | mark(2ndspos(X1, X2)) |
| 2ndspos(X1, mark(X2)) | → | mark(2ndspos(X1, X2)) | | 2ndsneg(mark(X1), X2) | → | mark(2ndsneg(X1, X2)) |
| 2ndsneg(X1, mark(X2)) | → | mark(2ndsneg(X1, X2)) | | pi(mark(X)) | → | mark(pi(X)) |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) |
| times(mark(X1), X2) | → | mark(times(X1, X2)) | | times(X1, mark(X2)) | → | mark(times(X1, X2)) |
| square(mark(X)) | → | mark(square(X)) | | proper(0) | → | ok(0) |
| proper(s(X)) | → | s(proper(X)) | | proper(posrecip(X)) | → | posrecip(proper(X)) |
| proper(negrecip(X)) | → | negrecip(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(rnil) | → | ok(rnil) |
| proper(rcons(X1, X2)) | → | rcons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(2ndspos(X1, X2)) | → | 2ndspos(proper(X1), proper(X2)) | | proper(2ndsneg(X1, X2)) | → | 2ndsneg(proper(X1), proper(X2)) |
| proper(pi(X)) | → | pi(proper(X)) | | proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) |
| proper(times(X1, X2)) | → | times(proper(X1), proper(X2)) | | proper(square(X)) | → | square(proper(X)) |
| s(ok(X)) | → | ok(s(X)) | | posrecip(ok(X)) | → | ok(posrecip(X)) |
| negrecip(ok(X)) | → | ok(negrecip(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| rcons(ok(X1), ok(X2)) | → | ok(rcons(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| 2ndspos(ok(X1), ok(X2)) | → | ok(2ndspos(X1, X2)) | | 2ndsneg(ok(X1), ok(X2)) | → | ok(2ndsneg(X1, X2)) |
| pi(ok(X)) | → | ok(pi(X)) | | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) |
| times(ok(X1), ok(X2)) | → | ok(times(X1, X2)) | | square(ok(X)) | → | ok(square(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: plus, posrecip, negrecip, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, proper, square, pi, top, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- 2ndsneg(x,y): 0
- 2ndspos(x,y): 0
- 2ndspos#(x,y): y + x + 1
- active(x): 0
- cons(x,y): 0
- from(x): 0
- mark(x): x + 2
- negrecip(x): 0
- nil: 0
- ok(x): 0
- pi(x): 0
- plus(x,y): 0
- posrecip(x): 0
- proper(x): 0
- rcons(x,y): 0
- rnil: 0
- s(x): 0
- square(x): 0
- times(x,y): 0
- top(x): 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:
| 2ndspos#(X1, mark(X2)) | → | 2ndspos#(X1, X2) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| 2ndsneg#(X1, mark(X2)) | → | 2ndsneg#(X1, X2) | | 2ndsneg#(mark(X1), X2) | → | 2ndsneg#(X1, X2) |
| 2ndsneg#(ok(X1), ok(X2)) | → | 2ndsneg#(X1, X2) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) | | active(2ndsneg(0, Z)) | → | mark(rnil) |
| active(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(negrecip(Y), 2ndspos(N, Z))) | | active(pi(X)) | → | mark(2ndspos(X, from(0))) |
| active(plus(0, Y)) | → | mark(Y) | | active(plus(s(X), Y)) | → | mark(s(plus(X, Y))) |
| active(times(0, Y)) | → | mark(0) | | active(times(s(X), Y)) | → | mark(plus(Y, times(X, Y))) |
| active(square(X)) | → | mark(times(X, X)) | | active(s(X)) | → | s(active(X)) |
| active(posrecip(X)) | → | posrecip(active(X)) | | active(negrecip(X)) | → | negrecip(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(rcons(X1, X2)) | → | rcons(active(X1), X2) |
| active(rcons(X1, X2)) | → | rcons(X1, active(X2)) | | active(from(X)) | → | from(active(X)) |
| active(2ndspos(X1, X2)) | → | 2ndspos(active(X1), X2) | | active(2ndspos(X1, X2)) | → | 2ndspos(X1, active(X2)) |
| active(2ndsneg(X1, X2)) | → | 2ndsneg(active(X1), X2) | | active(2ndsneg(X1, X2)) | → | 2ndsneg(X1, active(X2)) |
| active(pi(X)) | → | pi(active(X)) | | active(plus(X1, X2)) | → | plus(active(X1), X2) |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | | active(times(X1, X2)) | → | times(active(X1), X2) |
| active(times(X1, X2)) | → | times(X1, active(X2)) | | active(square(X)) | → | square(active(X)) |
| s(mark(X)) | → | mark(s(X)) | | posrecip(mark(X)) | → | mark(posrecip(X)) |
| negrecip(mark(X)) | → | mark(negrecip(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| rcons(mark(X1), X2) | → | mark(rcons(X1, X2)) | | rcons(X1, mark(X2)) | → | mark(rcons(X1, X2)) |
| from(mark(X)) | → | mark(from(X)) | | 2ndspos(mark(X1), X2) | → | mark(2ndspos(X1, X2)) |
| 2ndspos(X1, mark(X2)) | → | mark(2ndspos(X1, X2)) | | 2ndsneg(mark(X1), X2) | → | mark(2ndsneg(X1, X2)) |
| 2ndsneg(X1, mark(X2)) | → | mark(2ndsneg(X1, X2)) | | pi(mark(X)) | → | mark(pi(X)) |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) |
| times(mark(X1), X2) | → | mark(times(X1, X2)) | | times(X1, mark(X2)) | → | mark(times(X1, X2)) |
| square(mark(X)) | → | mark(square(X)) | | proper(0) | → | ok(0) |
| proper(s(X)) | → | s(proper(X)) | | proper(posrecip(X)) | → | posrecip(proper(X)) |
| proper(negrecip(X)) | → | negrecip(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(rnil) | → | ok(rnil) |
| proper(rcons(X1, X2)) | → | rcons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(2ndspos(X1, X2)) | → | 2ndspos(proper(X1), proper(X2)) | | proper(2ndsneg(X1, X2)) | → | 2ndsneg(proper(X1), proper(X2)) |
| proper(pi(X)) | → | pi(proper(X)) | | proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) |
| proper(times(X1, X2)) | → | times(proper(X1), proper(X2)) | | proper(square(X)) | → | square(proper(X)) |
| s(ok(X)) | → | ok(s(X)) | | posrecip(ok(X)) | → | ok(posrecip(X)) |
| negrecip(ok(X)) | → | ok(negrecip(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| rcons(ok(X1), ok(X2)) | → | ok(rcons(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| 2ndspos(ok(X1), ok(X2)) | → | ok(2ndspos(X1, X2)) | | 2ndsneg(ok(X1), ok(X2)) | → | ok(2ndsneg(X1, X2)) |
| pi(ok(X)) | → | ok(pi(X)) | | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) |
| times(ok(X1), ok(X2)) | → | ok(times(X1, X2)) | | square(ok(X)) | → | ok(square(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: plus, posrecip, negrecip, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, square, proper, pi, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| 2ndsneg#(mark(X1), X2) | → | 2ndsneg#(X1, X2) | | 2ndsneg#(ok(X1), ok(X2)) | → | 2ndsneg#(X1, X2) |
Problem 18: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| 2ndsneg#(X1, mark(X2)) | → | 2ndsneg#(X1, X2) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) | | active(2ndsneg(0, Z)) | → | mark(rnil) |
| active(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(negrecip(Y), 2ndspos(N, Z))) | | active(pi(X)) | → | mark(2ndspos(X, from(0))) |
| active(plus(0, Y)) | → | mark(Y) | | active(plus(s(X), Y)) | → | mark(s(plus(X, Y))) |
| active(times(0, Y)) | → | mark(0) | | active(times(s(X), Y)) | → | mark(plus(Y, times(X, Y))) |
| active(square(X)) | → | mark(times(X, X)) | | active(s(X)) | → | s(active(X)) |
| active(posrecip(X)) | → | posrecip(active(X)) | | active(negrecip(X)) | → | negrecip(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(rcons(X1, X2)) | → | rcons(active(X1), X2) |
| active(rcons(X1, X2)) | → | rcons(X1, active(X2)) | | active(from(X)) | → | from(active(X)) |
| active(2ndspos(X1, X2)) | → | 2ndspos(active(X1), X2) | | active(2ndspos(X1, X2)) | → | 2ndspos(X1, active(X2)) |
| active(2ndsneg(X1, X2)) | → | 2ndsneg(active(X1), X2) | | active(2ndsneg(X1, X2)) | → | 2ndsneg(X1, active(X2)) |
| active(pi(X)) | → | pi(active(X)) | | active(plus(X1, X2)) | → | plus(active(X1), X2) |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | | active(times(X1, X2)) | → | times(active(X1), X2) |
| active(times(X1, X2)) | → | times(X1, active(X2)) | | active(square(X)) | → | square(active(X)) |
| s(mark(X)) | → | mark(s(X)) | | posrecip(mark(X)) | → | mark(posrecip(X)) |
| negrecip(mark(X)) | → | mark(negrecip(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| rcons(mark(X1), X2) | → | mark(rcons(X1, X2)) | | rcons(X1, mark(X2)) | → | mark(rcons(X1, X2)) |
| from(mark(X)) | → | mark(from(X)) | | 2ndspos(mark(X1), X2) | → | mark(2ndspos(X1, X2)) |
| 2ndspos(X1, mark(X2)) | → | mark(2ndspos(X1, X2)) | | 2ndsneg(mark(X1), X2) | → | mark(2ndsneg(X1, X2)) |
| 2ndsneg(X1, mark(X2)) | → | mark(2ndsneg(X1, X2)) | | pi(mark(X)) | → | mark(pi(X)) |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) |
| times(mark(X1), X2) | → | mark(times(X1, X2)) | | times(X1, mark(X2)) | → | mark(times(X1, X2)) |
| square(mark(X)) | → | mark(square(X)) | | proper(0) | → | ok(0) |
| proper(s(X)) | → | s(proper(X)) | | proper(posrecip(X)) | → | posrecip(proper(X)) |
| proper(negrecip(X)) | → | negrecip(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(rnil) | → | ok(rnil) |
| proper(rcons(X1, X2)) | → | rcons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(2ndspos(X1, X2)) | → | 2ndspos(proper(X1), proper(X2)) | | proper(2ndsneg(X1, X2)) | → | 2ndsneg(proper(X1), proper(X2)) |
| proper(pi(X)) | → | pi(proper(X)) | | proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) |
| proper(times(X1, X2)) | → | times(proper(X1), proper(X2)) | | proper(square(X)) | → | square(proper(X)) |
| s(ok(X)) | → | ok(s(X)) | | posrecip(ok(X)) | → | ok(posrecip(X)) |
| negrecip(ok(X)) | → | ok(negrecip(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| rcons(ok(X1), ok(X2)) | → | ok(rcons(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| 2ndspos(ok(X1), ok(X2)) | → | ok(2ndspos(X1, X2)) | | 2ndsneg(ok(X1), ok(X2)) | → | ok(2ndsneg(X1, X2)) |
| pi(ok(X)) | → | ok(pi(X)) | | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) |
| times(ok(X1), ok(X2)) | → | ok(times(X1, X2)) | | square(ok(X)) | → | ok(square(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: plus, posrecip, negrecip, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, proper, square, pi, top, nil, cons
Strategy
Function Precedence
plus = posrecip = negrecip = rnil = 2ndsneg# = mark = from = rcons = 2ndspos = 0 = s = times = 2ndsneg = active = ok = square = proper = pi = top = cons = nil
Argument Filtering
plus: 1
posrecip: all arguments are removed from posrecip
negrecip: collapses to 1
rnil: all arguments are removed from rnil
2ndsneg#: 2
mark: 1
from: all arguments are removed from from
rcons: all arguments are removed from rcons
2ndspos: all arguments are removed from 2ndspos
0: all arguments are removed from 0
s: all arguments are removed from s
times: all arguments are removed from times
2ndsneg: 1 2
active: collapses to 1
ok: all arguments are removed from ok
square: all arguments are removed from square
proper: all arguments are removed from proper
pi: 1
top: collapses to 1
cons: 1 2
nil: all arguments are removed from nil
Status
plus: lexicographic with permutation 1 → 1
posrecip: multiset
rnil: multiset
2ndsneg#: lexicographic with permutation 2 → 1
mark: multiset
from: multiset
rcons: multiset
2ndspos: multiset
0: multiset
s: multiset
times: multiset
2ndsneg: lexicographic with permutation 1 → 1 2 → 2
ok: multiset
square: multiset
proper: multiset
pi: lexicographic with permutation 1 → 1
cons: lexicographic with permutation 1 → 2 2 → 1
nil: multiset
Usable Rules
There are no usable rules.
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.
| 2ndsneg#(X1, mark(X2)) → 2ndsneg#(X1, X2) |
Problem 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| from#(mark(X)) | → | from#(X) | | from#(ok(X)) | → | from#(X) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) | | active(2ndsneg(0, Z)) | → | mark(rnil) |
| active(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(negrecip(Y), 2ndspos(N, Z))) | | active(pi(X)) | → | mark(2ndspos(X, from(0))) |
| active(plus(0, Y)) | → | mark(Y) | | active(plus(s(X), Y)) | → | mark(s(plus(X, Y))) |
| active(times(0, Y)) | → | mark(0) | | active(times(s(X), Y)) | → | mark(plus(Y, times(X, Y))) |
| active(square(X)) | → | mark(times(X, X)) | | active(s(X)) | → | s(active(X)) |
| active(posrecip(X)) | → | posrecip(active(X)) | | active(negrecip(X)) | → | negrecip(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(rcons(X1, X2)) | → | rcons(active(X1), X2) |
| active(rcons(X1, X2)) | → | rcons(X1, active(X2)) | | active(from(X)) | → | from(active(X)) |
| active(2ndspos(X1, X2)) | → | 2ndspos(active(X1), X2) | | active(2ndspos(X1, X2)) | → | 2ndspos(X1, active(X2)) |
| active(2ndsneg(X1, X2)) | → | 2ndsneg(active(X1), X2) | | active(2ndsneg(X1, X2)) | → | 2ndsneg(X1, active(X2)) |
| active(pi(X)) | → | pi(active(X)) | | active(plus(X1, X2)) | → | plus(active(X1), X2) |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | | active(times(X1, X2)) | → | times(active(X1), X2) |
| active(times(X1, X2)) | → | times(X1, active(X2)) | | active(square(X)) | → | square(active(X)) |
| s(mark(X)) | → | mark(s(X)) | | posrecip(mark(X)) | → | mark(posrecip(X)) |
| negrecip(mark(X)) | → | mark(negrecip(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| rcons(mark(X1), X2) | → | mark(rcons(X1, X2)) | | rcons(X1, mark(X2)) | → | mark(rcons(X1, X2)) |
| from(mark(X)) | → | mark(from(X)) | | 2ndspos(mark(X1), X2) | → | mark(2ndspos(X1, X2)) |
| 2ndspos(X1, mark(X2)) | → | mark(2ndspos(X1, X2)) | | 2ndsneg(mark(X1), X2) | → | mark(2ndsneg(X1, X2)) |
| 2ndsneg(X1, mark(X2)) | → | mark(2ndsneg(X1, X2)) | | pi(mark(X)) | → | mark(pi(X)) |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) |
| times(mark(X1), X2) | → | mark(times(X1, X2)) | | times(X1, mark(X2)) | → | mark(times(X1, X2)) |
| square(mark(X)) | → | mark(square(X)) | | proper(0) | → | ok(0) |
| proper(s(X)) | → | s(proper(X)) | | proper(posrecip(X)) | → | posrecip(proper(X)) |
| proper(negrecip(X)) | → | negrecip(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(rnil) | → | ok(rnil) |
| proper(rcons(X1, X2)) | → | rcons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(2ndspos(X1, X2)) | → | 2ndspos(proper(X1), proper(X2)) | | proper(2ndsneg(X1, X2)) | → | 2ndsneg(proper(X1), proper(X2)) |
| proper(pi(X)) | → | pi(proper(X)) | | proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) |
| proper(times(X1, X2)) | → | times(proper(X1), proper(X2)) | | proper(square(X)) | → | square(proper(X)) |
| s(ok(X)) | → | ok(s(X)) | | posrecip(ok(X)) | → | ok(posrecip(X)) |
| negrecip(ok(X)) | → | ok(negrecip(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| rcons(ok(X1), ok(X2)) | → | ok(rcons(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| 2ndspos(ok(X1), ok(X2)) | → | ok(2ndspos(X1, X2)) | | 2ndsneg(ok(X1), ok(X2)) | → | ok(2ndsneg(X1, X2)) |
| pi(ok(X)) | → | ok(pi(X)) | | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) |
| times(ok(X1), ok(X2)) | → | ok(times(X1, X2)) | | square(ok(X)) | → | ok(square(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: plus, posrecip, negrecip, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, square, proper, pi, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| from#(mark(X)) | → | from#(X) | | from#(ok(X)) | → | from#(X) |
Problem 9: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| negrecip#(ok(X)) | → | negrecip#(X) | | negrecip#(mark(X)) | → | negrecip#(X) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) | | active(2ndsneg(0, Z)) | → | mark(rnil) |
| active(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(negrecip(Y), 2ndspos(N, Z))) | | active(pi(X)) | → | mark(2ndspos(X, from(0))) |
| active(plus(0, Y)) | → | mark(Y) | | active(plus(s(X), Y)) | → | mark(s(plus(X, Y))) |
| active(times(0, Y)) | → | mark(0) | | active(times(s(X), Y)) | → | mark(plus(Y, times(X, Y))) |
| active(square(X)) | → | mark(times(X, X)) | | active(s(X)) | → | s(active(X)) |
| active(posrecip(X)) | → | posrecip(active(X)) | | active(negrecip(X)) | → | negrecip(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(rcons(X1, X2)) | → | rcons(active(X1), X2) |
| active(rcons(X1, X2)) | → | rcons(X1, active(X2)) | | active(from(X)) | → | from(active(X)) |
| active(2ndspos(X1, X2)) | → | 2ndspos(active(X1), X2) | | active(2ndspos(X1, X2)) | → | 2ndspos(X1, active(X2)) |
| active(2ndsneg(X1, X2)) | → | 2ndsneg(active(X1), X2) | | active(2ndsneg(X1, X2)) | → | 2ndsneg(X1, active(X2)) |
| active(pi(X)) | → | pi(active(X)) | | active(plus(X1, X2)) | → | plus(active(X1), X2) |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | | active(times(X1, X2)) | → | times(active(X1), X2) |
| active(times(X1, X2)) | → | times(X1, active(X2)) | | active(square(X)) | → | square(active(X)) |
| s(mark(X)) | → | mark(s(X)) | | posrecip(mark(X)) | → | mark(posrecip(X)) |
| negrecip(mark(X)) | → | mark(negrecip(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| rcons(mark(X1), X2) | → | mark(rcons(X1, X2)) | | rcons(X1, mark(X2)) | → | mark(rcons(X1, X2)) |
| from(mark(X)) | → | mark(from(X)) | | 2ndspos(mark(X1), X2) | → | mark(2ndspos(X1, X2)) |
| 2ndspos(X1, mark(X2)) | → | mark(2ndspos(X1, X2)) | | 2ndsneg(mark(X1), X2) | → | mark(2ndsneg(X1, X2)) |
| 2ndsneg(X1, mark(X2)) | → | mark(2ndsneg(X1, X2)) | | pi(mark(X)) | → | mark(pi(X)) |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) |
| times(mark(X1), X2) | → | mark(times(X1, X2)) | | times(X1, mark(X2)) | → | mark(times(X1, X2)) |
| square(mark(X)) | → | mark(square(X)) | | proper(0) | → | ok(0) |
| proper(s(X)) | → | s(proper(X)) | | proper(posrecip(X)) | → | posrecip(proper(X)) |
| proper(negrecip(X)) | → | negrecip(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(rnil) | → | ok(rnil) |
| proper(rcons(X1, X2)) | → | rcons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(2ndspos(X1, X2)) | → | 2ndspos(proper(X1), proper(X2)) | | proper(2ndsneg(X1, X2)) | → | 2ndsneg(proper(X1), proper(X2)) |
| proper(pi(X)) | → | pi(proper(X)) | | proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) |
| proper(times(X1, X2)) | → | times(proper(X1), proper(X2)) | | proper(square(X)) | → | square(proper(X)) |
| s(ok(X)) | → | ok(s(X)) | | posrecip(ok(X)) | → | ok(posrecip(X)) |
| negrecip(ok(X)) | → | ok(negrecip(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| rcons(ok(X1), ok(X2)) | → | ok(rcons(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| 2ndspos(ok(X1), ok(X2)) | → | ok(2ndspos(X1, X2)) | | 2ndsneg(ok(X1), ok(X2)) | → | ok(2ndsneg(X1, X2)) |
| pi(ok(X)) | → | ok(pi(X)) | | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) |
| times(ok(X1), ok(X2)) | → | ok(times(X1, X2)) | | square(ok(X)) | → | ok(square(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: plus, posrecip, negrecip, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, square, proper, pi, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| negrecip#(ok(X)) | → | negrecip#(X) | | negrecip#(mark(X)) | → | negrecip#(X) |
Problem 10: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| s#(mark(X)) | → | s#(X) | | s#(ok(X)) | → | s#(X) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) | | active(2ndsneg(0, Z)) | → | mark(rnil) |
| active(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(negrecip(Y), 2ndspos(N, Z))) | | active(pi(X)) | → | mark(2ndspos(X, from(0))) |
| active(plus(0, Y)) | → | mark(Y) | | active(plus(s(X), Y)) | → | mark(s(plus(X, Y))) |
| active(times(0, Y)) | → | mark(0) | | active(times(s(X), Y)) | → | mark(plus(Y, times(X, Y))) |
| active(square(X)) | → | mark(times(X, X)) | | active(s(X)) | → | s(active(X)) |
| active(posrecip(X)) | → | posrecip(active(X)) | | active(negrecip(X)) | → | negrecip(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(rcons(X1, X2)) | → | rcons(active(X1), X2) |
| active(rcons(X1, X2)) | → | rcons(X1, active(X2)) | | active(from(X)) | → | from(active(X)) |
| active(2ndspos(X1, X2)) | → | 2ndspos(active(X1), X2) | | active(2ndspos(X1, X2)) | → | 2ndspos(X1, active(X2)) |
| active(2ndsneg(X1, X2)) | → | 2ndsneg(active(X1), X2) | | active(2ndsneg(X1, X2)) | → | 2ndsneg(X1, active(X2)) |
| active(pi(X)) | → | pi(active(X)) | | active(plus(X1, X2)) | → | plus(active(X1), X2) |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | | active(times(X1, X2)) | → | times(active(X1), X2) |
| active(times(X1, X2)) | → | times(X1, active(X2)) | | active(square(X)) | → | square(active(X)) |
| s(mark(X)) | → | mark(s(X)) | | posrecip(mark(X)) | → | mark(posrecip(X)) |
| negrecip(mark(X)) | → | mark(negrecip(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| rcons(mark(X1), X2) | → | mark(rcons(X1, X2)) | | rcons(X1, mark(X2)) | → | mark(rcons(X1, X2)) |
| from(mark(X)) | → | mark(from(X)) | | 2ndspos(mark(X1), X2) | → | mark(2ndspos(X1, X2)) |
| 2ndspos(X1, mark(X2)) | → | mark(2ndspos(X1, X2)) | | 2ndsneg(mark(X1), X2) | → | mark(2ndsneg(X1, X2)) |
| 2ndsneg(X1, mark(X2)) | → | mark(2ndsneg(X1, X2)) | | pi(mark(X)) | → | mark(pi(X)) |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) |
| times(mark(X1), X2) | → | mark(times(X1, X2)) | | times(X1, mark(X2)) | → | mark(times(X1, X2)) |
| square(mark(X)) | → | mark(square(X)) | | proper(0) | → | ok(0) |
| proper(s(X)) | → | s(proper(X)) | | proper(posrecip(X)) | → | posrecip(proper(X)) |
| proper(negrecip(X)) | → | negrecip(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(rnil) | → | ok(rnil) |
| proper(rcons(X1, X2)) | → | rcons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(2ndspos(X1, X2)) | → | 2ndspos(proper(X1), proper(X2)) | | proper(2ndsneg(X1, X2)) | → | 2ndsneg(proper(X1), proper(X2)) |
| proper(pi(X)) | → | pi(proper(X)) | | proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) |
| proper(times(X1, X2)) | → | times(proper(X1), proper(X2)) | | proper(square(X)) | → | square(proper(X)) |
| s(ok(X)) | → | ok(s(X)) | | posrecip(ok(X)) | → | ok(posrecip(X)) |
| negrecip(ok(X)) | → | ok(negrecip(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| rcons(ok(X1), ok(X2)) | → | ok(rcons(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| 2ndspos(ok(X1), ok(X2)) | → | ok(2ndspos(X1, X2)) | | 2ndsneg(ok(X1), ok(X2)) | → | ok(2ndsneg(X1, X2)) |
| pi(ok(X)) | → | ok(pi(X)) | | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) |
| times(ok(X1), ok(X2)) | → | ok(times(X1, X2)) | | square(ok(X)) | → | ok(square(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: plus, posrecip, negrecip, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, square, proper, pi, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| s#(mark(X)) | → | s#(X) | | s#(ok(X)) | → | s#(X) |
Problem 11: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) | | active(2ndsneg(0, Z)) | → | mark(rnil) |
| active(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(negrecip(Y), 2ndspos(N, Z))) | | active(pi(X)) | → | mark(2ndspos(X, from(0))) |
| active(plus(0, Y)) | → | mark(Y) | | active(plus(s(X), Y)) | → | mark(s(plus(X, Y))) |
| active(times(0, Y)) | → | mark(0) | | active(times(s(X), Y)) | → | mark(plus(Y, times(X, Y))) |
| active(square(X)) | → | mark(times(X, X)) | | active(s(X)) | → | s(active(X)) |
| active(posrecip(X)) | → | posrecip(active(X)) | | active(negrecip(X)) | → | negrecip(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(rcons(X1, X2)) | → | rcons(active(X1), X2) |
| active(rcons(X1, X2)) | → | rcons(X1, active(X2)) | | active(from(X)) | → | from(active(X)) |
| active(2ndspos(X1, X2)) | → | 2ndspos(active(X1), X2) | | active(2ndspos(X1, X2)) | → | 2ndspos(X1, active(X2)) |
| active(2ndsneg(X1, X2)) | → | 2ndsneg(active(X1), X2) | | active(2ndsneg(X1, X2)) | → | 2ndsneg(X1, active(X2)) |
| active(pi(X)) | → | pi(active(X)) | | active(plus(X1, X2)) | → | plus(active(X1), X2) |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | | active(times(X1, X2)) | → | times(active(X1), X2) |
| active(times(X1, X2)) | → | times(X1, active(X2)) | | active(square(X)) | → | square(active(X)) |
| s(mark(X)) | → | mark(s(X)) | | posrecip(mark(X)) | → | mark(posrecip(X)) |
| negrecip(mark(X)) | → | mark(negrecip(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| rcons(mark(X1), X2) | → | mark(rcons(X1, X2)) | | rcons(X1, mark(X2)) | → | mark(rcons(X1, X2)) |
| from(mark(X)) | → | mark(from(X)) | | 2ndspos(mark(X1), X2) | → | mark(2ndspos(X1, X2)) |
| 2ndspos(X1, mark(X2)) | → | mark(2ndspos(X1, X2)) | | 2ndsneg(mark(X1), X2) | → | mark(2ndsneg(X1, X2)) |
| 2ndsneg(X1, mark(X2)) | → | mark(2ndsneg(X1, X2)) | | pi(mark(X)) | → | mark(pi(X)) |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) |
| times(mark(X1), X2) | → | mark(times(X1, X2)) | | times(X1, mark(X2)) | → | mark(times(X1, X2)) |
| square(mark(X)) | → | mark(square(X)) | | proper(0) | → | ok(0) |
| proper(s(X)) | → | s(proper(X)) | | proper(posrecip(X)) | → | posrecip(proper(X)) |
| proper(negrecip(X)) | → | negrecip(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(rnil) | → | ok(rnil) |
| proper(rcons(X1, X2)) | → | rcons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(2ndspos(X1, X2)) | → | 2ndspos(proper(X1), proper(X2)) | | proper(2ndsneg(X1, X2)) | → | 2ndsneg(proper(X1), proper(X2)) |
| proper(pi(X)) | → | pi(proper(X)) | | proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) |
| proper(times(X1, X2)) | → | times(proper(X1), proper(X2)) | | proper(square(X)) | → | square(proper(X)) |
| s(ok(X)) | → | ok(s(X)) | | posrecip(ok(X)) | → | ok(posrecip(X)) |
| negrecip(ok(X)) | → | ok(negrecip(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| rcons(ok(X1), ok(X2)) | → | ok(rcons(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| 2ndspos(ok(X1), ok(X2)) | → | ok(2ndspos(X1, X2)) | | 2ndsneg(ok(X1), ok(X2)) | → | ok(2ndsneg(X1, X2)) |
| pi(ok(X)) | → | ok(pi(X)) | | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) |
| times(ok(X1), ok(X2)) | → | ok(times(X1, X2)) | | square(ok(X)) | → | ok(square(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: plus, posrecip, negrecip, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, square, proper, pi, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
Problem 12: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| rcons#(ok(X1), ok(X2)) | → | rcons#(X1, X2) | | rcons#(mark(X1), X2) | → | rcons#(X1, X2) |
| rcons#(X1, mark(X2)) | → | rcons#(X1, X2) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) | | active(2ndsneg(0, Z)) | → | mark(rnil) |
| active(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(negrecip(Y), 2ndspos(N, Z))) | | active(pi(X)) | → | mark(2ndspos(X, from(0))) |
| active(plus(0, Y)) | → | mark(Y) | | active(plus(s(X), Y)) | → | mark(s(plus(X, Y))) |
| active(times(0, Y)) | → | mark(0) | | active(times(s(X), Y)) | → | mark(plus(Y, times(X, Y))) |
| active(square(X)) | → | mark(times(X, X)) | | active(s(X)) | → | s(active(X)) |
| active(posrecip(X)) | → | posrecip(active(X)) | | active(negrecip(X)) | → | negrecip(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(rcons(X1, X2)) | → | rcons(active(X1), X2) |
| active(rcons(X1, X2)) | → | rcons(X1, active(X2)) | | active(from(X)) | → | from(active(X)) |
| active(2ndspos(X1, X2)) | → | 2ndspos(active(X1), X2) | | active(2ndspos(X1, X2)) | → | 2ndspos(X1, active(X2)) |
| active(2ndsneg(X1, X2)) | → | 2ndsneg(active(X1), X2) | | active(2ndsneg(X1, X2)) | → | 2ndsneg(X1, active(X2)) |
| active(pi(X)) | → | pi(active(X)) | | active(plus(X1, X2)) | → | plus(active(X1), X2) |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | | active(times(X1, X2)) | → | times(active(X1), X2) |
| active(times(X1, X2)) | → | times(X1, active(X2)) | | active(square(X)) | → | square(active(X)) |
| s(mark(X)) | → | mark(s(X)) | | posrecip(mark(X)) | → | mark(posrecip(X)) |
| negrecip(mark(X)) | → | mark(negrecip(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| rcons(mark(X1), X2) | → | mark(rcons(X1, X2)) | | rcons(X1, mark(X2)) | → | mark(rcons(X1, X2)) |
| from(mark(X)) | → | mark(from(X)) | | 2ndspos(mark(X1), X2) | → | mark(2ndspos(X1, X2)) |
| 2ndspos(X1, mark(X2)) | → | mark(2ndspos(X1, X2)) | | 2ndsneg(mark(X1), X2) | → | mark(2ndsneg(X1, X2)) |
| 2ndsneg(X1, mark(X2)) | → | mark(2ndsneg(X1, X2)) | | pi(mark(X)) | → | mark(pi(X)) |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) |
| times(mark(X1), X2) | → | mark(times(X1, X2)) | | times(X1, mark(X2)) | → | mark(times(X1, X2)) |
| square(mark(X)) | → | mark(square(X)) | | proper(0) | → | ok(0) |
| proper(s(X)) | → | s(proper(X)) | | proper(posrecip(X)) | → | posrecip(proper(X)) |
| proper(negrecip(X)) | → | negrecip(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(rnil) | → | ok(rnil) |
| proper(rcons(X1, X2)) | → | rcons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(2ndspos(X1, X2)) | → | 2ndspos(proper(X1), proper(X2)) | | proper(2ndsneg(X1, X2)) | → | 2ndsneg(proper(X1), proper(X2)) |
| proper(pi(X)) | → | pi(proper(X)) | | proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) |
| proper(times(X1, X2)) | → | times(proper(X1), proper(X2)) | | proper(square(X)) | → | square(proper(X)) |
| s(ok(X)) | → | ok(s(X)) | | posrecip(ok(X)) | → | ok(posrecip(X)) |
| negrecip(ok(X)) | → | ok(negrecip(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| rcons(ok(X1), ok(X2)) | → | ok(rcons(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| 2ndspos(ok(X1), ok(X2)) | → | ok(2ndspos(X1, X2)) | | 2ndsneg(ok(X1), ok(X2)) | → | ok(2ndsneg(X1, X2)) |
| pi(ok(X)) | → | ok(pi(X)) | | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) |
| times(ok(X1), ok(X2)) | → | ok(times(X1, X2)) | | square(ok(X)) | → | ok(square(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: plus, posrecip, negrecip, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, square, proper, pi, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| rcons#(ok(X1), ok(X2)) | → | rcons#(X1, X2) | | rcons#(mark(X1), X2) | → | rcons#(X1, X2) |
Problem 19: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| rcons#(X1, mark(X2)) | → | rcons#(X1, X2) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) | | active(2ndsneg(0, Z)) | → | mark(rnil) |
| active(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(negrecip(Y), 2ndspos(N, Z))) | | active(pi(X)) | → | mark(2ndspos(X, from(0))) |
| active(plus(0, Y)) | → | mark(Y) | | active(plus(s(X), Y)) | → | mark(s(plus(X, Y))) |
| active(times(0, Y)) | → | mark(0) | | active(times(s(X), Y)) | → | mark(plus(Y, times(X, Y))) |
| active(square(X)) | → | mark(times(X, X)) | | active(s(X)) | → | s(active(X)) |
| active(posrecip(X)) | → | posrecip(active(X)) | | active(negrecip(X)) | → | negrecip(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(rcons(X1, X2)) | → | rcons(active(X1), X2) |
| active(rcons(X1, X2)) | → | rcons(X1, active(X2)) | | active(from(X)) | → | from(active(X)) |
| active(2ndspos(X1, X2)) | → | 2ndspos(active(X1), X2) | | active(2ndspos(X1, X2)) | → | 2ndspos(X1, active(X2)) |
| active(2ndsneg(X1, X2)) | → | 2ndsneg(active(X1), X2) | | active(2ndsneg(X1, X2)) | → | 2ndsneg(X1, active(X2)) |
| active(pi(X)) | → | pi(active(X)) | | active(plus(X1, X2)) | → | plus(active(X1), X2) |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | | active(times(X1, X2)) | → | times(active(X1), X2) |
| active(times(X1, X2)) | → | times(X1, active(X2)) | | active(square(X)) | → | square(active(X)) |
| s(mark(X)) | → | mark(s(X)) | | posrecip(mark(X)) | → | mark(posrecip(X)) |
| negrecip(mark(X)) | → | mark(negrecip(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| rcons(mark(X1), X2) | → | mark(rcons(X1, X2)) | | rcons(X1, mark(X2)) | → | mark(rcons(X1, X2)) |
| from(mark(X)) | → | mark(from(X)) | | 2ndspos(mark(X1), X2) | → | mark(2ndspos(X1, X2)) |
| 2ndspos(X1, mark(X2)) | → | mark(2ndspos(X1, X2)) | | 2ndsneg(mark(X1), X2) | → | mark(2ndsneg(X1, X2)) |
| 2ndsneg(X1, mark(X2)) | → | mark(2ndsneg(X1, X2)) | | pi(mark(X)) | → | mark(pi(X)) |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) |
| times(mark(X1), X2) | → | mark(times(X1, X2)) | | times(X1, mark(X2)) | → | mark(times(X1, X2)) |
| square(mark(X)) | → | mark(square(X)) | | proper(0) | → | ok(0) |
| proper(s(X)) | → | s(proper(X)) | | proper(posrecip(X)) | → | posrecip(proper(X)) |
| proper(negrecip(X)) | → | negrecip(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(rnil) | → | ok(rnil) |
| proper(rcons(X1, X2)) | → | rcons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(2ndspos(X1, X2)) | → | 2ndspos(proper(X1), proper(X2)) | | proper(2ndsneg(X1, X2)) | → | 2ndsneg(proper(X1), proper(X2)) |
| proper(pi(X)) | → | pi(proper(X)) | | proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) |
| proper(times(X1, X2)) | → | times(proper(X1), proper(X2)) | | proper(square(X)) | → | square(proper(X)) |
| s(ok(X)) | → | ok(s(X)) | | posrecip(ok(X)) | → | ok(posrecip(X)) |
| negrecip(ok(X)) | → | ok(negrecip(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| rcons(ok(X1), ok(X2)) | → | ok(rcons(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| 2ndspos(ok(X1), ok(X2)) | → | ok(2ndspos(X1, X2)) | | 2ndsneg(ok(X1), ok(X2)) | → | ok(2ndsneg(X1, X2)) |
| pi(ok(X)) | → | ok(pi(X)) | | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) |
| times(ok(X1), ok(X2)) | → | ok(times(X1, X2)) | | square(ok(X)) | → | ok(square(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: plus, posrecip, negrecip, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, proper, square, pi, top, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- 2ndsneg(x,y): 0
- 2ndspos(x,y): 0
- active(x): 0
- cons(x,y): 0
- from(x): 0
- mark(x): 2x + 1
- negrecip(x): 0
- nil: 0
- ok(x): 0
- pi(x): 0
- plus(x,y): 0
- posrecip(x): 0
- proper(x): 0
- rcons(x,y): 0
- rcons#(x,y): 2y + x
- rnil: 0
- s(x): 0
- square(x): 0
- times(x,y): 0
- top(x): 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:
| rcons#(X1, mark(X2)) | → | rcons#(X1, X2) |
Problem 13: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| times#(ok(X1), ok(X2)) | → | times#(X1, X2) | | times#(X1, mark(X2)) | → | times#(X1, X2) |
| times#(mark(X1), X2) | → | times#(X1, X2) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) | | active(2ndsneg(0, Z)) | → | mark(rnil) |
| active(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(negrecip(Y), 2ndspos(N, Z))) | | active(pi(X)) | → | mark(2ndspos(X, from(0))) |
| active(plus(0, Y)) | → | mark(Y) | | active(plus(s(X), Y)) | → | mark(s(plus(X, Y))) |
| active(times(0, Y)) | → | mark(0) | | active(times(s(X), Y)) | → | mark(plus(Y, times(X, Y))) |
| active(square(X)) | → | mark(times(X, X)) | | active(s(X)) | → | s(active(X)) |
| active(posrecip(X)) | → | posrecip(active(X)) | | active(negrecip(X)) | → | negrecip(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(rcons(X1, X2)) | → | rcons(active(X1), X2) |
| active(rcons(X1, X2)) | → | rcons(X1, active(X2)) | | active(from(X)) | → | from(active(X)) |
| active(2ndspos(X1, X2)) | → | 2ndspos(active(X1), X2) | | active(2ndspos(X1, X2)) | → | 2ndspos(X1, active(X2)) |
| active(2ndsneg(X1, X2)) | → | 2ndsneg(active(X1), X2) | | active(2ndsneg(X1, X2)) | → | 2ndsneg(X1, active(X2)) |
| active(pi(X)) | → | pi(active(X)) | | active(plus(X1, X2)) | → | plus(active(X1), X2) |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | | active(times(X1, X2)) | → | times(active(X1), X2) |
| active(times(X1, X2)) | → | times(X1, active(X2)) | | active(square(X)) | → | square(active(X)) |
| s(mark(X)) | → | mark(s(X)) | | posrecip(mark(X)) | → | mark(posrecip(X)) |
| negrecip(mark(X)) | → | mark(negrecip(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| rcons(mark(X1), X2) | → | mark(rcons(X1, X2)) | | rcons(X1, mark(X2)) | → | mark(rcons(X1, X2)) |
| from(mark(X)) | → | mark(from(X)) | | 2ndspos(mark(X1), X2) | → | mark(2ndspos(X1, X2)) |
| 2ndspos(X1, mark(X2)) | → | mark(2ndspos(X1, X2)) | | 2ndsneg(mark(X1), X2) | → | mark(2ndsneg(X1, X2)) |
| 2ndsneg(X1, mark(X2)) | → | mark(2ndsneg(X1, X2)) | | pi(mark(X)) | → | mark(pi(X)) |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) |
| times(mark(X1), X2) | → | mark(times(X1, X2)) | | times(X1, mark(X2)) | → | mark(times(X1, X2)) |
| square(mark(X)) | → | mark(square(X)) | | proper(0) | → | ok(0) |
| proper(s(X)) | → | s(proper(X)) | | proper(posrecip(X)) | → | posrecip(proper(X)) |
| proper(negrecip(X)) | → | negrecip(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(rnil) | → | ok(rnil) |
| proper(rcons(X1, X2)) | → | rcons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(2ndspos(X1, X2)) | → | 2ndspos(proper(X1), proper(X2)) | | proper(2ndsneg(X1, X2)) | → | 2ndsneg(proper(X1), proper(X2)) |
| proper(pi(X)) | → | pi(proper(X)) | | proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) |
| proper(times(X1, X2)) | → | times(proper(X1), proper(X2)) | | proper(square(X)) | → | square(proper(X)) |
| s(ok(X)) | → | ok(s(X)) | | posrecip(ok(X)) | → | ok(posrecip(X)) |
| negrecip(ok(X)) | → | ok(negrecip(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| rcons(ok(X1), ok(X2)) | → | ok(rcons(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| 2ndspos(ok(X1), ok(X2)) | → | ok(2ndspos(X1, X2)) | | 2ndsneg(ok(X1), ok(X2)) | → | ok(2ndsneg(X1, X2)) |
| pi(ok(X)) | → | ok(pi(X)) | | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) |
| times(ok(X1), ok(X2)) | → | ok(times(X1, X2)) | | square(ok(X)) | → | ok(square(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: plus, posrecip, negrecip, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, square, proper, pi, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| times#(ok(X1), ok(X2)) | → | times#(X1, X2) | | times#(mark(X1), X2) | → | times#(X1, X2) |
Problem 20: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| times#(X1, mark(X2)) | → | times#(X1, X2) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) | | active(2ndsneg(0, Z)) | → | mark(rnil) |
| active(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(negrecip(Y), 2ndspos(N, Z))) | | active(pi(X)) | → | mark(2ndspos(X, from(0))) |
| active(plus(0, Y)) | → | mark(Y) | | active(plus(s(X), Y)) | → | mark(s(plus(X, Y))) |
| active(times(0, Y)) | → | mark(0) | | active(times(s(X), Y)) | → | mark(plus(Y, times(X, Y))) |
| active(square(X)) | → | mark(times(X, X)) | | active(s(X)) | → | s(active(X)) |
| active(posrecip(X)) | → | posrecip(active(X)) | | active(negrecip(X)) | → | negrecip(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(rcons(X1, X2)) | → | rcons(active(X1), X2) |
| active(rcons(X1, X2)) | → | rcons(X1, active(X2)) | | active(from(X)) | → | from(active(X)) |
| active(2ndspos(X1, X2)) | → | 2ndspos(active(X1), X2) | | active(2ndspos(X1, X2)) | → | 2ndspos(X1, active(X2)) |
| active(2ndsneg(X1, X2)) | → | 2ndsneg(active(X1), X2) | | active(2ndsneg(X1, X2)) | → | 2ndsneg(X1, active(X2)) |
| active(pi(X)) | → | pi(active(X)) | | active(plus(X1, X2)) | → | plus(active(X1), X2) |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | | active(times(X1, X2)) | → | times(active(X1), X2) |
| active(times(X1, X2)) | → | times(X1, active(X2)) | | active(square(X)) | → | square(active(X)) |
| s(mark(X)) | → | mark(s(X)) | | posrecip(mark(X)) | → | mark(posrecip(X)) |
| negrecip(mark(X)) | → | mark(negrecip(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| rcons(mark(X1), X2) | → | mark(rcons(X1, X2)) | | rcons(X1, mark(X2)) | → | mark(rcons(X1, X2)) |
| from(mark(X)) | → | mark(from(X)) | | 2ndspos(mark(X1), X2) | → | mark(2ndspos(X1, X2)) |
| 2ndspos(X1, mark(X2)) | → | mark(2ndspos(X1, X2)) | | 2ndsneg(mark(X1), X2) | → | mark(2ndsneg(X1, X2)) |
| 2ndsneg(X1, mark(X2)) | → | mark(2ndsneg(X1, X2)) | | pi(mark(X)) | → | mark(pi(X)) |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) |
| times(mark(X1), X2) | → | mark(times(X1, X2)) | | times(X1, mark(X2)) | → | mark(times(X1, X2)) |
| square(mark(X)) | → | mark(square(X)) | | proper(0) | → | ok(0) |
| proper(s(X)) | → | s(proper(X)) | | proper(posrecip(X)) | → | posrecip(proper(X)) |
| proper(negrecip(X)) | → | negrecip(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(rnil) | → | ok(rnil) |
| proper(rcons(X1, X2)) | → | rcons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(2ndspos(X1, X2)) | → | 2ndspos(proper(X1), proper(X2)) | | proper(2ndsneg(X1, X2)) | → | 2ndsneg(proper(X1), proper(X2)) |
| proper(pi(X)) | → | pi(proper(X)) | | proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) |
| proper(times(X1, X2)) | → | times(proper(X1), proper(X2)) | | proper(square(X)) | → | square(proper(X)) |
| s(ok(X)) | → | ok(s(X)) | | posrecip(ok(X)) | → | ok(posrecip(X)) |
| negrecip(ok(X)) | → | ok(negrecip(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| rcons(ok(X1), ok(X2)) | → | ok(rcons(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| 2ndspos(ok(X1), ok(X2)) | → | ok(2ndspos(X1, X2)) | | 2ndsneg(ok(X1), ok(X2)) | → | ok(2ndsneg(X1, X2)) |
| pi(ok(X)) | → | ok(pi(X)) | | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) |
| times(ok(X1), ok(X2)) | → | ok(times(X1, X2)) | | square(ok(X)) | → | ok(square(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: plus, posrecip, negrecip, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, proper, square, pi, top, nil, cons
Strategy
Function Precedence
times# < mark < plus = posrecip = negrecip = rnil = from = rcons = 2ndspos = 0 = s = times = 2ndsneg = active = ok = square = proper = pi = top = cons = nil
Argument Filtering
plus: all arguments are removed from plus
posrecip: all arguments are removed from posrecip
negrecip: all arguments are removed from negrecip
rnil: all arguments are removed from rnil
mark: 1
from: all arguments are removed from from
rcons: collapses to 2
2ndspos: all arguments are removed from 2ndspos
0: all arguments are removed from 0
times#: 2
s: all arguments are removed from s
times: all arguments are removed from times
2ndsneg: 1 2
active: all arguments are removed from active
ok: all arguments are removed from ok
square: collapses to 1
proper: collapses to 1
pi: collapses to 1
top: all arguments are removed from top
cons: 1 2
nil: all arguments are removed from nil
Status
plus: multiset
posrecip: multiset
negrecip: multiset
rnil: multiset
mark: multiset
from: multiset
2ndspos: multiset
0: multiset
times#: lexicographic with permutation 2 → 1
s: multiset
times: multiset
2ndsneg: lexicographic with permutation 1 → 2 2 → 1
active: multiset
ok: multiset
top: multiset
cons: lexicographic with permutation 1 → 2 2 → 1
nil: multiset
Usable Rules
There are no usable rules.
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.
| times#(X1, mark(X2)) → times#(X1, X2) |
Problem 14: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| plus#(ok(X1), ok(X2)) | → | plus#(X1, X2) | | plus#(X1, mark(X2)) | → | plus#(X1, X2) |
| plus#(mark(X1), X2) | → | plus#(X1, X2) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) | | active(2ndsneg(0, Z)) | → | mark(rnil) |
| active(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(negrecip(Y), 2ndspos(N, Z))) | | active(pi(X)) | → | mark(2ndspos(X, from(0))) |
| active(plus(0, Y)) | → | mark(Y) | | active(plus(s(X), Y)) | → | mark(s(plus(X, Y))) |
| active(times(0, Y)) | → | mark(0) | | active(times(s(X), Y)) | → | mark(plus(Y, times(X, Y))) |
| active(square(X)) | → | mark(times(X, X)) | | active(s(X)) | → | s(active(X)) |
| active(posrecip(X)) | → | posrecip(active(X)) | | active(negrecip(X)) | → | negrecip(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(rcons(X1, X2)) | → | rcons(active(X1), X2) |
| active(rcons(X1, X2)) | → | rcons(X1, active(X2)) | | active(from(X)) | → | from(active(X)) |
| active(2ndspos(X1, X2)) | → | 2ndspos(active(X1), X2) | | active(2ndspos(X1, X2)) | → | 2ndspos(X1, active(X2)) |
| active(2ndsneg(X1, X2)) | → | 2ndsneg(active(X1), X2) | | active(2ndsneg(X1, X2)) | → | 2ndsneg(X1, active(X2)) |
| active(pi(X)) | → | pi(active(X)) | | active(plus(X1, X2)) | → | plus(active(X1), X2) |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | | active(times(X1, X2)) | → | times(active(X1), X2) |
| active(times(X1, X2)) | → | times(X1, active(X2)) | | active(square(X)) | → | square(active(X)) |
| s(mark(X)) | → | mark(s(X)) | | posrecip(mark(X)) | → | mark(posrecip(X)) |
| negrecip(mark(X)) | → | mark(negrecip(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| rcons(mark(X1), X2) | → | mark(rcons(X1, X2)) | | rcons(X1, mark(X2)) | → | mark(rcons(X1, X2)) |
| from(mark(X)) | → | mark(from(X)) | | 2ndspos(mark(X1), X2) | → | mark(2ndspos(X1, X2)) |
| 2ndspos(X1, mark(X2)) | → | mark(2ndspos(X1, X2)) | | 2ndsneg(mark(X1), X2) | → | mark(2ndsneg(X1, X2)) |
| 2ndsneg(X1, mark(X2)) | → | mark(2ndsneg(X1, X2)) | | pi(mark(X)) | → | mark(pi(X)) |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) |
| times(mark(X1), X2) | → | mark(times(X1, X2)) | | times(X1, mark(X2)) | → | mark(times(X1, X2)) |
| square(mark(X)) | → | mark(square(X)) | | proper(0) | → | ok(0) |
| proper(s(X)) | → | s(proper(X)) | | proper(posrecip(X)) | → | posrecip(proper(X)) |
| proper(negrecip(X)) | → | negrecip(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(rnil) | → | ok(rnil) |
| proper(rcons(X1, X2)) | → | rcons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(2ndspos(X1, X2)) | → | 2ndspos(proper(X1), proper(X2)) | | proper(2ndsneg(X1, X2)) | → | 2ndsneg(proper(X1), proper(X2)) |
| proper(pi(X)) | → | pi(proper(X)) | | proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) |
| proper(times(X1, X2)) | → | times(proper(X1), proper(X2)) | | proper(square(X)) | → | square(proper(X)) |
| s(ok(X)) | → | ok(s(X)) | | posrecip(ok(X)) | → | ok(posrecip(X)) |
| negrecip(ok(X)) | → | ok(negrecip(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| rcons(ok(X1), ok(X2)) | → | ok(rcons(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| 2ndspos(ok(X1), ok(X2)) | → | ok(2ndspos(X1, X2)) | | 2ndsneg(ok(X1), ok(X2)) | → | ok(2ndsneg(X1, X2)) |
| pi(ok(X)) | → | ok(pi(X)) | | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) |
| times(ok(X1), ok(X2)) | → | ok(times(X1, X2)) | | square(ok(X)) | → | ok(square(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: plus, posrecip, negrecip, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, square, proper, pi, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| plus#(ok(X1), ok(X2)) | → | plus#(X1, X2) | | plus#(mark(X1), X2) | → | plus#(X1, X2) |
Problem 21: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| plus#(X1, mark(X2)) | → | plus#(X1, X2) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) | | active(2ndsneg(0, Z)) | → | mark(rnil) |
| active(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(negrecip(Y), 2ndspos(N, Z))) | | active(pi(X)) | → | mark(2ndspos(X, from(0))) |
| active(plus(0, Y)) | → | mark(Y) | | active(plus(s(X), Y)) | → | mark(s(plus(X, Y))) |
| active(times(0, Y)) | → | mark(0) | | active(times(s(X), Y)) | → | mark(plus(Y, times(X, Y))) |
| active(square(X)) | → | mark(times(X, X)) | | active(s(X)) | → | s(active(X)) |
| active(posrecip(X)) | → | posrecip(active(X)) | | active(negrecip(X)) | → | negrecip(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(rcons(X1, X2)) | → | rcons(active(X1), X2) |
| active(rcons(X1, X2)) | → | rcons(X1, active(X2)) | | active(from(X)) | → | from(active(X)) |
| active(2ndspos(X1, X2)) | → | 2ndspos(active(X1), X2) | | active(2ndspos(X1, X2)) | → | 2ndspos(X1, active(X2)) |
| active(2ndsneg(X1, X2)) | → | 2ndsneg(active(X1), X2) | | active(2ndsneg(X1, X2)) | → | 2ndsneg(X1, active(X2)) |
| active(pi(X)) | → | pi(active(X)) | | active(plus(X1, X2)) | → | plus(active(X1), X2) |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | | active(times(X1, X2)) | → | times(active(X1), X2) |
| active(times(X1, X2)) | → | times(X1, active(X2)) | | active(square(X)) | → | square(active(X)) |
| s(mark(X)) | → | mark(s(X)) | | posrecip(mark(X)) | → | mark(posrecip(X)) |
| negrecip(mark(X)) | → | mark(negrecip(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| rcons(mark(X1), X2) | → | mark(rcons(X1, X2)) | | rcons(X1, mark(X2)) | → | mark(rcons(X1, X2)) |
| from(mark(X)) | → | mark(from(X)) | | 2ndspos(mark(X1), X2) | → | mark(2ndspos(X1, X2)) |
| 2ndspos(X1, mark(X2)) | → | mark(2ndspos(X1, X2)) | | 2ndsneg(mark(X1), X2) | → | mark(2ndsneg(X1, X2)) |
| 2ndsneg(X1, mark(X2)) | → | mark(2ndsneg(X1, X2)) | | pi(mark(X)) | → | mark(pi(X)) |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) |
| times(mark(X1), X2) | → | mark(times(X1, X2)) | | times(X1, mark(X2)) | → | mark(times(X1, X2)) |
| square(mark(X)) | → | mark(square(X)) | | proper(0) | → | ok(0) |
| proper(s(X)) | → | s(proper(X)) | | proper(posrecip(X)) | → | posrecip(proper(X)) |
| proper(negrecip(X)) | → | negrecip(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(rnil) | → | ok(rnil) |
| proper(rcons(X1, X2)) | → | rcons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(2ndspos(X1, X2)) | → | 2ndspos(proper(X1), proper(X2)) | | proper(2ndsneg(X1, X2)) | → | 2ndsneg(proper(X1), proper(X2)) |
| proper(pi(X)) | → | pi(proper(X)) | | proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) |
| proper(times(X1, X2)) | → | times(proper(X1), proper(X2)) | | proper(square(X)) | → | square(proper(X)) |
| s(ok(X)) | → | ok(s(X)) | | posrecip(ok(X)) | → | ok(posrecip(X)) |
| negrecip(ok(X)) | → | ok(negrecip(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| rcons(ok(X1), ok(X2)) | → | ok(rcons(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| 2ndspos(ok(X1), ok(X2)) | → | ok(2ndspos(X1, X2)) | | 2ndsneg(ok(X1), ok(X2)) | → | ok(2ndsneg(X1, X2)) |
| pi(ok(X)) | → | ok(pi(X)) | | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) |
| times(ok(X1), ok(X2)) | → | ok(times(X1, X2)) | | square(ok(X)) | → | ok(square(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: plus, posrecip, negrecip, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, proper, square, pi, top, nil, cons
Strategy
Function Precedence
plus = posrecip = negrecip = rnil = mark = from = rcons = 2ndspos = 0 = s = times = 2ndsneg = active = plus# = ok = square = proper = pi = top = cons = nil
Argument Filtering
plus: all arguments are removed from plus
posrecip: all arguments are removed from posrecip
negrecip: all arguments are removed from negrecip
rnil: all arguments are removed from rnil
mark: 1
from: all arguments are removed from from
rcons: all arguments are removed from rcons
2ndspos: all arguments are removed from 2ndspos
0: all arguments are removed from 0
s: all arguments are removed from s
times: all arguments are removed from times
2ndsneg: all arguments are removed from 2ndsneg
active: all arguments are removed from active
plus#: 1 2
ok: all arguments are removed from ok
square: collapses to 1
proper: all arguments are removed from proper
pi: collapses to 1
top: all arguments are removed from top
cons: all arguments are removed from cons
nil: all arguments are removed from nil
Status
plus: multiset
posrecip: multiset
negrecip: multiset
rnil: multiset
mark: multiset
from: multiset
rcons: multiset
2ndspos: multiset
0: multiset
s: multiset
times: multiset
2ndsneg: multiset
active: multiset
plus#: multiset
ok: multiset
proper: multiset
top: multiset
cons: multiset
nil: multiset
Usable Rules
There are no usable rules.
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.
| plus#(X1, mark(X2)) → plus#(X1, X2) |
Problem 15: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| active#(from(X)) | → | active#(X) | | active#(2ndspos(X1, X2)) | → | active#(X2) |
| active#(2ndsneg(X1, X2)) | → | active#(X2) | | active#(pi(X)) | → | active#(X) |
| active#(posrecip(X)) | → | active#(X) | | active#(times(X1, X2)) | → | active#(X1) |
| active#(plus(X1, X2)) | → | active#(X1) | | active#(square(X)) | → | active#(X) |
| active#(rcons(X1, X2)) | → | active#(X2) | | active#(s(X)) | → | active#(X) |
| active#(2ndspos(X1, X2)) | → | active#(X1) | | active#(negrecip(X)) | → | active#(X) |
| active#(times(X1, X2)) | → | active#(X2) | | active#(plus(X1, X2)) | → | active#(X2) |
| active#(2ndsneg(X1, X2)) | → | active#(X1) | | active#(rcons(X1, X2)) | → | active#(X1) |
| active#(cons(X1, X2)) | → | active#(X1) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) | | active(2ndsneg(0, Z)) | → | mark(rnil) |
| active(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(negrecip(Y), 2ndspos(N, Z))) | | active(pi(X)) | → | mark(2ndspos(X, from(0))) |
| active(plus(0, Y)) | → | mark(Y) | | active(plus(s(X), Y)) | → | mark(s(plus(X, Y))) |
| active(times(0, Y)) | → | mark(0) | | active(times(s(X), Y)) | → | mark(plus(Y, times(X, Y))) |
| active(square(X)) | → | mark(times(X, X)) | | active(s(X)) | → | s(active(X)) |
| active(posrecip(X)) | → | posrecip(active(X)) | | active(negrecip(X)) | → | negrecip(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(rcons(X1, X2)) | → | rcons(active(X1), X2) |
| active(rcons(X1, X2)) | → | rcons(X1, active(X2)) | | active(from(X)) | → | from(active(X)) |
| active(2ndspos(X1, X2)) | → | 2ndspos(active(X1), X2) | | active(2ndspos(X1, X2)) | → | 2ndspos(X1, active(X2)) |
| active(2ndsneg(X1, X2)) | → | 2ndsneg(active(X1), X2) | | active(2ndsneg(X1, X2)) | → | 2ndsneg(X1, active(X2)) |
| active(pi(X)) | → | pi(active(X)) | | active(plus(X1, X2)) | → | plus(active(X1), X2) |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | | active(times(X1, X2)) | → | times(active(X1), X2) |
| active(times(X1, X2)) | → | times(X1, active(X2)) | | active(square(X)) | → | square(active(X)) |
| s(mark(X)) | → | mark(s(X)) | | posrecip(mark(X)) | → | mark(posrecip(X)) |
| negrecip(mark(X)) | → | mark(negrecip(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| rcons(mark(X1), X2) | → | mark(rcons(X1, X2)) | | rcons(X1, mark(X2)) | → | mark(rcons(X1, X2)) |
| from(mark(X)) | → | mark(from(X)) | | 2ndspos(mark(X1), X2) | → | mark(2ndspos(X1, X2)) |
| 2ndspos(X1, mark(X2)) | → | mark(2ndspos(X1, X2)) | | 2ndsneg(mark(X1), X2) | → | mark(2ndsneg(X1, X2)) |
| 2ndsneg(X1, mark(X2)) | → | mark(2ndsneg(X1, X2)) | | pi(mark(X)) | → | mark(pi(X)) |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) |
| times(mark(X1), X2) | → | mark(times(X1, X2)) | | times(X1, mark(X2)) | → | mark(times(X1, X2)) |
| square(mark(X)) | → | mark(square(X)) | | proper(0) | → | ok(0) |
| proper(s(X)) | → | s(proper(X)) | | proper(posrecip(X)) | → | posrecip(proper(X)) |
| proper(negrecip(X)) | → | negrecip(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(rnil) | → | ok(rnil) |
| proper(rcons(X1, X2)) | → | rcons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(2ndspos(X1, X2)) | → | 2ndspos(proper(X1), proper(X2)) | | proper(2ndsneg(X1, X2)) | → | 2ndsneg(proper(X1), proper(X2)) |
| proper(pi(X)) | → | pi(proper(X)) | | proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) |
| proper(times(X1, X2)) | → | times(proper(X1), proper(X2)) | | proper(square(X)) | → | square(proper(X)) |
| s(ok(X)) | → | ok(s(X)) | | posrecip(ok(X)) | → | ok(posrecip(X)) |
| negrecip(ok(X)) | → | ok(negrecip(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| rcons(ok(X1), ok(X2)) | → | ok(rcons(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| 2ndspos(ok(X1), ok(X2)) | → | ok(2ndspos(X1, X2)) | | 2ndsneg(ok(X1), ok(X2)) | → | ok(2ndsneg(X1, X2)) |
| pi(ok(X)) | → | ok(pi(X)) | | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) |
| times(ok(X1), ok(X2)) | → | ok(times(X1, X2)) | | square(ok(X)) | → | ok(square(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: plus, posrecip, negrecip, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, square, proper, pi, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| active#(from(X)) | → | active#(X) | | active#(2ndspos(X1, X2)) | → | active#(X2) |
| active#(2ndsneg(X1, X2)) | → | active#(X2) | | active#(pi(X)) | → | active#(X) |
| active#(posrecip(X)) | → | active#(X) | | active#(times(X1, X2)) | → | active#(X1) |
| active#(plus(X1, X2)) | → | active#(X1) | | active#(square(X)) | → | active#(X) |
| active#(rcons(X1, X2)) | → | active#(X2) | | active#(s(X)) | → | active#(X) |
| active#(2ndspos(X1, X2)) | → | active#(X1) | | active#(negrecip(X)) | → | active#(X) |
| active#(times(X1, X2)) | → | active#(X2) | | active#(plus(X1, X2)) | → | active#(X2) |
| active#(2ndsneg(X1, X2)) | → | active#(X1) | | active#(rcons(X1, X2)) | → | active#(X1) |
| active#(cons(X1, X2)) | → | active#(X1) |
Problem 16: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| proper#(cons(X1, X2)) | → | proper#(X1) | | proper#(2ndsneg(X1, X2)) | → | proper#(X1) |
| proper#(cons(X1, X2)) | → | proper#(X2) | | proper#(square(X)) | → | proper#(X) |
| proper#(negrecip(X)) | → | proper#(X) | | proper#(times(X1, X2)) | → | proper#(X2) |
| proper#(rcons(X1, X2)) | → | proper#(X2) | | proper#(posrecip(X)) | → | proper#(X) |
| proper#(2ndspos(X1, X2)) | → | proper#(X2) | | proper#(s(X)) | → | proper#(X) |
| proper#(times(X1, X2)) | → | proper#(X1) | | proper#(2ndspos(X1, X2)) | → | proper#(X1) |
| proper#(2ndsneg(X1, X2)) | → | proper#(X2) | | proper#(plus(X1, X2)) | → | proper#(X1) |
| proper#(pi(X)) | → | proper#(X) | | proper#(rcons(X1, X2)) | → | proper#(X1) |
| proper#(plus(X1, X2)) | → | proper#(X2) | | proper#(from(X)) | → | proper#(X) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) | | active(2ndsneg(0, Z)) | → | mark(rnil) |
| active(2ndsneg(s(N), cons(X, cons(Y, Z)))) | → | mark(rcons(negrecip(Y), 2ndspos(N, Z))) | | active(pi(X)) | → | mark(2ndspos(X, from(0))) |
| active(plus(0, Y)) | → | mark(Y) | | active(plus(s(X), Y)) | → | mark(s(plus(X, Y))) |
| active(times(0, Y)) | → | mark(0) | | active(times(s(X), Y)) | → | mark(plus(Y, times(X, Y))) |
| active(square(X)) | → | mark(times(X, X)) | | active(s(X)) | → | s(active(X)) |
| active(posrecip(X)) | → | posrecip(active(X)) | | active(negrecip(X)) | → | negrecip(active(X)) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(rcons(X1, X2)) | → | rcons(active(X1), X2) |
| active(rcons(X1, X2)) | → | rcons(X1, active(X2)) | | active(from(X)) | → | from(active(X)) |
| active(2ndspos(X1, X2)) | → | 2ndspos(active(X1), X2) | | active(2ndspos(X1, X2)) | → | 2ndspos(X1, active(X2)) |
| active(2ndsneg(X1, X2)) | → | 2ndsneg(active(X1), X2) | | active(2ndsneg(X1, X2)) | → | 2ndsneg(X1, active(X2)) |
| active(pi(X)) | → | pi(active(X)) | | active(plus(X1, X2)) | → | plus(active(X1), X2) |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | | active(times(X1, X2)) | → | times(active(X1), X2) |
| active(times(X1, X2)) | → | times(X1, active(X2)) | | active(square(X)) | → | square(active(X)) |
| s(mark(X)) | → | mark(s(X)) | | posrecip(mark(X)) | → | mark(posrecip(X)) |
| negrecip(mark(X)) | → | mark(negrecip(X)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| rcons(mark(X1), X2) | → | mark(rcons(X1, X2)) | | rcons(X1, mark(X2)) | → | mark(rcons(X1, X2)) |
| from(mark(X)) | → | mark(from(X)) | | 2ndspos(mark(X1), X2) | → | mark(2ndspos(X1, X2)) |
| 2ndspos(X1, mark(X2)) | → | mark(2ndspos(X1, X2)) | | 2ndsneg(mark(X1), X2) | → | mark(2ndsneg(X1, X2)) |
| 2ndsneg(X1, mark(X2)) | → | mark(2ndsneg(X1, X2)) | | pi(mark(X)) | → | mark(pi(X)) |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) |
| times(mark(X1), X2) | → | mark(times(X1, X2)) | | times(X1, mark(X2)) | → | mark(times(X1, X2)) |
| square(mark(X)) | → | mark(square(X)) | | proper(0) | → | ok(0) |
| proper(s(X)) | → | s(proper(X)) | | proper(posrecip(X)) | → | posrecip(proper(X)) |
| proper(negrecip(X)) | → | negrecip(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(rnil) | → | ok(rnil) |
| proper(rcons(X1, X2)) | → | rcons(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(2ndspos(X1, X2)) | → | 2ndspos(proper(X1), proper(X2)) | | proper(2ndsneg(X1, X2)) | → | 2ndsneg(proper(X1), proper(X2)) |
| proper(pi(X)) | → | pi(proper(X)) | | proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) |
| proper(times(X1, X2)) | → | times(proper(X1), proper(X2)) | | proper(square(X)) | → | square(proper(X)) |
| s(ok(X)) | → | ok(s(X)) | | posrecip(ok(X)) | → | ok(posrecip(X)) |
| negrecip(ok(X)) | → | ok(negrecip(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| rcons(ok(X1), ok(X2)) | → | ok(rcons(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| 2ndspos(ok(X1), ok(X2)) | → | ok(2ndspos(X1, X2)) | | 2ndsneg(ok(X1), ok(X2)) | → | ok(2ndsneg(X1, X2)) |
| pi(ok(X)) | → | ok(pi(X)) | | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) |
| times(ok(X1), ok(X2)) | → | ok(times(X1, X2)) | | square(ok(X)) | → | ok(square(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: plus, posrecip, negrecip, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, square, proper, pi, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| proper#(cons(X1, X2)) | → | proper#(X1) | | proper#(2ndsneg(X1, X2)) | → | proper#(X1) |
| proper#(cons(X1, X2)) | → | proper#(X2) | | proper#(square(X)) | → | proper#(X) |
| proper#(negrecip(X)) | → | proper#(X) | | proper#(times(X1, X2)) | → | proper#(X2) |
| proper#(rcons(X1, X2)) | → | proper#(X2) | | proper#(2ndspos(X1, X2)) | → | proper#(X2) |
| proper#(posrecip(X)) | → | proper#(X) | | proper#(s(X)) | → | proper#(X) |
| proper#(times(X1, X2)) | → | proper#(X1) | | proper#(2ndspos(X1, X2)) | → | proper#(X1) |
| proper#(2ndsneg(X1, X2)) | → | proper#(X2) | | proper#(plus(X1, X2)) | → | proper#(X1) |
| proper#(pi(X)) | → | proper#(X) | | proper#(plus(X1, X2)) | → | proper#(X2) |
| proper#(rcons(X1, X2)) | → | proper#(X1) | | proper#(from(X)) | → | proper#(X) |