TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60061 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (18998ms).
| – Problem 2 was processed with processor SubtermCriterion (2ms).
| – Problem 3 was processed with processor SubtermCriterion (2ms).
| | – Problem 18 was processed with processor PolynomialLinearRange4iUR (57ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| | – Problem 19 was processed with processor PolynomialLinearRange4iUR (81ms).
| – Problem 5 was processed with processor SubtermCriterion (3ms).
| – Problem 6 was processed with processor SubtermCriterion (2ms).
| | – Problem 20 was processed with processor PolynomialLinearRange4iUR (43ms).
| – Problem 7 was processed with processor SubtermCriterion (1ms).
| | – Problem 21 was processed with processor PolynomialLinearRange4iUR (33ms).
| – Problem 8 was processed with processor SubtermCriterion (5ms).
| – Problem 9 was processed with processor SubtermCriterion (2ms).
| | – Problem 22 was processed with processor PolynomialLinearRange4iUR (25ms).
| – Problem 10 was processed with processor SubtermCriterion (1ms).
| | – Problem 23 was processed with processor PolynomialLinearRange4iUR (21ms).
| – Problem 11 was processed with processor SubtermCriterion (4ms).
| – Problem 12 was processed with processor SubtermCriterion (1ms).
| – Problem 13 was processed with processor SubtermCriterion (2ms).
| – Problem 14 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (6ms), PolynomialLinearRange4iUR (1428ms), DependencyGraph (6ms), PolynomialLinearRange4iUR (timeout), DependencyGraph (7ms), PolynomialLinearRange8NegiUR (timeout)].
| – Problem 15 was processed with processor SubtermCriterion (43ms).
| – Problem 16 was processed with processor SubtermCriterion (1ms).
| – Problem 17 was processed with processor SubtermCriterion (1ms).
The following open problems remain:
Open Dependency Pair Problem 14
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, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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#(cons(X1, X2)) | → | proper#(X1) | | proper#(2ndsneg(X1, X2)) | → | proper#(X1) |
| proper#(square(X)) | → | proper#(X) | | active#(pi(X)) | → | from#(0) |
| active#(2ndsneg(s(N), cons(X, Z))) | → | 2ndsneg#(s(N), cons2(X, Z)) | | 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)) | | active#(2ndsneg(s(N), cons2(X, cons(Y, Z)))) | → | negrecip#(Y) |
| top#(mark(X)) | → | proper#(X) | | active#(posrecip(X)) | → | posrecip#(active(X)) |
| active#(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | posrecip#(Y) | | active#(2ndsneg(X1, X2)) | → | 2ndsneg#(X1, active(X2)) |
| 2ndspos#(X1, mark(X2)) | → | 2ndspos#(X1, X2) | | active#(pi(X)) | → | pi#(active(X)) |
| negrecip#(ok(X)) | → | negrecip#(X) | | active#(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | rcons#(posrecip(Y), 2ndsneg(N, Z)) |
| 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) |
| active#(2ndsneg(s(N), cons2(X, cons(Y, Z)))) | → | 2ndspos#(N, Z) | | 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) |
| active#(cons2(X1, X2)) | → | active#(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) | | active#(cons2(X1, X2)) | → | cons2#(X1, active(X2)) |
| active#(2ndspos(s(N), cons(X, Z))) | → | s#(N) | | times#(ok(X1), ok(X2)) | → | times#(X1, X2) |
| square#(mark(X)) | → | square#(X) | | active#(2ndspos(s(N), cons(X, Z))) | → | 2ndspos#(s(N), cons2(X, Z)) |
| proper#(from(X)) | → | from#(proper(X)) | | proper#(cons2(X1, X2)) | → | proper#(X2) |
| times#(X1, mark(X2)) | → | times#(X1, X2) | | active#(pi(X)) | → | 2ndspos#(X, from(0)) |
| proper#(rcons(X1, X2)) | → | proper#(X1) | | plus#(ok(X1), ok(X2)) | → | plus#(X1, X2) |
| active#(plus(s(X), Y)) | → | plus#(X, Y) | | posrecip#(mark(X)) | → | posrecip#(X) |
| 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#(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)) |
| proper#(cons2(X1, X2)) | → | cons2#(proper(X1), proper(X2)) | | active#(2ndsneg(X1, X2)) | → | active#(X1) |
| rcons#(X1, mark(X2)) | → | rcons#(X1, X2) | | active#(2ndsneg(s(N), cons(X, Z))) | → | s#(N) |
| active#(2ndsneg(s(N), cons2(X, cons(Y, Z)))) | → | rcons#(negrecip(Y), 2ndspos(N, Z)) | | active#(from(X)) | → | from#(s(X)) |
| top#(ok(X)) | → | top#(active(X)) | | active#(square(X)) | → | square#(active(X)) |
| active#(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | 2ndsneg#(N, Z) | | cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
| proper#(times(X1, X2)) | → | proper#(X2) | | active#(rcons(X1, X2)) | → | rcons#(active(X1), 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#(cons2(X1, X2)) | → | proper#(X1) |
| 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) | | cons2#(X1, mark(X2)) | → | cons2#(X1, X2) |
| active#(from(X)) | → | s#(X) | | proper#(rcons(X1, X2)) | → | rcons#(proper(X1), proper(X2)) |
| proper#(square(X)) | → | square#(proper(X)) | | proper#(s(X)) | → | proper#(X) |
| active#(plus(X1, X2)) | → | active#(X1) | | proper#(times(X1, X2)) | → | times#(proper(X1), proper(X2)) |
| active#(times(X1, X2)) | → | active#(X2) | | active#(2ndsneg(s(N), cons(X, Z))) | → | cons2#(X, Z) |
| active#(plus(s(X), Y)) | → | s#(plus(X, Y)) | | active#(cons(X1, X2)) | → | active#(X1) |
| cons2#(ok(X1), ok(X2)) | → | cons2#(X1, X2) | | active#(2ndspos(s(N), cons(X, Z))) | → | cons2#(X, Z) |
| 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#(cons(X1, X2)) | → | cons#(proper(X1), proper(X2)) | | proper#(times(X1, X2)) | → | proper#(X1) |
| 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) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, ok, square, proper, pi, cons, nil, top
Strategy
The following SCCs where found
| cons2#(ok(X1), ok(X2)) → cons2#(X1, X2) | cons2#(X1, mark(X2)) → cons2#(X1, X2) |
| 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#(2ndsneg(X1, X2)) → active#(X1) |
| active#(plus(X1, X2)) → active#(X2) | active#(rcons(X1, X2)) → active#(X1) |
| active#(cons2(X1, X2)) → active#(X2) | active#(cons(X1, X2)) → active#(X1) |
| 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#(cons2(X1, X2)) → proper#(X1) |
| proper#(cons2(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) |
| 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) |
| 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 2: 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, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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 3: 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, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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 18: 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, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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
- cons2(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
- rcons#(x,y): y + x + 1
- 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 4: 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, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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 19: PolynomialLinearRange4iUR
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, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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
- 2ndsneg#(x,y): y + x + 1
- 2ndspos(x,y): 0
- active(x): 0
- cons(x,y): 0
- cons2(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:
| 2ndsneg#(X1, mark(X2)) | → | 2ndsneg#(X1, X2) |
Problem 5: 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, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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 6: 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, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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 20: PolynomialLinearRange4iUR
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, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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
- cons2(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
- plus#(x,y): y + x + 1
- 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:
| plus#(X1, mark(X2)) | → | plus#(X1, X2) |
Problem 7: 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, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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 21: 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, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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): 2y
- active(x): 0
- cons(x,y): 0
- cons2(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
- 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 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| 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#(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#(cons2(X1, X2)) | → | proper#(X1) |
| proper#(cons2(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) |
Rewrite Rules
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(2ndspos(0, Z)) | → | mark(rnil) |
| active(2ndspos(s(N), cons(X, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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#(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#(cons2(X1, X2)) | → | proper#(X2) |
| proper#(cons2(X1, X2)) | → | proper#(X1) | | 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) |
Problem 9: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons2#(ok(X1), ok(X2)) | → | cons2#(X1, X2) | | cons2#(X1, mark(X2)) | → | cons2#(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, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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:
| cons2#(ok(X1), ok(X2)) | → | cons2#(X1, X2) |
Problem 22: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| cons2#(X1, mark(X2)) | → | cons2#(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, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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
- cons2(x,y): 0
- cons2#(x,y): y + x + 1
- 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:
| cons2#(X1, mark(X2)) | → | cons2#(X1, X2) |
Problem 10: 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, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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 23: PolynomialLinearRange4iUR
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, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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
- cons2(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
- times#(x,y): y + x + 1
- 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:
| times#(X1, mark(X2)) | → | times#(X1, X2) |
Problem 11: 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, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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 12: 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, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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 13: 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, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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 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#(2ndsneg(X1, X2)) | → | active#(X1) |
| active#(plus(X1, X2)) | → | active#(X2) | | active#(rcons(X1, X2)) | → | active#(X1) |
| active#(cons2(X1, X2)) | → | active#(X2) | | 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, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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#(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#(cons2(X1, X2)) | → | active#(X2) |
| active#(rcons(X1, X2)) | → | active#(X1) | | active#(cons(X1, X2)) | → | active#(X1) |
Problem 16: 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, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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 17: 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, Z))) | → | mark(2ndspos(s(N), cons2(X, Z))) | | active(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| active(2ndsneg(0, Z)) | → | mark(rnil) | | active(2ndsneg(s(N), cons(X, Z))) | → | mark(2ndsneg(s(N), cons2(X, Z))) |
| active(2ndsneg(s(N), cons2(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(cons2(X1, X2)) | → | cons2(X1, active(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)) | | cons2(X1, mark(X2)) | → | mark(cons2(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(cons2(X1, X2)) | → | cons2(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)) | | cons2(ok(X1), ok(X2)) | → | ok(cons2(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, cons2, 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) |