(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a__from(X) → cons(mark(X), from(s(X)))
a__2ndspos(0, Z) → rnil
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons2(X, cons(Y, Z))) → rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z)))
a__pi(X) → a__2ndspos(mark(X), a__from(0))
a__plus(0, Y) → mark(Y)
a__plus(s(X), Y) → s(a__plus(mark(X), mark(Y)))
a__times(0, Y) → 0
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__square(X) → a__times(mark(X), mark(X))
mark(from(X)) → a__from(mark(X))
mark(2ndspos(X1, X2)) → a__2ndspos(mark(X1), mark(X2))
mark(2ndsneg(X1, X2)) → a__2ndsneg(mark(X1), mark(X2))
mark(pi(X)) → a__pi(mark(X))
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
mark(square(X)) → a__square(mark(X))
mark(0) → 0
mark(s(X)) → s(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
mark(negrecip(X)) → negrecip(mark(X))
mark(nil) → nil
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
mark(rnil) → rnil
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
a__from(X) → from(X)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__pi(X) → pi(X)
a__plus(X1, X2) → plus(X1, X2)
a__times(X1, X2) → times(X1, X2)
a__square(X) → square(X)
Q is empty.
(1) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(2) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__FROM(X) → MARK(X)
A__2NDSPOS(s(N), cons(X, Z)) → A__2NDSPOS(s(mark(N)), cons2(X, mark(Z)))
A__2NDSPOS(s(N), cons(X, Z)) → MARK(N)
A__2NDSPOS(s(N), cons(X, Z)) → MARK(Z)
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → MARK(Y)
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → A__2NDSNEG(mark(N), mark(Z))
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → MARK(N)
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → MARK(Z)
A__2NDSNEG(s(N), cons(X, Z)) → A__2NDSNEG(s(mark(N)), cons2(X, mark(Z)))
A__2NDSNEG(s(N), cons(X, Z)) → MARK(N)
A__2NDSNEG(s(N), cons(X, Z)) → MARK(Z)
A__2NDSNEG(s(N), cons2(X, cons(Y, Z))) → MARK(Y)
A__2NDSNEG(s(N), cons2(X, cons(Y, Z))) → A__2NDSPOS(mark(N), mark(Z))
A__2NDSNEG(s(N), cons2(X, cons(Y, Z))) → MARK(N)
A__2NDSNEG(s(N), cons2(X, cons(Y, Z))) → MARK(Z)
A__PI(X) → A__2NDSPOS(mark(X), a__from(0))
A__PI(X) → MARK(X)
A__PI(X) → A__FROM(0)
A__PLUS(0, Y) → MARK(Y)
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
A__PLUS(s(X), Y) → MARK(X)
A__PLUS(s(X), Y) → MARK(Y)
A__TIMES(s(X), Y) → A__PLUS(mark(Y), a__times(mark(X), mark(Y)))
A__TIMES(s(X), Y) → MARK(Y)
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
A__TIMES(s(X), Y) → MARK(X)
A__SQUARE(X) → A__TIMES(mark(X), mark(X))
A__SQUARE(X) → MARK(X)
MARK(from(X)) → A__FROM(mark(X))
MARK(from(X)) → MARK(X)
MARK(2ndspos(X1, X2)) → A__2NDSPOS(mark(X1), mark(X2))
MARK(2ndspos(X1, X2)) → MARK(X1)
MARK(2ndspos(X1, X2)) → MARK(X2)
MARK(2ndsneg(X1, X2)) → A__2NDSNEG(mark(X1), mark(X2))
MARK(2ndsneg(X1, X2)) → MARK(X1)
MARK(2ndsneg(X1, X2)) → MARK(X2)
MARK(pi(X)) → A__PI(mark(X))
MARK(pi(X)) → MARK(X)
MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → A__TIMES(mark(X1), mark(X2))
MARK(times(X1, X2)) → MARK(X1)
MARK(times(X1, X2)) → MARK(X2)
MARK(square(X)) → A__SQUARE(mark(X))
MARK(square(X)) → MARK(X)
MARK(s(X)) → MARK(X)
MARK(posrecip(X)) → MARK(X)
MARK(negrecip(X)) → MARK(X)
MARK(cons(X1, X2)) → MARK(X1)
MARK(cons2(X1, X2)) → MARK(X2)
MARK(rcons(X1, X2)) → MARK(X1)
MARK(rcons(X1, X2)) → MARK(X2)
The TRS R consists of the following rules:
a__from(X) → cons(mark(X), from(s(X)))
a__2ndspos(0, Z) → rnil
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons2(X, cons(Y, Z))) → rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z)))
a__pi(X) → a__2ndspos(mark(X), a__from(0))
a__plus(0, Y) → mark(Y)
a__plus(s(X), Y) → s(a__plus(mark(X), mark(Y)))
a__times(0, Y) → 0
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__square(X) → a__times(mark(X), mark(X))
mark(from(X)) → a__from(mark(X))
mark(2ndspos(X1, X2)) → a__2ndspos(mark(X1), mark(X2))
mark(2ndsneg(X1, X2)) → a__2ndsneg(mark(X1), mark(X2))
mark(pi(X)) → a__pi(mark(X))
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
mark(square(X)) → a__square(mark(X))
mark(0) → 0
mark(s(X)) → s(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
mark(negrecip(X)) → negrecip(mark(X))
mark(nil) → nil
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
mark(rnil) → rnil
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
a__from(X) → from(X)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__pi(X) → pi(X)
a__plus(X1, X2) → plus(X1, X2)
a__times(X1, X2) → times(X1, X2)
a__square(X) → square(X)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.