(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.
(3) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
A__PI(X) → A__FROM(0)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(A__FROM(x1)) = | -I | + | 0A | · | x1 |
POL(MARK(x1)) = | -I | + | 0A | · | x1 |
POL(A__2NDSPOS(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(cons(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(mark(x1)) = | -I | + | 0A | · | x1 |
POL(cons2(x1, x2)) = | -I | + | -I | · | x1 | + | 0A | · | x2 |
POL(A__2NDSNEG(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__PI(x1)) = | 1A | + | 0A | · | x1 |
POL(a__from(x1)) = | 0A | + | 0A | · | x1 |
POL(A__PLUS(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__TIMES(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__times(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__SQUARE(x1)) = | 1A | + | 0A | · | x1 |
POL(from(x1)) = | 0A | + | 0A | · | x1 |
POL(2ndspos(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(2ndsneg(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(plus(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(times(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(square(x1)) = | 1A | + | 0A | · | x1 |
POL(posrecip(x1)) = | -I | + | 0A | · | x1 |
POL(negrecip(x1)) = | -I | + | 0A | · | x1 |
POL(rcons(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__plus(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__pi(x1)) = | 1A | + | 0A | · | x1 |
POL(a__2ndsneg(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__2ndspos(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__square(x1)) = | 1A | + | 0A | · | x1 |
The following usable rules [FROCOS05] were oriented:
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
mark(negrecip(X)) → negrecip(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
a__from(X) → from(X)
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
mark(rnil) → rnil
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
a__plus(X1, X2) → plus(X1, X2)
a__pi(X) → pi(X)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__square(X) → square(X)
a__times(X1, X2) → times(X1, X2)
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndspos(0, Z) → rnil
a__from(X) → cons(mark(X), from(s(X)))
a__times(0, Y) → 0
mark(from(X)) → a__from(mark(X))
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(s(X), Y) → s(a__plus(mark(X), mark(Y)))
mark(0) → 0
mark(s(X)) → s(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))
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__plus(0, Y) → mark(Y)
mark(square(X)) → a__square(mark(X))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
a__square(X) → a__times(mark(X), mark(X))
(4) 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__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.
(5) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MARK(pi(X)) → MARK(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(A__FROM(x1)) = | 0A | + | 0A | · | x1 |
POL(MARK(x1)) = | 0A | + | 0A | · | x1 |
POL(A__2NDSPOS(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(cons(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(mark(x1)) = | 0A | + | 0A | · | x1 |
POL(cons2(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__2NDSNEG(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__PI(x1)) = | 0A | + | 1A | · | x1 |
POL(a__from(x1)) = | 0A | + | 0A | · | x1 |
POL(A__PLUS(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__TIMES(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__times(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__SQUARE(x1)) = | 0A | + | 0A | · | x1 |
POL(from(x1)) = | 0A | + | 0A | · | x1 |
POL(2ndspos(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(2ndsneg(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(plus(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(times(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(square(x1)) = | -I | + | 0A | · | x1 |
POL(posrecip(x1)) = | -I | + | 0A | · | x1 |
POL(negrecip(x1)) = | -I | + | 0A | · | x1 |
POL(rcons(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__plus(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__pi(x1)) = | 1A | + | 1A | · | x1 |
POL(a__2ndsneg(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__2ndspos(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__square(x1)) = | 0A | + | 0A | · | x1 |
The following usable rules [FROCOS05] were oriented:
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
mark(negrecip(X)) → negrecip(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
a__from(X) → from(X)
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
mark(rnil) → rnil
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
a__plus(X1, X2) → plus(X1, X2)
a__pi(X) → pi(X)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__square(X) → square(X)
a__times(X1, X2) → times(X1, X2)
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndspos(0, Z) → rnil
a__from(X) → cons(mark(X), from(s(X)))
a__times(0, Y) → 0
mark(from(X)) → a__from(mark(X))
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(s(X), Y) → s(a__plus(mark(X), mark(Y)))
mark(0) → 0
mark(s(X)) → s(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))
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__plus(0, Y) → mark(Y)
mark(square(X)) → a__square(mark(X))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
a__square(X) → a__times(mark(X), mark(X))
(6) 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__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(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.
(7) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
A__TIMES(s(X), Y) → MARK(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(A__FROM(x1)) = | 0A | + | 0A | · | x1 |
POL(MARK(x1)) = | 0A | + | 0A | · | x1 |
POL(A__2NDSPOS(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(cons(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(mark(x1)) = | -I | + | 0A | · | x1 |
POL(cons2(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__2NDSNEG(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__PI(x1)) = | 0A | + | 0A | · | x1 |
POL(a__from(x1)) = | 0A | + | 0A | · | x1 |
POL(A__PLUS(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__TIMES(x1, x2)) = | 0A | + | 1A | · | x1 | + | 0A | · | x2 |
POL(a__times(x1, x2)) = | -I | + | 1A | · | x1 | + | 0A | · | x2 |
POL(A__SQUARE(x1)) = | 0A | + | 1A | · | x1 |
POL(from(x1)) = | 0A | + | 0A | · | x1 |
POL(2ndspos(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(2ndsneg(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(plus(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(times(x1, x2)) = | -I | + | 1A | · | x1 | + | 0A | · | x2 |
POL(square(x1)) = | -I | + | 1A | · | x1 |
POL(posrecip(x1)) = | 0A | + | 0A | · | x1 |
POL(negrecip(x1)) = | 0A | + | 0A | · | x1 |
POL(rcons(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__plus(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__pi(x1)) = | 0A | + | 0A | · | x1 |
POL(a__2ndsneg(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__2ndspos(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__square(x1)) = | -I | + | 1A | · | x1 |
The following usable rules [FROCOS05] were oriented:
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
mark(negrecip(X)) → negrecip(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
a__from(X) → from(X)
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
mark(rnil) → rnil
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
a__plus(X1, X2) → plus(X1, X2)
a__pi(X) → pi(X)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__square(X) → square(X)
a__times(X1, X2) → times(X1, X2)
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndspos(0, Z) → rnil
a__from(X) → cons(mark(X), from(s(X)))
a__times(0, Y) → 0
mark(from(X)) → a__from(mark(X))
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(s(X), Y) → s(a__plus(mark(X), mark(Y)))
mark(0) → 0
mark(s(X)) → s(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))
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__plus(0, Y) → mark(Y)
mark(square(X)) → a__square(mark(X))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
a__square(X) → a__times(mark(X), mark(X))
(8) 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__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__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(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.
(9) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MARK(pi(X)) → A__PI(mark(X))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(A__FROM(x1)) = | 0A | + | 0A | · | x1 |
POL(MARK(x1)) = | 0A | + | 0A | · | x1 |
POL(A__2NDSPOS(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(cons(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(mark(x1)) = | 0A | + | 0A | · | x1 |
POL(cons2(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__2NDSNEG(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__PI(x1)) = | 0A | + | 0A | · | x1 |
POL(a__from(x1)) = | 0A | + | 0A | · | x1 |
POL(A__PLUS(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__TIMES(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__times(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__SQUARE(x1)) = | 5A | + | 0A | · | x1 |
POL(from(x1)) = | -I | + | 0A | · | x1 |
POL(2ndspos(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(2ndsneg(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(plus(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(times(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(square(x1)) = | 5A | + | 0A | · | x1 |
POL(posrecip(x1)) = | 0A | + | 0A | · | x1 |
POL(negrecip(x1)) = | 0A | + | 0A | · | x1 |
POL(rcons(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__plus(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__pi(x1)) = | 1A | + | 1A | · | x1 |
POL(a__2ndsneg(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__2ndspos(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__square(x1)) = | 5A | + | 0A | · | x1 |
The following usable rules [FROCOS05] were oriented:
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
mark(negrecip(X)) → negrecip(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
a__from(X) → from(X)
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
mark(rnil) → rnil
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
a__plus(X1, X2) → plus(X1, X2)
a__pi(X) → pi(X)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__square(X) → square(X)
a__times(X1, X2) → times(X1, X2)
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndspos(0, Z) → rnil
a__from(X) → cons(mark(X), from(s(X)))
a__times(0, Y) → 0
mark(from(X)) → a__from(mark(X))
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(s(X), Y) → s(a__plus(mark(X), mark(Y)))
mark(0) → 0
mark(s(X)) → s(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))
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__plus(0, Y) → mark(Y)
mark(square(X)) → a__square(mark(X))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
a__square(X) → a__times(mark(X), mark(X))
(10) 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__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__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(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.
(11) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.
(12) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MARK(from(X)) → A__FROM(mark(X))
A__FROM(X) → MARK(X)
MARK(from(X)) → MARK(X)
MARK(2ndspos(X1, X2)) → A__2NDSPOS(mark(X1), mark(X2))
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))) → MARK(Y)
MARK(2ndspos(X1, X2)) → MARK(X1)
MARK(2ndspos(X1, X2)) → MARK(X2)
MARK(2ndsneg(X1, X2)) → A__2NDSNEG(mark(X1), mark(X2))
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))) → MARK(Y)
MARK(2ndsneg(X1, X2)) → MARK(X1)
MARK(2ndsneg(X1, X2)) → MARK(X2)
MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(0, Y) → MARK(Y)
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → A__TIMES(mark(X1), mark(X2))
A__TIMES(s(X), Y) → A__PLUS(mark(Y), a__times(mark(X), mark(Y)))
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
A__PLUS(s(X), Y) → MARK(X)
MARK(times(X1, X2)) → MARK(X1)
MARK(times(X1, X2)) → MARK(X2)
MARK(square(X)) → A__SQUARE(mark(X))
A__SQUARE(X) → A__TIMES(mark(X), mark(X))
A__TIMES(s(X), Y) → MARK(Y)
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)
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
A__SQUARE(X) → MARK(X)
A__PLUS(s(X), Y) → MARK(Y)
A__2NDSNEG(s(N), cons2(X, cons(Y, Z))) → A__2NDSPOS(mark(N), 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))) → A__2NDSNEG(mark(N), 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(N)
A__2NDSNEG(s(N), cons2(X, cons(Y, Z))) → MARK(Z)
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → MARK(N)
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → MARK(Z)
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.
(13) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MARK(posrecip(X)) → MARK(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(MARK(x1)) = | 0A | + | 0A | · | x1 |
POL(from(x1)) = | 1A | + | 0A | · | x1 |
POL(A__FROM(x1)) = | 1A | + | 0A | · | x1 |
POL(mark(x1)) = | -I | + | 0A | · | x1 |
POL(2ndspos(x1, x2)) = | 0A | + | 0A | · | x1 | + | 4A | · | x2 |
POL(A__2NDSPOS(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(cons(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(cons2(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(2ndsneg(x1, x2)) = | -I | + | 0A | · | x1 | + | 4A | · | x2 |
POL(A__2NDSNEG(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(plus(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__PLUS(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(times(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__TIMES(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__times(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(square(x1)) = | 1A | + | 0A | · | x1 |
POL(A__SQUARE(x1)) = | 1A | + | 0A | · | x1 |
POL(posrecip(x1)) = | 1A | + | 3A | · | x1 |
POL(negrecip(x1)) = | -I | + | 0A | · | x1 |
POL(rcons(x1, x2)) = | -I | + | 1A | · | x1 | + | 0A | · | x2 |
POL(a__from(x1)) = | 1A | + | 0A | · | x1 |
POL(a__plus(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__pi(x1)) = | 5A | + | 0A | · | x1 |
POL(a__2ndsneg(x1, x2)) = | -I | + | 0A | · | x1 | + | 4A | · | x2 |
POL(a__2ndspos(x1, x2)) = | 0A | + | 0A | · | x1 | + | 4A | · | x2 |
POL(a__square(x1)) = | 1A | + | 0A | · | x1 |
The following usable rules [FROCOS05] were oriented:
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
mark(negrecip(X)) → negrecip(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
a__from(X) → from(X)
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
mark(rnil) → rnil
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
a__plus(X1, X2) → plus(X1, X2)
a__pi(X) → pi(X)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__square(X) → square(X)
a__times(X1, X2) → times(X1, X2)
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndspos(0, Z) → rnil
a__from(X) → cons(mark(X), from(s(X)))
a__times(0, Y) → 0
mark(from(X)) → a__from(mark(X))
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(s(X), Y) → s(a__plus(mark(X), mark(Y)))
mark(0) → 0
mark(s(X)) → s(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))
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__plus(0, Y) → mark(Y)
mark(square(X)) → a__square(mark(X))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
a__square(X) → a__times(mark(X), mark(X))
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MARK(from(X)) → A__FROM(mark(X))
A__FROM(X) → MARK(X)
MARK(from(X)) → MARK(X)
MARK(2ndspos(X1, X2)) → A__2NDSPOS(mark(X1), mark(X2))
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))) → MARK(Y)
MARK(2ndspos(X1, X2)) → MARK(X1)
MARK(2ndspos(X1, X2)) → MARK(X2)
MARK(2ndsneg(X1, X2)) → A__2NDSNEG(mark(X1), mark(X2))
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))) → MARK(Y)
MARK(2ndsneg(X1, X2)) → MARK(X1)
MARK(2ndsneg(X1, X2)) → MARK(X2)
MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(0, Y) → MARK(Y)
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → A__TIMES(mark(X1), mark(X2))
A__TIMES(s(X), Y) → A__PLUS(mark(Y), a__times(mark(X), mark(Y)))
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
A__PLUS(s(X), Y) → MARK(X)
MARK(times(X1, X2)) → MARK(X1)
MARK(times(X1, X2)) → MARK(X2)
MARK(square(X)) → A__SQUARE(mark(X))
A__SQUARE(X) → A__TIMES(mark(X), mark(X))
A__TIMES(s(X), Y) → MARK(Y)
MARK(square(X)) → MARK(X)
MARK(s(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)
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
A__SQUARE(X) → MARK(X)
A__PLUS(s(X), Y) → MARK(Y)
A__2NDSNEG(s(N), cons2(X, cons(Y, Z))) → A__2NDSPOS(mark(N), 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))) → A__2NDSNEG(mark(N), 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(N)
A__2NDSNEG(s(N), cons2(X, cons(Y, Z))) → MARK(Z)
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → MARK(N)
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → MARK(Z)
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.
(15) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MARK(from(X)) → A__FROM(mark(X))
MARK(from(X)) → MARK(X)
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → MARK(Y)
A__2NDSNEG(s(N), cons2(X, cons(Y, Z))) → MARK(Y)
MARK(cons(X1, X2)) → MARK(X1)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(MARK(x1)) = | 3A | + | 3A | · | x1 |
POL(from(x1)) = | 5A | + | 5A | · | x1 |
POL(A__FROM(x1)) = | 3A | + | 3A | · | x1 |
POL(mark(x1)) = | 0A | + | 0A | · | x1 |
POL(2ndspos(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__2NDSPOS(x1, x2)) = | -I | + | 3A | · | x1 | + | 3A | · | x2 |
POL(cons(x1, x2)) = | 5A | + | 5A | · | x1 | + | 0A | · | x2 |
POL(cons2(x1, x2)) = | 5A | + | -I | · | x1 | + | 0A | · | x2 |
POL(2ndsneg(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__2NDSNEG(x1, x2)) = | 0A | + | 3A | · | x1 | + | 3A | · | x2 |
POL(plus(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__PLUS(x1, x2)) = | 3A | + | 3A | · | x1 | + | 3A | · | x2 |
POL(times(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__TIMES(x1, x2)) = | 3A | + | 3A | · | x1 | + | 3A | · | x2 |
POL(a__times(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(square(x1)) = | -I | + | 0A | · | x1 |
POL(A__SQUARE(x1)) = | 3A | + | 3A | · | x1 |
POL(negrecip(x1)) = | -I | + | 0A | · | x1 |
POL(rcons(x1, x2)) = | 5A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(posrecip(x1)) = | 0A | + | -I | · | x1 |
POL(a__from(x1)) = | 5A | + | 5A | · | x1 |
POL(a__plus(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__pi(x1)) = | 5A | + | 0A | · | x1 |
POL(a__2ndsneg(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__2ndspos(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__square(x1)) = | 0A | + | 0A | · | x1 |
The following usable rules [FROCOS05] were oriented:
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
mark(negrecip(X)) → negrecip(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
a__from(X) → from(X)
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
mark(rnil) → rnil
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
a__plus(X1, X2) → plus(X1, X2)
a__pi(X) → pi(X)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__square(X) → square(X)
a__times(X1, X2) → times(X1, X2)
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndspos(0, Z) → rnil
a__from(X) → cons(mark(X), from(s(X)))
a__times(0, Y) → 0
mark(from(X)) → a__from(mark(X))
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(s(X), Y) → s(a__plus(mark(X), mark(Y)))
mark(0) → 0
mark(s(X)) → s(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))
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__plus(0, Y) → mark(Y)
mark(square(X)) → a__square(mark(X))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
a__square(X) → a__times(mark(X), mark(X))
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__FROM(X) → MARK(X)
MARK(2ndspos(X1, X2)) → A__2NDSPOS(mark(X1), mark(X2))
A__2NDSPOS(s(N), cons(X, Z)) → A__2NDSPOS(s(mark(N)), cons2(X, mark(Z)))
MARK(2ndspos(X1, X2)) → MARK(X1)
MARK(2ndspos(X1, X2)) → MARK(X2)
MARK(2ndsneg(X1, X2)) → A__2NDSNEG(mark(X1), mark(X2))
A__2NDSNEG(s(N), cons(X, Z)) → A__2NDSNEG(s(mark(N)), cons2(X, mark(Z)))
MARK(2ndsneg(X1, X2)) → MARK(X1)
MARK(2ndsneg(X1, X2)) → MARK(X2)
MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(0, Y) → MARK(Y)
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → A__TIMES(mark(X1), mark(X2))
A__TIMES(s(X), Y) → A__PLUS(mark(Y), a__times(mark(X), mark(Y)))
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
A__PLUS(s(X), Y) → MARK(X)
MARK(times(X1, X2)) → MARK(X1)
MARK(times(X1, X2)) → MARK(X2)
MARK(square(X)) → A__SQUARE(mark(X))
A__SQUARE(X) → A__TIMES(mark(X), mark(X))
A__TIMES(s(X), Y) → MARK(Y)
MARK(square(X)) → MARK(X)
MARK(s(X)) → MARK(X)
MARK(negrecip(X)) → MARK(X)
MARK(cons2(X1, X2)) → MARK(X2)
MARK(rcons(X1, X2)) → MARK(X1)
MARK(rcons(X1, X2)) → MARK(X2)
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
A__SQUARE(X) → MARK(X)
A__PLUS(s(X), Y) → MARK(Y)
A__2NDSNEG(s(N), cons2(X, cons(Y, Z))) → A__2NDSPOS(mark(N), 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))) → A__2NDSNEG(mark(N), 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(N)
A__2NDSNEG(s(N), cons2(X, cons(Y, Z))) → MARK(Z)
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → MARK(N)
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → MARK(Z)
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.
(17) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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))) → A__2NDSNEG(mark(N), mark(Z))
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))) → A__2NDSPOS(mark(N), mark(Z))
A__2NDSPOS(s(N), cons(X, Z)) → MARK(N)
MARK(2ndspos(X1, X2)) → A__2NDSPOS(mark(X1), mark(X2))
A__2NDSPOS(s(N), cons(X, Z)) → MARK(Z)
MARK(2ndspos(X1, X2)) → MARK(X1)
MARK(2ndspos(X1, X2)) → MARK(X2)
MARK(2ndsneg(X1, X2)) → A__2NDSNEG(mark(X1), mark(X2))
A__2NDSNEG(s(N), cons(X, Z)) → MARK(N)
MARK(2ndsneg(X1, X2)) → MARK(X1)
MARK(2ndsneg(X1, X2)) → MARK(X2)
MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(0, Y) → MARK(Y)
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → A__TIMES(mark(X1), mark(X2))
A__TIMES(s(X), Y) → A__PLUS(mark(Y), a__times(mark(X), mark(Y)))
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
A__PLUS(s(X), Y) → MARK(X)
MARK(times(X1, X2)) → MARK(X1)
MARK(times(X1, X2)) → MARK(X2)
MARK(square(X)) → A__SQUARE(mark(X))
A__SQUARE(X) → A__TIMES(mark(X), mark(X))
A__TIMES(s(X), Y) → MARK(Y)
MARK(square(X)) → MARK(X)
MARK(s(X)) → MARK(X)
MARK(negrecip(X)) → MARK(X)
MARK(cons2(X1, X2)) → MARK(X2)
MARK(rcons(X1, X2)) → MARK(X1)
MARK(rcons(X1, X2)) → MARK(X2)
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
A__SQUARE(X) → MARK(X)
A__PLUS(s(X), Y) → MARK(Y)
A__2NDSNEG(s(N), cons(X, Z)) → 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__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → MARK(N)
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → MARK(Z)
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.
(19) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MARK(2ndspos(X1, X2)) → MARK(X1)
MARK(2ndsneg(X1, X2)) → MARK(X1)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(A__2NDSPOS(x1, x2)) = | 1A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(cons(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(mark(x1)) = | 0A | + | 0A | · | x1 |
POL(cons2(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__2NDSNEG(x1, x2)) = | 1A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(MARK(x1)) = | 0A | + | 0A | · | x1 |
POL(2ndspos(x1, x2)) = | 1A | + | 1A | · | x1 | + | 0A | · | x2 |
POL(2ndsneg(x1, x2)) = | 1A | + | 1A | · | x1 | + | 0A | · | x2 |
POL(plus(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__PLUS(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(times(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__TIMES(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__times(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(square(x1)) = | -I | + | 0A | · | x1 |
POL(A__SQUARE(x1)) = | 0A | + | 0A | · | x1 |
POL(negrecip(x1)) = | -I | + | 0A | · | x1 |
POL(rcons(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(posrecip(x1)) = | 1A | + | -I | · | x1 |
POL(a__from(x1)) = | 0A | + | 0A | · | x1 |
POL(from(x1)) = | -I | + | 0A | · | x1 |
POL(a__plus(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__pi(x1)) = | 1A | + | 1A | · | x1 |
POL(a__2ndsneg(x1, x2)) = | 1A | + | 1A | · | x1 | + | 0A | · | x2 |
POL(a__2ndspos(x1, x2)) = | 1A | + | 1A | · | x1 | + | 0A | · | x2 |
POL(a__square(x1)) = | 0A | + | 0A | · | x1 |
The following usable rules [FROCOS05] were oriented:
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
mark(negrecip(X)) → negrecip(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
a__from(X) → from(X)
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
mark(rnil) → rnil
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
a__plus(X1, X2) → plus(X1, X2)
a__pi(X) → pi(X)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__square(X) → square(X)
a__times(X1, X2) → times(X1, X2)
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndspos(0, Z) → rnil
a__from(X) → cons(mark(X), from(s(X)))
a__times(0, Y) → 0
mark(from(X)) → a__from(mark(X))
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(s(X), Y) → s(a__plus(mark(X), mark(Y)))
mark(0) → 0
mark(s(X)) → s(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))
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__plus(0, Y) → mark(Y)
mark(square(X)) → a__square(mark(X))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
a__square(X) → a__times(mark(X), mark(X))
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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))) → A__2NDSNEG(mark(N), mark(Z))
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))) → A__2NDSPOS(mark(N), mark(Z))
A__2NDSPOS(s(N), cons(X, Z)) → MARK(N)
MARK(2ndspos(X1, X2)) → A__2NDSPOS(mark(X1), mark(X2))
A__2NDSPOS(s(N), cons(X, Z)) → MARK(Z)
MARK(2ndspos(X1, X2)) → MARK(X2)
MARK(2ndsneg(X1, X2)) → A__2NDSNEG(mark(X1), mark(X2))
A__2NDSNEG(s(N), cons(X, Z)) → MARK(N)
MARK(2ndsneg(X1, X2)) → MARK(X2)
MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(0, Y) → MARK(Y)
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → A__TIMES(mark(X1), mark(X2))
A__TIMES(s(X), Y) → A__PLUS(mark(Y), a__times(mark(X), mark(Y)))
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
A__PLUS(s(X), Y) → MARK(X)
MARK(times(X1, X2)) → MARK(X1)
MARK(times(X1, X2)) → MARK(X2)
MARK(square(X)) → A__SQUARE(mark(X))
A__SQUARE(X) → A__TIMES(mark(X), mark(X))
A__TIMES(s(X), Y) → MARK(Y)
MARK(square(X)) → MARK(X)
MARK(s(X)) → MARK(X)
MARK(negrecip(X)) → MARK(X)
MARK(cons2(X1, X2)) → MARK(X2)
MARK(rcons(X1, X2)) → MARK(X1)
MARK(rcons(X1, X2)) → MARK(X2)
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
A__SQUARE(X) → MARK(X)
A__PLUS(s(X), Y) → MARK(Y)
A__2NDSNEG(s(N), cons(X, Z)) → 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__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → MARK(N)
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → MARK(Z)
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.
(21) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MARK(square(X)) → A__SQUARE(mark(X))
MARK(square(X)) → MARK(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(A__2NDSPOS(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(cons(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(mark(x1)) = | 0A | + | 0A | · | x1 |
POL(cons2(x1, x2)) = | -I | + | -I | · | x1 | + | 0A | · | x2 |
POL(A__2NDSNEG(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(MARK(x1)) = | 0A | + | 0A | · | x1 |
POL(2ndspos(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(2ndsneg(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(plus(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__PLUS(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(times(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__TIMES(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__times(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(square(x1)) = | 1A | + | 1A | · | x1 |
POL(A__SQUARE(x1)) = | 0A | + | 0A | · | x1 |
POL(negrecip(x1)) = | -I | + | 0A | · | x1 |
POL(rcons(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(posrecip(x1)) = | 0A | + | 0A | · | x1 |
POL(a__from(x1)) = | 0A | + | 0A | · | x1 |
POL(from(x1)) = | -I | + | 0A | · | x1 |
POL(a__plus(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__pi(x1)) = | 5A | + | 0A | · | x1 |
POL(a__2ndsneg(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__2ndspos(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__square(x1)) = | 1A | + | 1A | · | x1 |
The following usable rules [FROCOS05] were oriented:
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
mark(negrecip(X)) → negrecip(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
a__from(X) → from(X)
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
mark(rnil) → rnil
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
a__plus(X1, X2) → plus(X1, X2)
a__pi(X) → pi(X)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__square(X) → square(X)
a__times(X1, X2) → times(X1, X2)
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndspos(0, Z) → rnil
a__from(X) → cons(mark(X), from(s(X)))
a__times(0, Y) → 0
mark(from(X)) → a__from(mark(X))
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(s(X), Y) → s(a__plus(mark(X), mark(Y)))
mark(0) → 0
mark(s(X)) → s(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))
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__plus(0, Y) → mark(Y)
mark(square(X)) → a__square(mark(X))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
a__square(X) → a__times(mark(X), mark(X))
(22) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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))) → A__2NDSNEG(mark(N), mark(Z))
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))) → A__2NDSPOS(mark(N), mark(Z))
A__2NDSPOS(s(N), cons(X, Z)) → MARK(N)
MARK(2ndspos(X1, X2)) → A__2NDSPOS(mark(X1), mark(X2))
A__2NDSPOS(s(N), cons(X, Z)) → MARK(Z)
MARK(2ndspos(X1, X2)) → MARK(X2)
MARK(2ndsneg(X1, X2)) → A__2NDSNEG(mark(X1), mark(X2))
A__2NDSNEG(s(N), cons(X, Z)) → MARK(N)
MARK(2ndsneg(X1, X2)) → MARK(X2)
MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(0, Y) → MARK(Y)
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → A__TIMES(mark(X1), mark(X2))
A__TIMES(s(X), Y) → A__PLUS(mark(Y), a__times(mark(X), mark(Y)))
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
A__PLUS(s(X), Y) → MARK(X)
MARK(times(X1, X2)) → MARK(X1)
MARK(times(X1, X2)) → MARK(X2)
A__SQUARE(X) → A__TIMES(mark(X), mark(X))
A__TIMES(s(X), Y) → MARK(Y)
MARK(s(X)) → MARK(X)
MARK(negrecip(X)) → MARK(X)
MARK(cons2(X1, X2)) → MARK(X2)
MARK(rcons(X1, X2)) → MARK(X1)
MARK(rcons(X1, X2)) → MARK(X2)
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
A__SQUARE(X) → MARK(X)
A__PLUS(s(X), Y) → MARK(Y)
A__2NDSNEG(s(N), cons(X, Z)) → 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__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → MARK(N)
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → MARK(Z)
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.
(23) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.
(24) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → A__2NDSNEG(mark(N), mark(Z))
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))) → A__2NDSPOS(mark(N), mark(Z))
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))) → MARK(N)
MARK(2ndspos(X1, X2)) → A__2NDSPOS(mark(X1), mark(X2))
A__2NDSPOS(s(N), cons(X, Z)) → MARK(N)
MARK(2ndspos(X1, X2)) → MARK(X2)
MARK(2ndsneg(X1, X2)) → A__2NDSNEG(mark(X1), mark(X2))
A__2NDSNEG(s(N), cons(X, Z)) → MARK(N)
MARK(2ndsneg(X1, X2)) → MARK(X2)
MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(0, Y) → MARK(Y)
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → A__TIMES(mark(X1), mark(X2))
A__TIMES(s(X), Y) → A__PLUS(mark(Y), a__times(mark(X), mark(Y)))
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
A__PLUS(s(X), Y) → MARK(X)
MARK(times(X1, X2)) → MARK(X1)
MARK(times(X1, X2)) → MARK(X2)
MARK(s(X)) → MARK(X)
MARK(negrecip(X)) → MARK(X)
MARK(cons2(X1, X2)) → MARK(X2)
MARK(rcons(X1, X2)) → MARK(X1)
MARK(rcons(X1, X2)) → MARK(X2)
A__PLUS(s(X), Y) → MARK(Y)
A__TIMES(s(X), Y) → MARK(Y)
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
A__2NDSNEG(s(N), cons(X, Z)) → 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__2NDSPOS(s(N), cons(X, Z)) → MARK(Z)
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → MARK(Z)
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.
(25) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MARK(times(X1, X2)) → MARK(X2)
A__TIMES(s(X), Y) → MARK(Y)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(A__2NDSPOS(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(cons2(x1, x2)) = | 0A | + | -I | · | x1 | + | 0A | · | x2 |
POL(cons(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__2NDSNEG(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(mark(x1)) = | -I | + | 0A | · | x1 |
POL(MARK(x1)) = | 0A | + | 0A | · | x1 |
POL(2ndspos(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(2ndsneg(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(plus(x1, x2)) = | 0A | + | 1A | · | x1 | + | 0A | · | x2 |
POL(A__PLUS(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(times(x1, x2)) = | 1A | + | 0A | · | x1 | + | 5A | · | x2 |
POL(A__TIMES(x1, x2)) = | 1A | + | 0A | · | x1 | + | 5A | · | x2 |
POL(a__times(x1, x2)) = | 1A | + | 0A | · | x1 | + | 5A | · | x2 |
POL(negrecip(x1)) = | -I | + | 0A | · | x1 |
POL(rcons(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(posrecip(x1)) = | -I | + | 0A | · | x1 |
POL(a__from(x1)) = | -I | + | 0A | · | x1 |
POL(from(x1)) = | -I | + | 0A | · | x1 |
POL(a__plus(x1, x2)) = | 0A | + | 1A | · | x1 | + | 0A | · | x2 |
POL(a__pi(x1)) = | 5A | + | 0A | · | x1 |
POL(a__2ndsneg(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__2ndspos(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__square(x1)) = | 1A | + | 5A | · | x1 |
POL(square(x1)) = | 1A | + | 5A | · | x1 |
The following usable rules [FROCOS05] were oriented:
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
mark(negrecip(X)) → negrecip(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
a__from(X) → from(X)
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
mark(rnil) → rnil
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
a__plus(X1, X2) → plus(X1, X2)
a__pi(X) → pi(X)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__square(X) → square(X)
a__times(X1, X2) → times(X1, X2)
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndspos(0, Z) → rnil
a__from(X) → cons(mark(X), from(s(X)))
a__times(0, Y) → 0
mark(from(X)) → a__from(mark(X))
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(s(X), Y) → s(a__plus(mark(X), mark(Y)))
mark(0) → 0
mark(s(X)) → s(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))
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__plus(0, Y) → mark(Y)
mark(square(X)) → a__square(mark(X))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
a__square(X) → a__times(mark(X), mark(X))
(26) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → A__2NDSNEG(mark(N), mark(Z))
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))) → A__2NDSPOS(mark(N), mark(Z))
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))) → MARK(N)
MARK(2ndspos(X1, X2)) → A__2NDSPOS(mark(X1), mark(X2))
A__2NDSPOS(s(N), cons(X, Z)) → MARK(N)
MARK(2ndspos(X1, X2)) → MARK(X2)
MARK(2ndsneg(X1, X2)) → A__2NDSNEG(mark(X1), mark(X2))
A__2NDSNEG(s(N), cons(X, Z)) → MARK(N)
MARK(2ndsneg(X1, X2)) → MARK(X2)
MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(0, Y) → MARK(Y)
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → A__TIMES(mark(X1), mark(X2))
A__TIMES(s(X), Y) → A__PLUS(mark(Y), a__times(mark(X), mark(Y)))
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
A__PLUS(s(X), Y) → MARK(X)
MARK(times(X1, X2)) → MARK(X1)
MARK(s(X)) → MARK(X)
MARK(negrecip(X)) → MARK(X)
MARK(cons2(X1, X2)) → MARK(X2)
MARK(rcons(X1, X2)) → MARK(X1)
MARK(rcons(X1, X2)) → MARK(X2)
A__PLUS(s(X), Y) → MARK(Y)
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
A__2NDSNEG(s(N), cons(X, Z)) → 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__2NDSPOS(s(N), cons(X, Z)) → MARK(Z)
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → MARK(Z)
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.
(27) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MARK(2ndspos(X1, X2)) → MARK(X2)
MARK(2ndsneg(X1, X2)) → MARK(X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(A__2NDSPOS(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(cons2(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(cons(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__2NDSNEG(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(mark(x1)) = | 0A | + | 0A | · | x1 |
POL(MARK(x1)) = | 0A | + | 0A | · | x1 |
POL(2ndspos(x1, x2)) = | 1A | + | 0A | · | x1 | + | 1A | · | x2 |
POL(2ndsneg(x1, x2)) = | 1A | + | 0A | · | x1 | + | 1A | · | x2 |
POL(plus(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__PLUS(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(times(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__TIMES(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__times(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(negrecip(x1)) = | -I | + | 0A | · | x1 |
POL(rcons(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(posrecip(x1)) = | 1A | + | -I | · | x1 |
POL(a__from(x1)) = | 0A | + | 0A | · | x1 |
POL(from(x1)) = | -I | + | 0A | · | x1 |
POL(a__plus(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__pi(x1)) = | 2A | + | 0A | · | x1 |
POL(a__2ndsneg(x1, x2)) = | 1A | + | 0A | · | x1 | + | 1A | · | x2 |
POL(a__2ndspos(x1, x2)) = | 1A | + | 0A | · | x1 | + | 1A | · | x2 |
POL(a__square(x1)) = | 0A | + | 0A | · | x1 |
POL(square(x1)) = | -I | + | 0A | · | x1 |
The following usable rules [FROCOS05] were oriented:
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
mark(negrecip(X)) → negrecip(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
a__from(X) → from(X)
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
mark(rnil) → rnil
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
a__plus(X1, X2) → plus(X1, X2)
a__pi(X) → pi(X)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__square(X) → square(X)
a__times(X1, X2) → times(X1, X2)
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndspos(0, Z) → rnil
a__from(X) → cons(mark(X), from(s(X)))
a__times(0, Y) → 0
mark(from(X)) → a__from(mark(X))
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(s(X), Y) → s(a__plus(mark(X), mark(Y)))
mark(0) → 0
mark(s(X)) → s(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))
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__plus(0, Y) → mark(Y)
mark(square(X)) → a__square(mark(X))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
a__square(X) → a__times(mark(X), mark(X))
(28) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → A__2NDSNEG(mark(N), mark(Z))
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))) → A__2NDSPOS(mark(N), mark(Z))
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))) → MARK(N)
MARK(2ndspos(X1, X2)) → A__2NDSPOS(mark(X1), mark(X2))
A__2NDSPOS(s(N), cons(X, Z)) → MARK(N)
MARK(2ndsneg(X1, X2)) → A__2NDSNEG(mark(X1), mark(X2))
A__2NDSNEG(s(N), cons(X, Z)) → MARK(N)
MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(0, Y) → MARK(Y)
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → A__TIMES(mark(X1), mark(X2))
A__TIMES(s(X), Y) → A__PLUS(mark(Y), a__times(mark(X), mark(Y)))
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
A__PLUS(s(X), Y) → MARK(X)
MARK(times(X1, X2)) → MARK(X1)
MARK(s(X)) → MARK(X)
MARK(negrecip(X)) → MARK(X)
MARK(cons2(X1, X2)) → MARK(X2)
MARK(rcons(X1, X2)) → MARK(X1)
MARK(rcons(X1, X2)) → MARK(X2)
A__PLUS(s(X), Y) → MARK(Y)
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
A__2NDSNEG(s(N), cons(X, Z)) → 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__2NDSPOS(s(N), cons(X, Z)) → MARK(Z)
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → MARK(Z)
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.
(29) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MARK(plus(X1, X2)) → MARK(X1)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(A__2NDSPOS(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(cons2(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(cons(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__2NDSNEG(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(mark(x1)) = | 0A | + | 0A | · | x1 |
POL(MARK(x1)) = | -I | + | 0A | · | x1 |
POL(2ndspos(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(2ndsneg(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(plus(x1, x2)) = | 1A | + | 1A | · | x1 | + | 0A | · | x2 |
POL(A__PLUS(x1, x2)) = | 1A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(times(x1, x2)) = | 1A | + | 0A | · | x1 | + | 1A | · | x2 |
POL(A__TIMES(x1, x2)) = | 1A | + | 0A | · | x1 | + | 1A | · | x2 |
POL(a__times(x1, x2)) = | 1A | + | 0A | · | x1 | + | 1A | · | x2 |
POL(negrecip(x1)) = | -I | + | 0A | · | x1 |
POL(rcons(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(posrecip(x1)) = | 0A | + | -I | · | x1 |
POL(a__from(x1)) = | 0A | + | 0A | · | x1 |
POL(from(x1)) = | -I | + | 0A | · | x1 |
POL(a__plus(x1, x2)) = | 1A | + | 1A | · | x1 | + | 0A | · | x2 |
POL(a__pi(x1)) = | 5A | + | 0A | · | x1 |
POL(a__2ndsneg(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__2ndspos(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__square(x1)) = | 1A | + | 1A | · | x1 |
POL(square(x1)) = | 1A | + | 1A | · | x1 |
The following usable rules [FROCOS05] were oriented:
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
mark(negrecip(X)) → negrecip(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
a__from(X) → from(X)
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
mark(rnil) → rnil
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
a__plus(X1, X2) → plus(X1, X2)
a__pi(X) → pi(X)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__square(X) → square(X)
a__times(X1, X2) → times(X1, X2)
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndspos(0, Z) → rnil
a__from(X) → cons(mark(X), from(s(X)))
a__times(0, Y) → 0
mark(from(X)) → a__from(mark(X))
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(s(X), Y) → s(a__plus(mark(X), mark(Y)))
mark(0) → 0
mark(s(X)) → s(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))
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__plus(0, Y) → mark(Y)
mark(square(X)) → a__square(mark(X))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
a__square(X) → a__times(mark(X), mark(X))
(30) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → A__2NDSNEG(mark(N), mark(Z))
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))) → A__2NDSPOS(mark(N), mark(Z))
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))) → MARK(N)
MARK(2ndspos(X1, X2)) → A__2NDSPOS(mark(X1), mark(X2))
A__2NDSPOS(s(N), cons(X, Z)) → MARK(N)
MARK(2ndsneg(X1, X2)) → A__2NDSNEG(mark(X1), mark(X2))
A__2NDSNEG(s(N), cons(X, Z)) → MARK(N)
MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(0, Y) → MARK(Y)
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → A__TIMES(mark(X1), mark(X2))
A__TIMES(s(X), Y) → A__PLUS(mark(Y), a__times(mark(X), mark(Y)))
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
A__PLUS(s(X), Y) → MARK(X)
MARK(times(X1, X2)) → MARK(X1)
MARK(s(X)) → MARK(X)
MARK(negrecip(X)) → MARK(X)
MARK(cons2(X1, X2)) → MARK(X2)
MARK(rcons(X1, X2)) → MARK(X1)
MARK(rcons(X1, X2)) → MARK(X2)
A__PLUS(s(X), Y) → MARK(Y)
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
A__2NDSNEG(s(N), cons(X, Z)) → 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__2NDSPOS(s(N), cons(X, Z)) → MARK(Z)
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → MARK(Z)
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.
(31) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
A__2NDSNEG(s(N), cons(X, Z)) → MARK(Z)
A__2NDSNEG(s(N), cons2(X, cons(Y, Z))) → MARK(Z)
A__2NDSPOS(s(N), cons(X, Z)) → MARK(Z)
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → MARK(Z)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(A__2NDSPOS(x1, x2)) = | 0A | + | 0A | · | x1 | + | 1A | · | x2 |
POL(cons2(x1, x2)) = | -I | + | -I | · | x1 | + | 0A | · | x2 |
POL(cons(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__2NDSNEG(x1, x2)) = | -I | + | 0A | · | x1 | + | 1A | · | x2 |
POL(mark(x1)) = | 0A | + | 0A | · | x1 |
POL(MARK(x1)) = | 0A | + | 0A | · | x1 |
POL(2ndspos(x1, x2)) = | 1A | + | 0A | · | x1 | + | 1A | · | x2 |
POL(2ndsneg(x1, x2)) = | 1A | + | 0A | · | x1 | + | 1A | · | x2 |
POL(plus(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__PLUS(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(times(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__TIMES(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__times(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(negrecip(x1)) = | 0A | + | 0A | · | x1 |
POL(rcons(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(posrecip(x1)) = | 0A | + | -I | · | x1 |
POL(a__from(x1)) = | 0A | + | 0A | · | x1 |
POL(from(x1)) = | -I | + | 0A | · | x1 |
POL(a__plus(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__pi(x1)) = | 1A | + | 0A | · | x1 |
POL(a__2ndsneg(x1, x2)) = | 1A | + | 0A | · | x1 | + | 1A | · | x2 |
POL(a__2ndspos(x1, x2)) = | 1A | + | 0A | · | x1 | + | 1A | · | x2 |
POL(a__square(x1)) = | 0A | + | 0A | · | x1 |
POL(square(x1)) = | -I | + | 0A | · | x1 |
The following usable rules [FROCOS05] were oriented:
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
mark(negrecip(X)) → negrecip(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
a__from(X) → from(X)
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
mark(rnil) → rnil
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
a__plus(X1, X2) → plus(X1, X2)
a__pi(X) → pi(X)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__square(X) → square(X)
a__times(X1, X2) → times(X1, X2)
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndspos(0, Z) → rnil
a__from(X) → cons(mark(X), from(s(X)))
a__times(0, Y) → 0
mark(from(X)) → a__from(mark(X))
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(s(X), Y) → s(a__plus(mark(X), mark(Y)))
mark(0) → 0
mark(s(X)) → s(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))
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__plus(0, Y) → mark(Y)
mark(square(X)) → a__square(mark(X))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
a__square(X) → a__times(mark(X), mark(X))
(32) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → A__2NDSNEG(mark(N), mark(Z))
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))) → A__2NDSPOS(mark(N), mark(Z))
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))) → MARK(N)
MARK(2ndspos(X1, X2)) → A__2NDSPOS(mark(X1), mark(X2))
A__2NDSPOS(s(N), cons(X, Z)) → MARK(N)
MARK(2ndsneg(X1, X2)) → A__2NDSNEG(mark(X1), mark(X2))
A__2NDSNEG(s(N), cons(X, Z)) → MARK(N)
MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(0, Y) → MARK(Y)
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → A__TIMES(mark(X1), mark(X2))
A__TIMES(s(X), Y) → A__PLUS(mark(Y), a__times(mark(X), mark(Y)))
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
A__PLUS(s(X), Y) → MARK(X)
MARK(times(X1, X2)) → MARK(X1)
MARK(s(X)) → MARK(X)
MARK(negrecip(X)) → MARK(X)
MARK(cons2(X1, X2)) → MARK(X2)
MARK(rcons(X1, X2)) → MARK(X1)
MARK(rcons(X1, X2)) → MARK(X2)
A__PLUS(s(X), Y) → MARK(Y)
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
A__2NDSNEG(s(N), cons2(X, cons(Y, Z))) → MARK(N)
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.
(33) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
A__PLUS(s(X), Y) → MARK(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(A__2NDSPOS(x1, x2)) = | -I | + | 0A | · | x1 | + | -I | · | x2 |
POL(cons2(x1, x2)) = | -I | + | -I | · | x1 | + | 0A | · | x2 |
POL(cons(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__2NDSNEG(x1, x2)) = | 1A | + | 0A | · | x1 | + | -I | · | x2 |
POL(mark(x1)) = | 0A | + | 0A | · | x1 |
POL(MARK(x1)) = | 1A | + | 0A | · | x1 |
POL(2ndspos(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(2ndsneg(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(plus(x1, x2)) = | 1A | + | 1A | · | x1 | + | 0A | · | x2 |
POL(A__PLUS(x1, x2)) = | -I | + | 1A | · | x1 | + | 0A | · | x2 |
POL(times(x1, x2)) = | 1A | + | 1A | · | x1 | + | 1A | · | x2 |
POL(A__TIMES(x1, x2)) = | -I | + | 1A | · | x1 | + | 1A | · | x2 |
POL(a__times(x1, x2)) = | 1A | + | 1A | · | x1 | + | 1A | · | x2 |
POL(negrecip(x1)) = | -I | + | 0A | · | x1 |
POL(rcons(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(posrecip(x1)) = | -I | + | 0A | · | x1 |
POL(a__from(x1)) = | 1A | + | 0A | · | x1 |
POL(from(x1)) = | 1A | + | 0A | · | x1 |
POL(a__plus(x1, x2)) = | 1A | + | 1A | · | x1 | + | 0A | · | x2 |
POL(a__pi(x1)) = | 1A | + | 0A | · | x1 |
POL(a__2ndsneg(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__2ndspos(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__square(x1)) = | 1A | + | 1A | · | x1 |
POL(square(x1)) = | 1A | + | 1A | · | x1 |
The following usable rules [FROCOS05] were oriented:
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
mark(negrecip(X)) → negrecip(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
a__from(X) → from(X)
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
mark(rnil) → rnil
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
a__plus(X1, X2) → plus(X1, X2)
a__pi(X) → pi(X)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__square(X) → square(X)
a__times(X1, X2) → times(X1, X2)
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndspos(0, Z) → rnil
a__from(X) → cons(mark(X), from(s(X)))
a__times(0, Y) → 0
mark(from(X)) → a__from(mark(X))
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(s(X), Y) → s(a__plus(mark(X), mark(Y)))
mark(0) → 0
mark(s(X)) → s(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))
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__plus(0, Y) → mark(Y)
mark(square(X)) → a__square(mark(X))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
a__square(X) → a__times(mark(X), mark(X))
(34) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → A__2NDSNEG(mark(N), mark(Z))
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))) → A__2NDSPOS(mark(N), mark(Z))
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))) → MARK(N)
MARK(2ndspos(X1, X2)) → A__2NDSPOS(mark(X1), mark(X2))
A__2NDSPOS(s(N), cons(X, Z)) → MARK(N)
MARK(2ndsneg(X1, X2)) → A__2NDSNEG(mark(X1), mark(X2))
A__2NDSNEG(s(N), cons(X, Z)) → MARK(N)
MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(0, Y) → MARK(Y)
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → A__TIMES(mark(X1), mark(X2))
A__TIMES(s(X), Y) → A__PLUS(mark(Y), a__times(mark(X), mark(Y)))
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
MARK(times(X1, X2)) → MARK(X1)
MARK(s(X)) → MARK(X)
MARK(negrecip(X)) → MARK(X)
MARK(cons2(X1, X2)) → MARK(X2)
MARK(rcons(X1, X2)) → MARK(X1)
MARK(rcons(X1, X2)) → MARK(X2)
A__PLUS(s(X), Y) → MARK(Y)
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
A__2NDSNEG(s(N), cons2(X, cons(Y, Z))) → MARK(N)
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.
(35) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MARK(negrecip(X)) → MARK(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(A__2NDSPOS(x1, x2)) = | -I | + | 0A | · | x1 | + | -I | · | x2 |
POL(cons2(x1, x2)) = | -I | + | -I | · | x1 | + | 0A | · | x2 |
POL(cons(x1, x2)) = | -I | + | 4A | · | x1 | + | 0A | · | x2 |
POL(A__2NDSNEG(x1, x2)) = | -I | + | 0A | · | x1 | + | -I | · | x2 |
POL(mark(x1)) = | -I | + | 0A | · | x1 |
POL(MARK(x1)) = | -I | + | 0A | · | x1 |
POL(2ndspos(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(2ndsneg(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(plus(x1, x2)) = | 0A | + | -I | · | x1 | + | 0A | · | x2 |
POL(A__PLUS(x1, x2)) = | -I | + | -I | · | x1 | + | 0A | · | x2 |
POL(times(x1, x2)) = | 0A | + | 0A | · | x1 | + | -I | · | x2 |
POL(A__TIMES(x1, x2)) = | 0A | + | 0A | · | x1 | + | -I | · | x2 |
POL(a__times(x1, x2)) = | 0A | + | 0A | · | x1 | + | -I | · | x2 |
POL(negrecip(x1)) = | -I | + | 4A | · | x1 |
POL(rcons(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(posrecip(x1)) = | -I | + | 0A | · | x1 |
POL(a__from(x1)) = | -I | + | 4A | · | x1 |
POL(from(x1)) = | -I | + | 4A | · | x1 |
POL(a__plus(x1, x2)) = | 0A | + | -I | · | x1 | + | 0A | · | x2 |
POL(a__pi(x1)) = | 4A | + | 0A | · | x1 |
POL(a__2ndsneg(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__2ndspos(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__square(x1)) = | 0A | + | 1A | · | x1 |
POL(square(x1)) = | 0A | + | 1A | · | x1 |
The following usable rules [FROCOS05] were oriented:
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
mark(negrecip(X)) → negrecip(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
a__from(X) → from(X)
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
mark(rnil) → rnil
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
a__plus(X1, X2) → plus(X1, X2)
a__pi(X) → pi(X)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__square(X) → square(X)
a__times(X1, X2) → times(X1, X2)
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndspos(0, Z) → rnil
a__from(X) → cons(mark(X), from(s(X)))
a__times(0, Y) → 0
mark(from(X)) → a__from(mark(X))
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(s(X), Y) → s(a__plus(mark(X), mark(Y)))
mark(0) → 0
mark(s(X)) → s(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))
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__plus(0, Y) → mark(Y)
mark(square(X)) → a__square(mark(X))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
a__square(X) → a__times(mark(X), mark(X))
(36) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → A__2NDSNEG(mark(N), mark(Z))
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))) → A__2NDSPOS(mark(N), mark(Z))
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))) → MARK(N)
MARK(2ndspos(X1, X2)) → A__2NDSPOS(mark(X1), mark(X2))
A__2NDSPOS(s(N), cons(X, Z)) → MARK(N)
MARK(2ndsneg(X1, X2)) → A__2NDSNEG(mark(X1), mark(X2))
A__2NDSNEG(s(N), cons(X, Z)) → MARK(N)
MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(0, Y) → MARK(Y)
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → A__TIMES(mark(X1), mark(X2))
A__TIMES(s(X), Y) → A__PLUS(mark(Y), a__times(mark(X), mark(Y)))
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
MARK(times(X1, X2)) → MARK(X1)
MARK(s(X)) → MARK(X)
MARK(cons2(X1, X2)) → MARK(X2)
MARK(rcons(X1, X2)) → MARK(X1)
MARK(rcons(X1, X2)) → MARK(X2)
A__PLUS(s(X), Y) → MARK(Y)
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
A__2NDSNEG(s(N), cons2(X, cons(Y, Z))) → MARK(N)
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.
(37) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MARK(cons2(X1, X2)) → MARK(X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(2ndsneg(x1, x2)) = x1
POL(2ndspos(x1, x2)) = x1
POL(A__2NDSNEG(x1, x2)) = x1
POL(A__2NDSPOS(x1, x2)) = x1
POL(A__PLUS(x1, x2)) = x2
POL(A__TIMES(x1, x2)) = x1
POL(MARK(x1)) = x1
POL(a__2ndsneg(x1, x2)) = x1
POL(a__2ndspos(x1, x2)) = x1
POL(a__from(x1)) = 0
POL(a__pi(x1)) = x1
POL(a__plus(x1, x2)) = x2
POL(a__square(x1)) = x1
POL(a__times(x1, x2)) = x1
POL(cons(x1, x2)) = 0
POL(cons2(x1, x2)) = 1 + x1 + x2
POL(from(x1)) = 0
POL(mark(x1)) = x1
POL(negrecip(x1)) = 0
POL(nil) = 0
POL(pi(x1)) = x1
POL(plus(x1, x2)) = x2
POL(posrecip(x1)) = 0
POL(rcons(x1, x2)) = x1 + x2
POL(rnil) = 0
POL(s(x1)) = x1
POL(square(x1)) = x1
POL(times(x1, x2)) = x1
The following usable rules [FROCOS05] were oriented:
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
mark(negrecip(X)) → negrecip(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
a__from(X) → from(X)
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
mark(rnil) → rnil
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
a__plus(X1, X2) → plus(X1, X2)
a__pi(X) → pi(X)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__square(X) → square(X)
a__times(X1, X2) → times(X1, X2)
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndspos(0, Z) → rnil
a__from(X) → cons(mark(X), from(s(X)))
a__times(0, Y) → 0
mark(from(X)) → a__from(mark(X))
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(s(X), Y) → s(a__plus(mark(X), mark(Y)))
mark(0) → 0
mark(s(X)) → s(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))
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__plus(0, Y) → mark(Y)
mark(square(X)) → a__square(mark(X))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
a__square(X) → a__times(mark(X), mark(X))
(38) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → A__2NDSNEG(mark(N), mark(Z))
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))) → A__2NDSPOS(mark(N), mark(Z))
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))) → MARK(N)
MARK(2ndspos(X1, X2)) → A__2NDSPOS(mark(X1), mark(X2))
A__2NDSPOS(s(N), cons(X, Z)) → MARK(N)
MARK(2ndsneg(X1, X2)) → A__2NDSNEG(mark(X1), mark(X2))
A__2NDSNEG(s(N), cons(X, Z)) → MARK(N)
MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(0, Y) → MARK(Y)
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → A__TIMES(mark(X1), mark(X2))
A__TIMES(s(X), Y) → A__PLUS(mark(Y), a__times(mark(X), mark(Y)))
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
MARK(times(X1, X2)) → MARK(X1)
MARK(s(X)) → MARK(X)
MARK(rcons(X1, X2)) → MARK(X1)
MARK(rcons(X1, X2)) → MARK(X2)
A__PLUS(s(X), Y) → MARK(Y)
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
A__2NDSNEG(s(N), cons2(X, cons(Y, Z))) → MARK(N)
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.
(39) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MARK(times(X1, X2)) → MARK(X1)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(2ndsneg(x1, x2)) = x1
POL(2ndspos(x1, x2)) = x1
POL(A__2NDSNEG(x1, x2)) = x1
POL(A__2NDSPOS(x1, x2)) = x1
POL(A__PLUS(x1, x2)) = x2
POL(A__TIMES(x1, x2)) = 1 + x1
POL(MARK(x1)) = x1
POL(a__2ndsneg(x1, x2)) = x1
POL(a__2ndspos(x1, x2)) = x1
POL(a__from(x1)) = x1
POL(a__pi(x1)) = x1
POL(a__plus(x1, x2)) = x2
POL(a__square(x1)) = 1 + x1
POL(a__times(x1, x2)) = 1 + x1
POL(cons(x1, x2)) = 0
POL(cons2(x1, x2)) = x1
POL(from(x1)) = x1
POL(mark(x1)) = x1
POL(negrecip(x1)) = 0
POL(nil) = 0
POL(pi(x1)) = x1
POL(plus(x1, x2)) = x2
POL(posrecip(x1)) = 0
POL(rcons(x1, x2)) = x1 + x2
POL(rnil) = 0
POL(s(x1)) = x1
POL(square(x1)) = 1 + x1
POL(times(x1, x2)) = 1 + x1
The following usable rules [FROCOS05] were oriented:
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
mark(negrecip(X)) → negrecip(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
a__from(X) → from(X)
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
mark(rnil) → rnil
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
a__plus(X1, X2) → plus(X1, X2)
a__pi(X) → pi(X)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__square(X) → square(X)
a__times(X1, X2) → times(X1, X2)
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndspos(0, Z) → rnil
a__from(X) → cons(mark(X), from(s(X)))
a__times(0, Y) → 0
mark(from(X)) → a__from(mark(X))
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(s(X), Y) → s(a__plus(mark(X), mark(Y)))
mark(0) → 0
mark(s(X)) → s(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))
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__plus(0, Y) → mark(Y)
mark(square(X)) → a__square(mark(X))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
a__square(X) → a__times(mark(X), mark(X))
(40) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → A__2NDSNEG(mark(N), mark(Z))
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))) → A__2NDSPOS(mark(N), mark(Z))
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))) → MARK(N)
MARK(2ndspos(X1, X2)) → A__2NDSPOS(mark(X1), mark(X2))
A__2NDSPOS(s(N), cons(X, Z)) → MARK(N)
MARK(2ndsneg(X1, X2)) → A__2NDSNEG(mark(X1), mark(X2))
A__2NDSNEG(s(N), cons(X, Z)) → MARK(N)
MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(0, Y) → MARK(Y)
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → A__TIMES(mark(X1), mark(X2))
A__TIMES(s(X), Y) → A__PLUS(mark(Y), a__times(mark(X), mark(Y)))
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
MARK(s(X)) → MARK(X)
MARK(rcons(X1, X2)) → MARK(X1)
MARK(rcons(X1, X2)) → MARK(X2)
A__PLUS(s(X), Y) → MARK(Y)
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
A__2NDSNEG(s(N), cons2(X, cons(Y, Z))) → MARK(N)
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.
(41) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MARK(2ndspos(X1, X2)) → A__2NDSPOS(mark(X1), mark(X2))
MARK(2ndsneg(X1, X2)) → A__2NDSNEG(mark(X1), mark(X2))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(2ndsneg(x1, x2)) = 1 + x1
POL(2ndspos(x1, x2)) = 1 + x1
POL(A__2NDSNEG(x1, x2)) = x1
POL(A__2NDSPOS(x1, x2)) = x1
POL(A__PLUS(x1, x2)) = x2
POL(A__TIMES(x1, x2)) = x1
POL(MARK(x1)) = x1
POL(a__2ndsneg(x1, x2)) = 1 + x1
POL(a__2ndspos(x1, x2)) = 1 + x1
POL(a__from(x1)) = 0
POL(a__pi(x1)) = 1 + x1
POL(a__plus(x1, x2)) = x2
POL(a__square(x1)) = x1
POL(a__times(x1, x2)) = x1
POL(cons(x1, x2)) = 0
POL(cons2(x1, x2)) = 0
POL(from(x1)) = 0
POL(mark(x1)) = x1
POL(negrecip(x1)) = 0
POL(nil) = 0
POL(pi(x1)) = 1 + x1
POL(plus(x1, x2)) = x2
POL(posrecip(x1)) = 0
POL(rcons(x1, x2)) = x1 + x2
POL(rnil) = 1
POL(s(x1)) = x1
POL(square(x1)) = x1
POL(times(x1, x2)) = x1
The following usable rules [FROCOS05] were oriented:
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
mark(negrecip(X)) → negrecip(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
a__from(X) → from(X)
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
mark(rnil) → rnil
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
a__plus(X1, X2) → plus(X1, X2)
a__pi(X) → pi(X)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__square(X) → square(X)
a__times(X1, X2) → times(X1, X2)
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndspos(0, Z) → rnil
a__from(X) → cons(mark(X), from(s(X)))
a__times(0, Y) → 0
mark(from(X)) → a__from(mark(X))
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(s(X), Y) → s(a__plus(mark(X), mark(Y)))
mark(0) → 0
mark(s(X)) → s(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))
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__plus(0, Y) → mark(Y)
mark(square(X)) → a__square(mark(X))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
a__square(X) → a__times(mark(X), mark(X))
(42) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → A__2NDSNEG(mark(N), mark(Z))
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))) → A__2NDSPOS(mark(N), mark(Z))
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))) → MARK(N)
A__2NDSPOS(s(N), cons(X, Z)) → MARK(N)
A__2NDSNEG(s(N), cons(X, Z)) → MARK(N)
MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(0, Y) → MARK(Y)
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → A__TIMES(mark(X1), mark(X2))
A__TIMES(s(X), Y) → A__PLUS(mark(Y), a__times(mark(X), mark(Y)))
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
MARK(s(X)) → MARK(X)
MARK(rcons(X1, X2)) → MARK(X1)
MARK(rcons(X1, X2)) → MARK(X2)
A__PLUS(s(X), Y) → MARK(Y)
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
A__2NDSNEG(s(N), cons2(X, cons(Y, Z))) → MARK(N)
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.
(43) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 4 less nodes.
(44) Complex Obligation (AND)
(45) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__PLUS(0, Y) → MARK(Y)
MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
A__PLUS(s(X), Y) → MARK(Y)
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → A__TIMES(mark(X1), mark(X2))
A__TIMES(s(X), Y) → A__PLUS(mark(Y), a__times(mark(X), mark(Y)))
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
MARK(s(X)) → MARK(X)
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.
(46) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MARK(rcons(X1, X2)) → MARK(X1)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(A__PLUS(x1, x2)) = | 3A | + | -I | · | x1 | + | 0A | · | x2 |
POL(MARK(x1)) = | 3A | + | 0A | · | x1 |
POL(plus(x1, x2)) = | -I | + | -I | · | x1 | + | 0A | · | x2 |
POL(mark(x1)) = | -I | + | 0A | · | x1 |
POL(times(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(A__TIMES(x1, x2)) = | 3A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(a__times(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(rcons(x1, x2)) = | 5A | + | 1A | · | x1 | + | 0A | · | x2 |
POL(cons(x1, x2)) = | 0A | + | 0A | · | x1 | + | -I | · | x2 |
POL(negrecip(x1)) = | 0A | + | -I | · | x1 |
POL(posrecip(x1)) = | 0A | + | -I | · | x1 |
POL(a__from(x1)) = | 0A | + | 0A | · | x1 |
POL(from(x1)) = | 0A | + | 0A | · | x1 |
POL(cons2(x1, x2)) = | 5A | + | -I | · | x1 | + | -I | · | x2 |
POL(a__plus(x1, x2)) = | -I | + | -I | · | x1 | + | 0A | · | x2 |
POL(a__pi(x1)) = | 5A | + | 0A | · | x1 |
POL(a__2ndsneg(x1, x2)) = | 5A | + | 0A | · | x1 | + | -I | · | x2 |
POL(2ndsneg(x1, x2)) = | 5A | + | 0A | · | x1 | + | -I | · | x2 |
POL(a__2ndspos(x1, x2)) = | 5A | + | 0A | · | x1 | + | -I | · | x2 |
POL(2ndspos(x1, x2)) = | 5A | + | 0A | · | x1 | + | -I | · | x2 |
POL(a__square(x1)) = | -I | + | 0A | · | x1 |
POL(square(x1)) = | -I | + | 0A | · | x1 |
The following usable rules [FROCOS05] were oriented:
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
mark(negrecip(X)) → negrecip(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
a__from(X) → from(X)
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
mark(rnil) → rnil
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
a__plus(X1, X2) → plus(X1, X2)
a__pi(X) → pi(X)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__square(X) → square(X)
a__times(X1, X2) → times(X1, X2)
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndspos(0, Z) → rnil
a__from(X) → cons(mark(X), from(s(X)))
a__times(0, Y) → 0
mark(from(X)) → a__from(mark(X))
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(s(X), Y) → s(a__plus(mark(X), mark(Y)))
mark(0) → 0
mark(s(X)) → s(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))
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__plus(0, Y) → mark(Y)
mark(square(X)) → a__square(mark(X))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
a__square(X) → a__times(mark(X), mark(X))
(47) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__PLUS(0, Y) → MARK(Y)
MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
A__PLUS(s(X), Y) → MARK(Y)
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → A__TIMES(mark(X1), mark(X2))
A__TIMES(s(X), Y) → A__PLUS(mark(Y), a__times(mark(X), mark(Y)))
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
MARK(s(X)) → MARK(X)
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.
(48) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → A__TIMES(mark(X1), mark(X2))
A__TIMES(s(X), Y) → A__PLUS(mark(Y), a__times(mark(X), mark(Y)))
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
MARK(s(X)) → MARK(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
A__PLUS(
x1,
x2) =
A__PLUS(
x2)
0 =
0
MARK(
x1) =
MARK(
x1)
plus(
x1,
x2) =
plus(
x1,
x2)
mark(
x1) =
x1
s(
x1) =
s(
x1)
times(
x1,
x2) =
times(
x1,
x2)
A__TIMES(
x1,
x2) =
A__TIMES(
x1,
x2)
a__times(
x1,
x2) =
a__times(
x1,
x2)
rcons(
x1,
x2) =
x2
cons(
x1,
x2) =
x1
nil =
nil
negrecip(
x1) =
negrecip
posrecip(
x1) =
posrecip(
x1)
a__from(
x1) =
x1
from(
x1) =
x1
rnil =
rnil
cons2(
x1,
x2) =
x1
a__plus(
x1,
x2) =
a__plus(
x1,
x2)
a__pi(
x1) =
a__pi
pi(
x1) =
pi
a__2ndsneg(
x1,
x2) =
a__2ndsneg
2ndsneg(
x1,
x2) =
2ndsneg
a__2ndspos(
x1,
x2) =
a__2ndspos
2ndspos(
x1,
x2) =
2ndspos
a__square(
x1) =
a__square(
x1)
square(
x1) =
square(
x1)
Recursive path order with status [RPO].
Quasi-Precedence:
[posrecip1, api, pi, a2ndsneg, 2ndsneg, a2ndspos, 2ndspos] > 0
[posrecip1, api, pi, a2ndsneg, 2ndsneg, a2ndspos, 2ndspos] > s1
[posrecip1, api, pi, a2ndsneg, 2ndsneg, a2ndspos, 2ndspos] > negrecip
[posrecip1, api, pi, a2ndsneg, 2ndsneg, a2ndspos, 2ndspos] > rnil
[asquare1, square1] > [times2, ATIMES2, atimes2] > [APLUS1, MARK1, plus2, aplus2] > s1
[asquare1, square1] > [times2, ATIMES2, atimes2] > 0
Status:
api: []
plus2: multiset
rnil: multiset
ATIMES2: multiset
posrecip1: multiset
square1: multiset
2ndsneg: []
0: multiset
2ndspos: []
negrecip: []
aplus2: multiset
MARK1: multiset
APLUS1: multiset
a2ndspos: []
times2: multiset
pi: []
s1: multiset
atimes2: multiset
nil: multiset
a2ndsneg: []
asquare1: multiset
The following usable rules [FROCOS05] were oriented:
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
mark(negrecip(X)) → negrecip(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
a__from(X) → from(X)
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
mark(rnil) → rnil
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
a__plus(X1, X2) → plus(X1, X2)
a__pi(X) → pi(X)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__square(X) → square(X)
a__times(X1, X2) → times(X1, X2)
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndspos(0, Z) → rnil
a__from(X) → cons(mark(X), from(s(X)))
a__times(0, Y) → 0
mark(from(X)) → a__from(mark(X))
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(s(X), Y) → s(a__plus(mark(X), mark(Y)))
mark(0) → 0
mark(s(X)) → s(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))
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__plus(0, Y) → mark(Y)
mark(square(X)) → a__square(mark(X))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
a__square(X) → a__times(mark(X), mark(X))
(49) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__PLUS(0, Y) → MARK(Y)
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
A__PLUS(s(X), Y) → MARK(Y)
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.
(50) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 2 less nodes.
(51) Complex Obligation (AND)
(52) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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.
(53) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(54) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MARK(rcons(X1, X2)) → MARK(X2)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(55) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- MARK(rcons(X1, X2)) → MARK(X2)
The graph contains the following edges 1 > 1
(56) TRUE
(57) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
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.
(58) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
A__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
A__PLUS(
x1,
x2) =
A__PLUS(
x1)
s(
x1) =
s(
x1)
mark(
x1) =
x1
cons(
x1,
x2) =
x2
nil =
nil
negrecip(
x1) =
x1
posrecip(
x1) =
x1
a__from(
x1) =
a__from
from(
x1) =
from
rcons(
x1,
x2) =
rcons
rnil =
rnil
cons2(
x1,
x2) =
cons2
a__plus(
x1,
x2) =
a__plus(
x1,
x2)
plus(
x1,
x2) =
plus(
x1,
x2)
a__pi(
x1) =
a__pi(
x1)
pi(
x1) =
pi(
x1)
a__2ndsneg(
x1,
x2) =
a__2ndsneg(
x1)
2ndsneg(
x1,
x2) =
2ndsneg(
x1)
a__2ndspos(
x1,
x2) =
a__2ndspos(
x1,
x2)
2ndspos(
x1,
x2) =
2ndspos(
x1,
x2)
a__square(
x1) =
a__square(
x1)
square(
x1) =
square(
x1)
a__times(
x1,
x2) =
a__times(
x1,
x2)
times(
x1,
x2) =
times(
x1,
x2)
0 =
0
Recursive path order with status [RPO].
Quasi-Precedence:
nil > cons2
[api1, pi1] > [afrom, from] > cons2
[api1, pi1] > [rcons, a2ndspos2, 2ndspos2] > [APLUS1, s1] > cons2
[a2ndsneg1, 2ndsneg1] > [rcons, a2ndspos2, 2ndspos2] > [APLUS1, s1] > cons2
[a2ndsneg1, 2ndsneg1] > rnil > cons2
[asquare1, square1] > [atimes2, times2] > [aplus2, plus2] > [APLUS1, s1] > cons2
0 > rnil > cons2
Status:
plus2: multiset
rnil: multiset
cons2: []
pi1: multiset
square1: multiset
0: multiset
a2ndsneg1: multiset
from: []
aplus2: multiset
api1: multiset
a2ndspos2: multiset
APLUS1: multiset
2ndspos2: multiset
rcons: multiset
times2: multiset
afrom: []
s1: multiset
atimes2: multiset
2ndsneg1: multiset
nil: multiset
asquare1: multiset
The following usable rules [FROCOS05] were oriented:
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
mark(negrecip(X)) → negrecip(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
a__from(X) → from(X)
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
mark(rnil) → rnil
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
a__plus(X1, X2) → plus(X1, X2)
a__pi(X) → pi(X)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__square(X) → square(X)
a__times(X1, X2) → times(X1, X2)
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndspos(0, Z) → rnil
a__from(X) → cons(mark(X), from(s(X)))
a__times(0, Y) → 0
mark(from(X)) → a__from(mark(X))
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(s(X), Y) → s(a__plus(mark(X), mark(Y)))
mark(0) → 0
mark(s(X)) → s(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))
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__plus(0, Y) → mark(Y)
mark(square(X)) → a__square(mark(X))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
a__square(X) → a__times(mark(X), mark(X))
(59) Obligation:
Q DP problem:
P is empty.
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.
(60) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(61) TRUE
(62) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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))) → A__2NDSPOS(mark(N), mark(Z))
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))) → A__2NDSNEG(mark(N), mark(Z))
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.
(63) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
A__2NDSNEG(s(N), cons2(X, cons(Y, Z))) → A__2NDSPOS(mark(N), mark(Z))
A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → A__2NDSNEG(mark(N), mark(Z))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
A__2NDSNEG(
x1,
x2) =
A__2NDSNEG(
x1)
s(
x1) =
s(
x1)
cons(
x1,
x2) =
cons(
x1)
mark(
x1) =
x1
cons2(
x1,
x2) =
cons2
A__2NDSPOS(
x1,
x2) =
A__2NDSPOS(
x1)
nil =
nil
negrecip(
x1) =
negrecip
posrecip(
x1) =
posrecip
a__from(
x1) =
a__from(
x1)
from(
x1) =
from(
x1)
rcons(
x1,
x2) =
x1
rnil =
rnil
a__plus(
x1,
x2) =
a__plus(
x1,
x2)
plus(
x1,
x2) =
plus(
x1,
x2)
a__pi(
x1) =
a__pi(
x1)
pi(
x1) =
pi(
x1)
a__2ndsneg(
x1,
x2) =
a__2ndsneg(
x1,
x2)
2ndsneg(
x1,
x2) =
2ndsneg(
x1,
x2)
a__2ndspos(
x1,
x2) =
x2
2ndspos(
x1,
x2) =
x2
a__square(
x1) =
a__square(
x1)
square(
x1) =
square(
x1)
a__times(
x1,
x2) =
a__times(
x1,
x2)
times(
x1,
x2) =
times(
x1,
x2)
0 =
0
Recursive path order with status [RPO].
Quasi-Precedence:
[A2NDSNEG1, A2NDSPOS1] > [cons2, posrecip] > [s1, rnil, 0]
[cons1, afrom1, from1, api1, pi1] > [cons2, posrecip] > [s1, rnil, 0]
nil > [s1, rnil, 0]
[a2ndsneg2, 2ndsneg2] > [cons2, posrecip] > [s1, rnil, 0]
[a2ndsneg2, 2ndsneg2] > negrecip > [s1, rnil, 0]
[asquare1, square1] > [atimes2, times2] > [aplus2, plus2] > [s1, rnil, 0]
Status:
from1: [1]
plus2: multiset
cons1: [1]
rnil: multiset
cons2: []
afrom1: [1]
pi1: [1]
square1: multiset
0: multiset
2ndsneg2: multiset
negrecip: multiset
aplus2: multiset
api1: [1]
A2NDSPOS1: multiset
times2: multiset
s1: multiset
atimes2: multiset
posrecip: []
a2ndsneg2: multiset
A2NDSNEG1: multiset
nil: multiset
asquare1: multiset
The following usable rules [FROCOS05] were oriented:
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(nil) → nil
mark(negrecip(X)) → negrecip(mark(X))
mark(posrecip(X)) → posrecip(mark(X))
a__from(X) → from(X)
mark(rcons(X1, X2)) → rcons(mark(X1), mark(X2))
mark(rnil) → rnil
mark(cons2(X1, X2)) → cons2(X1, mark(X2))
a__plus(X1, X2) → plus(X1, X2)
a__pi(X) → pi(X)
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__square(X) → square(X)
a__times(X1, X2) → times(X1, X2)
a__2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
a__2ndspos(s(N), cons(X, Z)) → a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(s(N), cons(X, Z)) → a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
a__2ndsneg(0, Z) → rnil
a__2ndspos(0, Z) → rnil
a__from(X) → cons(mark(X), from(s(X)))
a__times(0, Y) → 0
mark(from(X)) → a__from(mark(X))
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(s(X), Y) → s(a__plus(mark(X), mark(Y)))
mark(0) → 0
mark(s(X)) → s(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))
a__times(s(X), Y) → a__plus(mark(Y), a__times(mark(X), mark(Y)))
a__plus(0, Y) → mark(Y)
mark(square(X)) → a__square(mark(X))
mark(times(X1, X2)) → a__times(mark(X1), mark(X2))
a__square(X) → a__times(mark(X), mark(X))
(64) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__2NDSNEG(s(N), cons(X, Z)) → A__2NDSNEG(s(mark(N)), cons2(X, mark(Z)))
A__2NDSPOS(s(N), cons(X, Z)) → A__2NDSPOS(s(mark(N)), cons2(X, mark(Z)))
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.
(65) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
(66) TRUE