TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60002 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (11990ms).
 | – Problem 2 was processed with processor SubtermCriterion (2ms).
 | – Problem 3 was processed with processor SubtermCriterion (4ms).
 | – Problem 4 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 15 remains open; application of the following processors failed [DependencyGraph (4ms), PolynomialLinearRange4iUR (16ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (11ms), DependencyGraph (4ms), PolynomialLinearRange4iUR (26ms), DependencyGraph (4ms), PolynomialLinearRange8NegiUR (0ms), DependencyGraph (4ms)].
 | – Problem 5 was processed with processor SubtermCriterion (1ms).
 | – Problem 6 was processed with processor SubtermCriterion (2ms).
 | – Problem 7 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 16 was processed with processor PolynomialLinearRange4iUR (40ms).
 |    |    | – Problem 21 was processed with processor PolynomialLinearRange4iUR (88ms).
 | – Problem 8 was processed with processor SubtermCriterion (3ms).
 | – Problem 9 was processed with processor SubtermCriterion (2ms).
 |    | – Problem 17 was processed with processor PolynomialLinearRange4iUR (126ms).
 | – Problem 10 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 18 was processed with processor PolynomialLinearRange4iUR (60ms).
 | – Problem 11 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 19 was processed with processor PolynomialLinearRange4iUR (76ms).
 | – Problem 12 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 20 was processed with processor PolynomialLinearRange4iUR (72ms).
 |    |    | – Problem 22 was processed with processor PolynomialLinearRange4iUR (65ms).
 | – Problem 13 remains open; application of the following processors failed [SubtermCriterion (3ms), DependencyGraph (2191ms), PolynomialLinearRange4iUR (1437ms), DependencyGraph (2269ms), PolynomialLinearRange4iUR (2532ms), DependencyGraph (1897ms), PolynomialLinearRange4iUR (5033ms), DependencyGraph (2004ms), PolynomialLinearRange8NegiUR (15021ms), DependencyGraph (1891ms), ReductionPairSAT (timeout)].
 | – Problem 14 was processed with processor SubtermCriterion (1ms).

The following open problems remain:

Open Dependency Pair Problem 13

Dependency Pairs

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)
mark#(pi(X)) → 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)))
active#(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark#(rcons(negrecip(Y), 2ndspos(N, Z)))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)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)))
active#(2ndspos(s(N), cons(X, cons(Y, Z)))) → mark#(rcons(posrecip(Y), 2ndsneg(N, Z)))mark#(0) → active#(0)
mark#(plus(X1, X2)) → active#(plus(mark(X1), mark(X2)))active#(plus(0, Y)) → mark#(Y)
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#(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)))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, square, pi, cons

