(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following 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)
Q is empty.