TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60001 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (17496ms).
| – Problem 2 was processed with processor SubtermCriterion (2ms).
| | – Problem 16 was processed with processor PolynomialLinearRange4iUR (39ms).
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| | – Problem 17 was processed with processor PolynomialLinearRange4iUR (125ms).
| | | – Problem 23 was processed with processor PolynomialLinearRange4iUR (20ms).
| – Problem 4 was processed with processor SubtermCriterion (2ms).
| | – Problem 18 was processed with processor PolynomialLinearRange4iUR (70ms).
| – Problem 5 was processed with processor SubtermCriterion (1ms).
| – Problem 6 was processed with processor SubtermCriterion (4ms).
| – Problem 7 was processed with processor SubtermCriterion (1ms).
| – Problem 8 was processed with processor SubtermCriterion (1ms).
| | – Problem 19 was processed with processor PolynomialLinearRange4iUR (32ms).
| – Problem 9 was processed with processor SubtermCriterion (2ms).
| – Problem 10 was processed with processor SubtermCriterion (3ms).
| | – Problem 20 was processed with processor PolynomialLinearRange4iUR (26ms).
| – Problem 11 was processed with processor SubtermCriterion (1ms).
| | – Problem 21 was processed with processor PolynomialLinearRange4iUR (26ms).
| | | – Problem 24 was processed with processor PolynomialLinearRange4iUR (16ms).
| – Problem 12 was processed with processor SubtermCriterion (2ms).
| – Problem 13 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (3152ms), PolynomialLinearRange4iUR (1283ms), DependencyGraph (3034ms), PolynomialLinearRange4iUR (2533ms), DependencyGraph (3157ms), PolynomialLinearRange4iUR (timeout), DependencyGraph (3170ms), PolynomialLinearRange8NegiUR (timeout)].
| – Problem 14 was processed with processor SubtermCriterion (5ms).
| | – Problem 22 was processed with processor PolynomialLinearRange4iUR (70ms).
| | | – Problem 25 was processed with processor PolynomialLinearRange4iUR (60ms).
| – Problem 15 was processed with processor SubtermCriterion (2ms).
The following open problems remain:
Open Dependency Pair Problem 13
Dependency Pairs
| active#(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark#(rcons(posrecip(Y), 2ndsneg(N, Z))) | | mark#(cons(X1, X2)) | → | active#(cons(mark(X1), X2)) |
| mark#(2ndspos(X1, X2)) | → | mark#(X2) | | active#(2ndsneg(0, Z)) | → | mark#(rnil) |
| mark#(square(X)) | → | mark#(X) | | active#(2ndsneg(s(N), cons(X, Z))) | → | mark#(2ndsneg(s(N), cons2(X, Z))) |
| mark#(pi(X)) | → | mark#(X) | | mark#(cons2(X1, X2)) | → | mark#(X2) |
| active#(2ndsneg(s(N), cons2(X, cons(Y, Z)))) | → | mark#(rcons(negrecip(Y), 2ndspos(N, Z))) | | mark#(pi(X)) | → | active#(pi(mark(X))) |
| active#(2ndspos(s(N), cons(X, Z))) | → | mark#(2ndspos(s(N), cons2(X, Z))) | | mark#(times(X1, X2)) | → | mark#(X2) |
| mark#(negrecip(X)) | → | mark#(X) | | mark#(2ndsneg(X1, X2)) | → | mark#(X1) |
| active#(plus(s(X), Y)) | → | mark#(s(plus(X, Y))) | | mark#(plus(X1, X2)) | → | mark#(X2) |
| mark#(times(X1, X2)) | → | mark#(X1) | | mark#(2ndsneg(X1, X2)) | → | mark#(X2) |
| mark#(s(X)) | → | mark#(X) | | mark#(rnil) | → | active#(rnil) |
| active#(times(0, Y)) | → | mark#(0) | | mark#(square(X)) | → | active#(square(mark(X))) |
| active#(times(s(X), Y)) | → | mark#(plus(Y, times(X, Y))) | | mark#(2ndspos(X1, X2)) | → | active#(2ndspos(mark(X1), mark(X2))) |
| mark#(0) | → | active#(0) | | active#(plus(0, Y)) | → | mark#(Y) |
| mark#(plus(X1, X2)) | → | active#(plus(mark(X1), mark(X2))) | | mark#(cons2(X1, X2)) | → | active#(cons2(X1, mark(X2))) |
| mark#(s(X)) | → | active#(s(mark(X))) | | mark#(rcons(X1, X2)) | → | active#(rcons(mark(X1), mark(X2))) |
| mark#(negrecip(X)) | → | active#(negrecip(mark(X))) | | mark#(times(X1, X2)) | → | active#(times(mark(X1), mark(X2))) |
| mark#(rcons(X1, X2)) | → | mark#(X2) | | mark#(2ndsneg(X1, X2)) | → | active#(2ndsneg(mark(X1), mark(X2))) |
| mark#(from(X)) | → | mark#(X) | | active#(square(X)) | → | mark#(times(X, X)) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | mark#(posrecip(X)) | → | active#(posrecip(mark(X))) |
| active#(from(X)) | → | mark#(cons(X, from(s(X)))) | | mark#(plus(X1, X2)) | → | mark#(X1) |
| active#(2ndspos(0, Z)) | → | mark#(rnil) | | mark#(from(X)) | → | active#(from(mark(X))) |
| mark#(posrecip(X)) | → | mark#(X) | | mark#(2ndspos(X1, X2)) | → | mark#(X1) |
| mark#(rcons(X1, X2)) | → | mark#(X1) | | active#(pi(X)) | → | mark#(2ndspos(X, from(0))) |
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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(2ndsneg(X1, X2)) | → | 2ndsneg#(mark(X1), mark(X2)) | | active#(2ndsneg(0, Z)) | → | mark#(rnil) |
| active#(pi(X)) | → | from#(0) | | active#(2ndsneg(s(N), cons(X, Z))) | → | 2ndsneg#(s(N), cons2(X, Z)) |
| rcons#(X1, active(X2)) | → | rcons#(X1, X2) | | mark#(pi(X)) | → | mark#(X) |
| mark#(negrecip(X)) | → | negrecip#(mark(X)) | | mark#(pi(X)) | → | active#(pi(mark(X))) |
| mark#(times(X1, X2)) | → | mark#(X2) | | mark#(negrecip(X)) | → | mark#(X) |
| mark#(2ndsneg(X1, X2)) | → | mark#(X1) | | active#(plus(s(X), Y)) | → | mark#(s(plus(X, Y))) |
| times#(active(X1), X2) | → | times#(X1, X2) | | mark#(times(X1, X2)) | → | mark#(X1) |
| mark#(s(X)) | → | mark#(X) | | active#(2ndsneg(s(N), cons2(X, cons(Y, Z)))) | → | negrecip#(Y) |
| active#(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | posrecip#(Y) | | mark#(plus(X1, X2)) | → | active#(plus(mark(X1), mark(X2))) |
| mark#(cons2(X1, X2)) | → | active#(cons2(X1, mark(X2))) | | 2ndspos#(X1, mark(X2)) | → | 2ndspos#(X1, X2) |
| mark#(rcons(X1, X2)) | → | mark#(X2) | | active#(square(X)) | → | mark#(times(X, X)) |
| active#(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | rcons#(posrecip(Y), 2ndsneg(N, Z)) | | mark#(pi(X)) | → | pi#(mark(X)) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | rcons#(mark(X1), X2) | → | rcons#(X1, X2) |
| active#(square(X)) | → | times#(X, X) | | times#(mark(X1), X2) | → | times#(X1, X2) |
| active#(from(X)) | → | mark#(cons(X, from(s(X)))) | | negrecip#(mark(X)) | → | negrecip#(X) |
| active#(2ndsneg(s(N), cons2(X, cons(Y, Z)))) | → | 2ndspos#(N, Z) | | 2ndspos#(mark(X1), X2) | → | 2ndspos#(X1, X2) |
| mark#(2ndspos(X1, X2)) | → | 2ndspos#(mark(X1), mark(X2)) | | plus#(mark(X1), X2) | → | plus#(X1, X2) |
| plus#(active(X1), X2) | → | plus#(X1, X2) | | active#(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | mark#(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | mark#(rcons(X1, X2)) | → | rcons#(mark(X1), mark(X2)) |
| active#(2ndsneg(s(N), cons(X, Z))) | → | mark#(2ndsneg(s(N), cons2(X, Z))) | | from#(mark(X)) | → | from#(X) |
| active#(2ndsneg(s(N), cons2(X, cons(Y, Z)))) | → | mark#(rcons(negrecip(Y), 2ndspos(N, Z))) | | active#(2ndspos(s(N), cons(X, Z))) | → | mark#(2ndspos(s(N), cons2(X, Z))) |
| active#(2ndspos(s(N), cons(X, Z))) | → | s#(N) | | active#(2ndspos(s(N), cons(X, Z))) | → | 2ndspos#(s(N), cons2(X, Z)) |
| square#(mark(X)) | → | square#(X) | | cons2#(active(X1), X2) | → | cons2#(X1, X2) |
| times#(X1, mark(X2)) | → | times#(X1, X2) | | cons#(X1, mark(X2)) | → | cons#(X1, X2) |
| active#(pi(X)) | → | 2ndspos#(X, from(0)) | | active#(times(0, Y)) | → | mark#(0) |
| mark#(square(X)) | → | square#(mark(X)) | | mark#(2ndspos(X1, X2)) | → | active#(2ndspos(mark(X1), mark(X2))) |
| active#(plus(s(X), Y)) | → | plus#(X, Y) | | posrecip#(mark(X)) | → | posrecip#(X) |
| mark#(0) | → | active#(0) | | mark#(s(X)) | → | active#(s(mark(X))) |
| mark#(negrecip(X)) | → | active#(negrecip(mark(X))) | | active#(times(s(X), Y)) | → | plus#(Y, times(X, Y)) |
| mark#(posrecip(X)) | → | active#(posrecip(mark(X))) | | cons#(active(X1), X2) | → | cons#(X1, X2) |
| active#(2ndspos(0, Z)) | → | mark#(rnil) | | 2ndsneg#(X1, mark(X2)) | → | 2ndsneg#(X1, X2) |
| 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)) |
| mark#(cons(X1, X2)) | → | active#(cons(mark(X1), X2)) | | mark#(2ndspos(X1, X2)) | → | mark#(X2) |
| active#(2ndspos(s(N), cons2(X, cons(Y, Z)))) | → | 2ndsneg#(N, Z) | | mark#(square(X)) | → | mark#(X) |
| 2ndspos#(X1, active(X2)) | → | 2ndspos#(X1, X2) | | mark#(cons2(X1, X2)) | → | mark#(X2) |
| mark#(s(X)) | → | s#(mark(X)) | | pi#(mark(X)) | → | pi#(X) |
| plus#(X1, mark(X2)) | → | plus#(X1, X2) | | mark#(2ndsneg(X1, X2)) | → | mark#(X2) |
| mark#(rnil) | → | active#(rnil) | | pi#(active(X)) | → | pi#(X) |
| mark#(posrecip(X)) | → | posrecip#(mark(X)) | | active#(times(s(X), Y)) | → | mark#(plus(Y, times(X, Y))) |
| active#(plus(0, Y)) | → | mark#(Y) | | 2ndspos#(active(X1), X2) | → | 2ndspos#(X1, X2) |
| mark#(2ndsneg(X1, X2)) | → | active#(2ndsneg(mark(X1), mark(X2))) | | mark#(from(X)) | → | mark#(X) |
| posrecip#(active(X)) | → | posrecip#(X) | | cons2#(X1, mark(X2)) | → | cons2#(X1, X2) |
| mark#(plus(X1, X2)) | → | mark#(X1) | | active#(from(X)) | → | s#(X) |
| cons#(X1, active(X2)) | → | cons#(X1, X2) | | mark#(from(X)) | → | from#(mark(X)) |
| mark#(from(X)) | → | active#(from(mark(X))) | | plus#(X1, active(X2)) | → | plus#(X1, X2) |
| mark#(posrecip(X)) | → | mark#(X) | | from#(active(X)) | → | from#(X) |
| active#(2ndsneg(s(N), cons(X, Z))) | → | cons2#(X, Z) | | active#(plus(s(X), Y)) | → | s#(plus(X, Y)) |
| active#(2ndspos(s(N), cons(X, Z))) | → | cons2#(X, Z) | | square#(active(X)) | → | square#(X) |
| active#(times(s(X), Y)) | → | times#(X, Y) | | mark#(plus(X1, X2)) | → | mark#(X2) |
| 2ndsneg#(active(X1), X2) | → | 2ndsneg#(X1, X2) | | negrecip#(active(X)) | → | negrecip#(X) |
| mark#(times(X1, X2)) | → | times#(mark(X1), mark(X2)) | | active#(from(X)) | → | cons#(X, from(s(X))) |
| 2ndsneg#(mark(X1), X2) | → | 2ndsneg#(X1, X2) | | mark#(cons(X1, X2)) | → | cons#(mark(X1), X2) |
| mark#(square(X)) | → | active#(square(mark(X))) | | mark#(rcons(X1, X2)) | → | active#(rcons(mark(X1), mark(X2))) |
| mark#(times(X1, X2)) | → | active#(times(mark(X1), mark(X2))) | | times#(X1, active(X2)) | → | times#(X1, X2) |
| mark#(plus(X1, X2)) | → | plus#(mark(X1), mark(X2)) | | 2ndsneg#(X1, active(X2)) | → | 2ndsneg#(X1, X2) |
| mark#(cons2(X1, X2)) | → | cons2#(X1, mark(X2)) | | s#(mark(X)) | → | s#(X) |
| cons2#(X1, active(X2)) | → | cons2#(X1, X2) | | rcons#(active(X1), X2) | → | rcons#(X1, X2) |
| s#(active(X)) | → | s#(X) | | cons2#(mark(X1), X2) | → | cons2#(X1, X2) |
| mark#(2ndspos(X1, X2)) | → | mark#(X1) | | mark#(rcons(X1, X2)) | → | mark#(X1) |
| active#(pi(X)) | → | mark#(2ndspos(X, from(0))) |
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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
The following SCCs where found
| cons2#(X1, active(X2)) → cons2#(X1, X2) | cons2#(active(X1), X2) → cons2#(X1, X2) |
| cons2#(X1, mark(X2)) → cons2#(X1, X2) | cons2#(mark(X1), X2) → cons2#(X1, X2) |
| posrecip#(mark(X)) → posrecip#(X) | posrecip#(active(X)) → posrecip#(X) |
| from#(active(X)) → from#(X) | from#(mark(X)) → from#(X) |
| square#(mark(X)) → square#(X) | square#(active(X)) → square#(X) |
| pi#(mark(X)) → pi#(X) | pi#(active(X)) → pi#(X) |
| times#(active(X1), X2) → times#(X1, X2) | times#(X1, active(X2)) → times#(X1, X2) |
| times#(X1, mark(X2)) → times#(X1, X2) | times#(mark(X1), X2) → times#(X1, X2) |
| 2ndspos#(mark(X1), X2) → 2ndspos#(X1, X2) | 2ndspos#(active(X1), X2) → 2ndspos#(X1, X2) |
| 2ndspos#(X1, mark(X2)) → 2ndspos#(X1, X2) | 2ndspos#(X1, active(X2)) → 2ndspos#(X1, X2) |
| 2ndsneg#(X1, mark(X2)) → 2ndsneg#(X1, X2) | 2ndsneg#(active(X1), X2) → 2ndsneg#(X1, X2) |
| 2ndsneg#(mark(X1), X2) → 2ndsneg#(X1, X2) | 2ndsneg#(X1, active(X2)) → 2ndsneg#(X1, X2) |
| cons#(X1, active(X2)) → cons#(X1, X2) | cons#(mark(X1), X2) → cons#(X1, X2) |
| cons#(active(X1), X2) → cons#(X1, X2) | cons#(X1, mark(X2)) → cons#(X1, X2) |
| negrecip#(active(X)) → negrecip#(X) | negrecip#(mark(X)) → negrecip#(X) |
| rcons#(active(X1), X2) → rcons#(X1, X2) | rcons#(X1, active(X2)) → rcons#(X1, X2) |
| rcons#(mark(X1), X2) → rcons#(X1, X2) | rcons#(X1, mark(X2)) → rcons#(X1, X2) |
| mark#(cons(X1, X2)) → active#(cons(mark(X1), X2)) | active#(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark#(rcons(posrecip(Y), 2ndsneg(N, Z))) |
| mark#(2ndspos(X1, X2)) → mark#(X2) | active#(2ndsneg(0, Z)) → mark#(rnil) |
| mark#(square(X)) → mark#(X) | mark#(pi(X)) → mark#(X) |
| active#(2ndsneg(s(N), cons(X, Z))) → mark#(2ndsneg(s(N), cons2(X, Z))) | mark#(cons2(X1, X2)) → mark#(X2) |
| mark#(pi(X)) → active#(pi(mark(X))) | active#(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark#(rcons(negrecip(Y), 2ndspos(N, Z))) |
| active#(2ndspos(s(N), cons(X, Z))) → mark#(2ndspos(s(N), cons2(X, Z))) | mark#(negrecip(X)) → mark#(X) |
| mark#(times(X1, X2)) → mark#(X2) | mark#(2ndsneg(X1, X2)) → mark#(X1) |
| active#(plus(s(X), Y)) → mark#(s(plus(X, Y))) | mark#(plus(X1, X2)) → mark#(X2) |
| mark#(times(X1, X2)) → mark#(X1) | mark#(2ndsneg(X1, X2)) → mark#(X2) |
| mark#(rnil) → active#(rnil) | mark#(s(X)) → mark#(X) |
| active#(times(0, Y)) → mark#(0) | active#(times(s(X), Y)) → mark#(plus(Y, times(X, Y))) |
| mark#(square(X)) → active#(square(mark(X))) | mark#(2ndspos(X1, X2)) → active#(2ndspos(mark(X1), mark(X2))) |
| mark#(plus(X1, X2)) → active#(plus(mark(X1), mark(X2))) | active#(plus(0, Y)) → mark#(Y) |
| mark#(0) → active#(0) | mark#(negrecip(X)) → active#(negrecip(mark(X))) |
| mark#(rcons(X1, X2)) → active#(rcons(mark(X1), mark(X2))) | mark#(s(X)) → active#(s(mark(X))) |
| mark#(cons2(X1, X2)) → active#(cons2(X1, mark(X2))) | mark#(rcons(X1, X2)) → mark#(X2) |
| mark#(times(X1, X2)) → active#(times(mark(X1), mark(X2))) | mark#(2ndsneg(X1, X2)) → active#(2ndsneg(mark(X1), mark(X2))) |
| active#(square(X)) → mark#(times(X, X)) | mark#(from(X)) → mark#(X) |
| mark#(posrecip(X)) → active#(posrecip(mark(X))) | mark#(cons(X1, X2)) → mark#(X1) |
| active#(from(X)) → mark#(cons(X, from(s(X)))) | mark#(plus(X1, X2)) → mark#(X1) |
| active#(2ndspos(0, Z)) → mark#(rnil) | mark#(from(X)) → active#(from(mark(X))) |
| mark#(posrecip(X)) → mark#(X) | mark#(2ndspos(X1, X2)) → mark#(X1) |
| mark#(rcons(X1, X2)) → mark#(X1) | active#(pi(X)) → mark#(2ndspos(X, from(0))) |
| s#(mark(X)) → s#(X) | s#(active(X)) → s#(X) |
| plus#(X1, active(X2)) → plus#(X1, X2) | plus#(X1, mark(X2)) → plus#(X1, X2) |
| plus#(mark(X1), X2) → plus#(X1, X2) | plus#(active(X1), X2) → plus#(X1, X2) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| times#(active(X1), X2) | → | times#(X1, X2) | | times#(X1, active(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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| times#(active(X1), X2) | → | times#(X1, X2) | | times#(mark(X1), X2) | → | times#(X1, X2) |
Problem 16: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| times#(X1, active(X2)) | → | times#(X1, X2) | | 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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Polynomial Interpretation
- 0: 0
- 2ndsneg(x,y): 0
- 2ndspos(x,y): 0
- active(x): 2x + 2
- cons(x,y): 0
- cons2(x,y): 0
- from(x): 0
- mark(x): 2x + 1
- negrecip(x): 0
- pi(x): 0
- plus(x,y): 0
- posrecip(x): 0
- rcons(x,y): 0
- rnil: 0
- s(x): 0
- square(x): 0
- times(x,y): 0
- times#(x,y): y + 1
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, active(X2)) | → | times#(X1, X2) | | times#(X1, mark(X2)) | → | times#(X1, X2) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons#(X1, active(X2)) | → | cons#(X1, X2) | | cons#(mark(X1), X2) | → | cons#(X1, X2) |
| cons#(active(X1), X2) | → | cons#(X1, X2) | | cons#(X1, mark(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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | cons#(active(X1), X2) | → | cons#(X1, X2) |
Problem 17: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| cons#(X1, active(X2)) | → | cons#(X1, X2) | | cons#(X1, mark(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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Polynomial Interpretation
- 0: 0
- 2ndsneg(x,y): 0
- 2ndspos(x,y): 0
- active(x): 2x + 1
- cons(x,y): 0
- cons#(x,y): 2y + 2x + 1
- cons2(x,y): 0
- from(x): 0
- mark(x): 3x
- negrecip(x): 0
- pi(x): 0
- plus(x,y): 0
- posrecip(x): 0
- rcons(x,y): 0
- rnil: 0
- s(x): 0
- square(x): 0
- times(x,y): 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:
| cons#(X1, active(X2)) | → | cons#(X1, X2) |
Problem 23: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| cons#(X1, mark(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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Polynomial Interpretation
- 0: 0
- 2ndsneg(x,y): 0
- 2ndspos(x,y): 0
- active(x): 0
- cons(x,y): 0
- cons#(x,y): 2y + x
- cons2(x,y): 0
- from(x): 0
- mark(x): 2x + 1
- negrecip(x): 0
- pi(x): 0
- plus(x,y): 0
- posrecip(x): 0
- rcons(x,y): 0
- rnil: 0
- s(x): 0
- square(x): 0
- times(x,y): 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:
| cons#(X1, mark(X2)) | → | cons#(X1, X2) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| rcons#(active(X1), X2) | → | rcons#(X1, X2) | | rcons#(X1, active(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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| rcons#(active(X1), X2) | → | rcons#(X1, X2) | | rcons#(mark(X1), X2) | → | rcons#(X1, X2) |
Problem 18: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| rcons#(X1, active(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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Polynomial Interpretation
- 0: 0
- 2ndsneg(x,y): 0
- 2ndspos(x,y): 0
- active(x): 2x + 2
- cons(x,y): 0
- cons2(x,y): 0
- from(x): 0
- mark(x): 2x + 1
- negrecip(x): 0
- pi(x): 0
- plus(x,y): 0
- posrecip(x): 0
- rcons(x,y): 0
- rcons#(x,y): y + 1
- rnil: 0
- s(x): 0
- square(x): 0
- times(x,y): 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, active(X2)) | → | rcons#(X1, X2) | | rcons#(X1, mark(X2)) | → | rcons#(X1, X2) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| negrecip#(active(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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| negrecip#(active(X)) | → | negrecip#(X) | | negrecip#(mark(X)) | → | negrecip#(X) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| pi#(mark(X)) | → | pi#(X) | | pi#(active(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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| pi#(mark(X)) | → | pi#(X) | | pi#(active(X)) | → | pi#(X) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| square#(mark(X)) | → | square#(X) | | square#(active(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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| square#(mark(X)) | → | square#(X) | | square#(active(X)) | → | square#(X) |
Problem 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons2#(X1, active(X2)) | → | cons2#(X1, X2) | | cons2#(active(X1), X2) | → | cons2#(X1, X2) |
| cons2#(X1, mark(X2)) | → | cons2#(X1, X2) | | cons2#(mark(X1), 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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| cons2#(active(X1), X2) | → | cons2#(X1, X2) | | cons2#(mark(X1), X2) | → | cons2#(X1, X2) |
Problem 19: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| cons2#(X1, active(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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Polynomial Interpretation
- 0: 0
- 2ndsneg(x,y): 0
- 2ndspos(x,y): 0
- active(x): 2x + 2
- cons(x,y): 0
- cons2(x,y): 0
- cons2#(x,y): y + 1
- from(x): 0
- mark(x): 2x + 1
- negrecip(x): 0
- pi(x): 0
- plus(x,y): 0
- posrecip(x): 0
- rcons(x,y): 0
- rnil: 0
- s(x): 0
- square(x): 0
- times(x,y): 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, active(X2)) | → | cons2#(X1, X2) | | cons2#(X1, mark(X2)) | → | cons2#(X1, X2) |
Problem 9: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| from#(active(X)) | → | from#(X) | | from#(mark(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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| from#(active(X)) | → | from#(X) | | from#(mark(X)) | → | from#(X) |
Problem 10: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| plus#(X1, active(X2)) | → | plus#(X1, X2) | | plus#(X1, mark(X2)) | → | plus#(X1, X2) |
| plus#(mark(X1), X2) | → | plus#(X1, X2) | | plus#(active(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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| plus#(mark(X1), X2) | → | plus#(X1, X2) | | plus#(active(X1), X2) | → | plus#(X1, X2) |
Problem 20: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| plus#(X1, mark(X2)) | → | plus#(X1, X2) | | plus#(X1, active(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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Polynomial Interpretation
- 0: 0
- 2ndsneg(x,y): 0
- 2ndspos(x,y): 0
- active(x): 2x + 2
- cons(x,y): 0
- cons2(x,y): 0
- from(x): 0
- mark(x): 2x + 1
- negrecip(x): 0
- pi(x): 0
- plus(x,y): 0
- plus#(x,y): y + 1
- posrecip(x): 0
- rcons(x,y): 0
- rnil: 0
- s(x): 0
- square(x): 0
- times(x,y): 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, active(X2)) | → | plus#(X1, X2) | | plus#(X1, mark(X2)) | → | plus#(X1, X2) |
Problem 11: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| 2ndspos#(mark(X1), X2) | → | 2ndspos#(X1, X2) | | 2ndspos#(active(X1), X2) | → | 2ndspos#(X1, X2) |
| 2ndspos#(X1, mark(X2)) | → | 2ndspos#(X1, X2) | | 2ndspos#(X1, active(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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| 2ndspos#(mark(X1), X2) | → | 2ndspos#(X1, X2) | | 2ndspos#(active(X1), X2) | → | 2ndspos#(X1, X2) |
Problem 21: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| 2ndspos#(X1, mark(X2)) | → | 2ndspos#(X1, X2) | | 2ndspos#(X1, active(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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Polynomial Interpretation
- 0: 0
- 2ndsneg(x,y): 0
- 2ndspos(x,y): 0
- 2ndspos#(x,y): y + 1
- active(x): 2x
- cons(x,y): 0
- cons2(x,y): 0
- from(x): 0
- mark(x): 2x + 1
- negrecip(x): 0
- pi(x): 0
- plus(x,y): 0
- posrecip(x): 0
- rcons(x,y): 0
- rnil: 0
- s(x): 0
- square(x): 0
- times(x,y): 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 24: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| 2ndspos#(X1, active(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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Polynomial Interpretation
- 0: 0
- 2ndsneg(x,y): 0
- 2ndspos(x,y): 0
- 2ndspos#(x,y): y + x + 1
- active(x): x + 2
- cons(x,y): 0
- cons2(x,y): 0
- from(x): 0
- mark(x): 0
- negrecip(x): 0
- pi(x): 0
- plus(x,y): 0
- posrecip(x): 0
- rcons(x,y): 0
- rnil: 0
- s(x): 0
- square(x): 0
- times(x,y): 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, active(X2)) | → | 2ndspos#(X1, X2) |
Problem 12: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| s#(mark(X)) | → | s#(X) | | s#(active(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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| s#(mark(X)) | → | s#(X) | | s#(active(X)) | → | s#(X) |
Problem 14: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| 2ndsneg#(X1, mark(X2)) | → | 2ndsneg#(X1, X2) | | 2ndsneg#(active(X1), X2) | → | 2ndsneg#(X1, X2) |
| 2ndsneg#(mark(X1), X2) | → | 2ndsneg#(X1, X2) | | 2ndsneg#(X1, active(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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| 2ndsneg#(active(X1), X2) | → | 2ndsneg#(X1, X2) | | 2ndsneg#(mark(X1), X2) | → | 2ndsneg#(X1, X2) |
Problem 22: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| 2ndsneg#(X1, mark(X2)) | → | 2ndsneg#(X1, X2) | | 2ndsneg#(X1, active(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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Polynomial Interpretation
- 0: 0
- 2ndsneg(x,y): 0
- 2ndsneg#(x,y): y + 1
- 2ndspos(x,y): 0
- active(x): x
- cons(x,y): 0
- cons2(x,y): 0
- from(x): 0
- mark(x): 2x + 2
- negrecip(x): 0
- pi(x): 0
- plus(x,y): 0
- posrecip(x): 0
- rcons(x,y): 0
- rnil: 0
- s(x): 0
- square(x): 0
- times(x,y): 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 25: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| 2ndsneg#(X1, active(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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Polynomial Interpretation
- 0: 0
- 2ndsneg(x,y): 0
- 2ndsneg#(x,y): 2y
- 2ndspos(x,y): 0
- active(x): 2x + 1
- cons(x,y): 0
- cons2(x,y): 0
- from(x): 0
- mark(x): 0
- negrecip(x): 0
- pi(x): 0
- plus(x,y): 0
- posrecip(x): 0
- rcons(x,y): 0
- rnil: 0
- s(x): 0
- square(x): 0
- times(x,y): 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, active(X2)) | → | 2ndsneg#(X1, X2) |
Problem 15: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| posrecip#(mark(X)) | → | posrecip#(X) | | posrecip#(active(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)) | | mark(from(X)) | → | active(from(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(2ndspos(X1, X2)) | → | active(2ndspos(mark(X1), mark(X2))) | | mark(0) | → | active(0) |
| mark(rnil) | → | active(rnil) | | mark(cons2(X1, X2)) | → | active(cons2(X1, mark(X2))) |
| mark(rcons(X1, X2)) | → | active(rcons(mark(X1), mark(X2))) | | mark(posrecip(X)) | → | active(posrecip(mark(X))) |
| mark(2ndsneg(X1, X2)) | → | active(2ndsneg(mark(X1), mark(X2))) | | mark(negrecip(X)) | → | active(negrecip(mark(X))) |
| mark(pi(X)) | → | active(pi(mark(X))) | | mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) |
| mark(times(X1, X2)) | → | active(times(mark(X1), mark(X2))) | | mark(square(X)) | → | active(square(mark(X))) |
| from(mark(X)) | → | from(X) | | from(active(X)) | → | from(X) |
| cons(mark(X1), X2) | → | cons(X1, X2) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| cons(active(X1), X2) | → | cons(X1, X2) | | cons(X1, active(X2)) | → | cons(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| 2ndspos(mark(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, mark(X2)) | → | 2ndspos(X1, X2) |
| 2ndspos(active(X1), X2) | → | 2ndspos(X1, X2) | | 2ndspos(X1, active(X2)) | → | 2ndspos(X1, X2) |
| cons2(mark(X1), X2) | → | cons2(X1, X2) | | cons2(X1, mark(X2)) | → | cons2(X1, X2) |
| cons2(active(X1), X2) | → | cons2(X1, X2) | | cons2(X1, active(X2)) | → | cons2(X1, X2) |
| rcons(mark(X1), X2) | → | rcons(X1, X2) | | rcons(X1, mark(X2)) | → | rcons(X1, X2) |
| rcons(active(X1), X2) | → | rcons(X1, X2) | | rcons(X1, active(X2)) | → | rcons(X1, X2) |
| posrecip(mark(X)) | → | posrecip(X) | | posrecip(active(X)) | → | posrecip(X) |
| 2ndsneg(mark(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, mark(X2)) | → | 2ndsneg(X1, X2) |
| 2ndsneg(active(X1), X2) | → | 2ndsneg(X1, X2) | | 2ndsneg(X1, active(X2)) | → | 2ndsneg(X1, X2) |
| negrecip(mark(X)) | → | negrecip(X) | | negrecip(active(X)) | → | negrecip(X) |
| pi(mark(X)) | → | pi(X) | | pi(active(X)) | → | pi(X) |
| plus(mark(X1), X2) | → | plus(X1, X2) | | plus(X1, mark(X2)) | → | plus(X1, X2) |
| plus(active(X1), X2) | → | plus(X1, X2) | | plus(X1, active(X2)) | → | plus(X1, X2) |
| times(mark(X1), X2) | → | times(X1, X2) | | times(X1, mark(X2)) | → | times(X1, X2) |
| times(active(X1), X2) | → | times(X1, X2) | | times(X1, active(X2)) | → | times(X1, X2) |
| square(mark(X)) | → | square(X) | | square(active(X)) | → | square(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, square, pi, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| posrecip#(mark(X)) | → | posrecip#(X) | | posrecip#(active(X)) | → | posrecip#(X) |