Open Dependency Pair Problem 15

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, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, 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#(2ndspos(s(N), cons(X, cons(Y, Z)))) → posrecip#(Y)
active#(2ndsneg(0, Z)) → mark#(rnil)active#(pi(X)) → from#(0)
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)mark#(plus(X1, X2)) → active#(plus(mark(X1), mark(X2)))
2ndspos#(X1, mark(X2)) → 2ndspos#(X1, X2)mark#(rcons(X1, X2)) → mark#(X2)
active#(square(X)) → mark#(times(X, X))mark#(pi(X)) → pi#(mark(X))
mark#(cons(X1, X2)) → mark#(X1)rcons#(mark(X1), X2) → rcons#(X1, X2)
times#(mark(X1), X2) → times#(X1, X2)active#(square(X)) → times#(X, X)
negrecip#(mark(X)) → negrecip#(X)active#(from(X)) → mark#(cons(X, from(s(X))))
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)
cons#(mark(X1), X2) → cons#(X1, X2)mark#(rcons(X1, X2)) → rcons#(mark(X1), mark(X2))
from#(mark(X)) → from#(X)active#(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark#(rcons(negrecip(Y), 2ndspos(N, Z)))
square#(mark(X)) → square#(X)times#(X1, mark(X2)) → times#(X1, X2)
cons#(X1, mark(X2)) → cons#(X1, X2)active#(pi(X)) → 2ndspos#(X, from(0))
mark#(square(X)) → square#(mark(X))active#(times(0, Y)) → mark#(0)
mark#(2ndspos(X1, X2)) → active#(2ndspos(mark(X1), mark(X2)))active#(plus(s(X), Y)) → plus#(X, Y)
active#(2ndspos(s(N), cons(X, cons(Y, Z)))) → mark#(rcons(posrecip(Y), 2ndsneg(N, Z)))posrecip#(mark(X)) → posrecip#(X)
mark#(0) → active#(0)mark#(negrecip(X)) → active#(negrecip(mark(X)))
active#(2ndsneg(s(N), cons(X, cons(Y, Z)))) → negrecip#(Y)mark#(s(X)) → active#(s(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#(2ndsneg(s(N), cons(X, cons(Y, Z)))) → 2ndspos#(N, Z)
active#(2ndspos(0, Z)) → mark#(rnil)2ndsneg#(X1, mark(X2)) → 2ndsneg#(X1, X2)
rcons#(X1, mark(X2)) → rcons#(X1, X2)active#(from(X)) → from#(s(X))
mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))active#(2ndspos(s(N), cons(X, cons(Y, Z)))) → rcons#(posrecip(Y), 2ndsneg(N, Z))
mark#(2ndspos(X1, X2)) → mark#(X2)mark#(square(X)) → mark#(X)
2ndspos#(X1, active(X2)) → 2ndspos#(X1, X2)active#(2ndsneg(s(N), cons(X, cons(Y, Z)))) → rcons#(negrecip(Y), 2ndspos(N, Z))
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)mark#(posrecip(X)) → posrecip#(mark(X))
pi#(active(X)) → pi#(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)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#(plus(s(X), Y)) → s#(plus(X, Y))
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)s#(mark(X)) → s#(X)
rcons#(active(X1), X2) → rcons#(X1, X2)s#(active(X)) → s#(X)
mark#(2ndspos(X1, X2)) → mark#(X1)mark#(rcons(X1, X2)) → mark#(X1)
active#(pi(X)) → mark#(2ndspos(X, from(0)))active#(2ndspos(s(N), cons(X, cons(Y, Z)))) → 2ndsneg#(N, Z)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, square, pi, cons

Strategy

The following SCCs where found

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)
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)
mark#(pi(X)) → mark#(X)mark#(pi(X)) → active#(pi(mark(X)))
mark#(negrecip(X)) → mark#(X)mark#(times(X1, X2)) → mark#(X2)
mark#(2ndsneg(X1, X2)) → mark#(X1)active#(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark#(rcons(negrecip(Y), 2ndspos(N, Z)))
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)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)))
active#(2ndspos(s(N), cons(X, cons(Y, Z)))) → mark#(rcons(posrecip(Y), 2ndsneg(N, Z)))active#(plus(0, Y)) → mark#(Y)
mark#(plus(X1, X2)) → active#(plus(mark(X1), mark(X2)))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#(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#(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)))
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)
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

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, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, 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 3: 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, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, 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)

Problem 4: 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, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, 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 5: 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, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, 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 6: 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, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, 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 7: 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, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, 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 16: 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, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, square, pi, cons

Strategy

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

rcons#(X1, mark(X2)) → rcons#(X1, X2)

Problem 21: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

rcons#(X1, active(X2)) → rcons#(X1, X2)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, square, pi, cons

Strategy

Polynomial Interpretation

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)

Problem 8: 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, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, 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 9: 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, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, 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 17: 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, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, square, pi, cons

Strategy

Polynomial Interpretation

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 10: 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, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, 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 18: 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, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, square, pi, cons

Strategy

Polynomial Interpretation

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 11: 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, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, 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 19: 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, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, square, pi, cons

Strategy

Polynomial Interpretation

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)2ndsneg#(X1, active(X2)) → 2ndsneg#(X1, X2)

Problem 12: 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, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, 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 20: 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, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, square, pi, cons

Strategy

Polynomial Interpretation

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 22: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

cons#(X1, active(X2)) → cons#(X1, X2)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, rnil, mark, from, rcons, 2ndspos, 0, s, times, 2ndsneg, active, square, pi, cons

Strategy

Polynomial Interpretation

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 14: 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, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))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(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)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, 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)