YES Termination w.r.t. Q proof of Transformed_CSR_04_ExAppendixB_AEL03_GM.ari

Termination w.r.t. Q of the given QTRS could be proven:

0 QTRS
↳1 DependencyPairsProof (⇔, 0 ms)
↳2 QDP
↳3 QDPOrderProof (⇔, 192 ms)
↳4 QDP
↳5 QDPOrderProof (⇔, 175 ms)
↳6 QDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 QDP
↳9 QDPOrderProof (⇔, 130 ms)
↳10 QDP
↳11 DependencyGraphProof (⇔, 0 ms)
↳12 AND
    ↳13 QDP
        ↳14 QDPOrderProof (⇔, 291 ms)
        ↳15 QDP
        ↳16 DependencyGraphProof (⇔, 0 ms)
        ↳17 TRUE
    ↳18 QDP
        ↳19 QDPOrderProof (⇔, 158 ms)
        ↳20 QDP
        ↳21 QDPOrderProof (⇔, 190 ms)
        ↳22 QDP
        ↳23 QDPOrderProof (⇔, 150 ms)
        ↳24 QDP
        ↳25 DependencyGraphProof (⇔, 0 ms)
        ↳26 QDP
        ↳27 QDPOrderProof (⇔, 21 ms)
        ↳28 QDP
        ↳29 QDPOrderProof (⇔, 0 ms)
        ↳30 QDP
        ↳31 QDPOrderProof (⇔, 0 ms)
        ↳32 QDP
        ↳33 QDPOrderProof (⇔, 0 ms)
        ↳34 QDP
        ↳35 QDPOrderProof (⇔, 0 ms)
        ↳36 QDP
        ↳37 QDPOrderProof (⇔, 0 ms)
        ↳38 QDP
        ↳39 QDPOrderProof (⇔, 0 ms)
        ↳40 QDP
        ↳41 QDPOrderProof (⇔, 0 ms)
        ↳42 QDP
        ↳43 DependencyGraphProof (⇔, 0 ms)
        ↳44 TRUE

(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,JAR06].


The following pairs can be oriented strictly and are deleted.


A__PI(X) → MARK(X)
A__PI(X) → A__FROM(0)
A__TIMES(s(X), Y) → MARK(Y)
A__SQUARE(X) → MARK(X)
MARK(pi(X)) → MARK(X)
MARK(times(X1, X2)) → MARK(X2)
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__FROM(x1)) = 4A + 0A·x1

POL(MARK(x1)) = 4A + 0A·x1

POL(A__2NDSPOS(x1, x2)) = 4A + 0A·x1 + 1A·x2

POL(s(x1)) = 0A + 0A·x1

POL(cons(x1, x2)) = 1A + 0A·x1 + 0A·x2

POL(mark(x1)) = -I + 0A·x1

POL(cons2(x1, x2)) = 1A + -I·x1 + 0A·x2

POL(A__2NDSNEG(x1, x2)) = 4A + 0A·x1 + 1A·x2

POL(A__PI(x1)) = 5A + 3A·x1

POL(a__from(x1)) = 4A + 4A·x1

POL(0) = 0A

POL(A__PLUS(x1, x2)) = 4A + 0A·x1 + 0A·x2

POL(A__TIMES(x1, x2)) = 5A + 0A·x1 + 1A·x2

POL(a__times(x1, x2)) = 5A + 0A·x1 + 1A·x2

POL(A__SQUARE(x1)) = 5A + 2A·x1

POL(from(x1)) = 4A + 4A·x1

POL(2ndspos(x1, x2)) = 3A + 5A·x1 + 1A·x2

POL(2ndsneg(x1, x2)) = 4A + 5A·x1 + 1A·x2

POL(pi(x1)) = 5A + 5A·x1

POL(plus(x1, x2)) = 4A + 0A·x1 + 0A·x2

POL(times(x1, x2)) = 5A + 0A·x1 + 1A·x2

POL(square(x1)) = 5A + 3A·x1

POL(posrecip(x1)) = 5A + 0A·x1

POL(negrecip(x1)) = 5A + 0A·x1

POL(rcons(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(a__2ndspos(x1, x2)) = 3A + 5A·x1 + 1A·x2

POL(a__2ndsneg(x1, x2)) = 4A + 5A·x1 + 1A·x2

POL(a__pi(x1)) = 5A + 5A·x1

POL(a__plus(x1, x2)) = 4A + 0A·x1 + 0A·x2

POL(a__square(x1)) = 5A + 3A·x1

POL(nil) = 0A

POL(rnil) = 3A

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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))
a__plus(0, Y) → mark(Y)
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)))
mark(square(X)) → a__square(mark(X))
a__square(X) → a__times(mark(X), 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) → cons(mark(X), from(s(X)))
a__from(X) → from(X)
a__times(0, Y) → 0
a__times(X1, X2) → times(X1, X2)
a__2ndspos(0, Z) → rnil
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__2ndsneg(0, Z) → rnil
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__pi(X) → pi(X)
a__plus(X1, X2) → plus(X1, X2)
a__square(X) → square(X)
a__plus(s(X), Y) → s(a__plus(mark(X), mark(Y)))
a__pi(X) → a__2ndspos(mark(X), a__from(0))
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(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)))

(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__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) → A__TIMES(mark(X), mark(Y))
A__TIMES(s(X), Y) → MARK(X)
A__SQUARE(X) → A__TIMES(mark(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(square(X)) → A__SQUARE(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,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(pi(X)) → A__PI(mark(X))
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__FROM(x1)) = 4A + 0A·x1

POL(MARK(x1)) = 1A + 0A·x1

POL(A__2NDSPOS(x1, x2)) = 1A + 0A·x1 + 0A·x2

POL(s(x1)) = 1A + 0A·x1

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(A__PI(x1)) = 4A + 0A·x1

POL(a__from(x1)) = 4A + 0A·x1

POL(0) = 1A

POL(A__PLUS(x1, x2)) = 0A + 0A·x1 + 0A·x2

POL(A__TIMES(x1, x2)) = 4A + 0A·x1 + 3A·x2

POL(a__times(x1, x2)) = 4A + 0A·x1 + 3A·x2

POL(A__SQUARE(x1)) = 4A + 5A·x1

POL(from(x1)) = 4A + 0A·x1

POL(2ndspos(x1, x2)) = 1A + 1A·x1 + 1A·x2

POL(2ndsneg(x1, x2)) = 1A + 1A·x1 + 1A·x2

POL(pi(x1)) = 5A + 2A·x1

POL(plus(x1, x2)) = 4A + 1A·x1 + 0A·x2

POL(times(x1, x2)) = 4A + 0A·x1 + 3A·x2

POL(square(x1)) = 5A + 5A·x1

POL(posrecip(x1)) = -I + 0A·x1

POL(negrecip(x1)) = -I + 0A·x1

POL(rcons(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(a__2ndspos(x1, x2)) = 1A + 1A·x1 + 1A·x2

POL(a__2ndsneg(x1, x2)) = 1A + 1A·x1 + 1A·x2

POL(a__pi(x1)) = 5A + 2A·x1

POL(a__plus(x1, x2)) = 4A + 1A·x1 + 0A·x2

POL(a__square(x1)) = 5A + 5A·x1

POL(nil) = 3A

POL(rnil) = 0A

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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))
a__plus(0, Y) → mark(Y)
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)))
mark(square(X)) → a__square(mark(X))
a__square(X) → a__times(mark(X), 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) → cons(mark(X), from(s(X)))
a__from(X) → from(X)
a__times(0, Y) → 0
a__times(X1, X2) → times(X1, X2)
a__2ndspos(0, Z) → rnil
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__2ndsneg(0, Z) → rnil
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__pi(X) → pi(X)
a__plus(X1, X2) → plus(X1, X2)
a__square(X) → square(X)
a__plus(s(X), Y) → s(a__plus(mark(X), mark(Y)))
a__pi(X) → a__2ndspos(mark(X), a__from(0))
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(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)))

(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__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) → A__TIMES(mark(X), mark(Y))
A__TIMES(s(X), Y) → MARK(X)
A__SQUARE(X) → A__TIMES(mark(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(X2)
MARK(times(X1, X2)) → A__TIMES(mark(X1), mark(X2))
MARK(times(X1, X2)) → MARK(X1)
MARK(square(X)) → A__SQUARE(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) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(8) 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(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(square(X)) → A__SQUARE(mark(X))
A__SQUARE(X) → A__TIMES(mark(X), mark(X))
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
A__TIMES(s(X), Y) → 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__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.

(9) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


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(2ndsneg(X1, X2)) → MARK(X1)
MARK(2ndsneg(X1, X2)) → MARK(X2)
A__2NDSPOS(s(N), cons(X, Z)) → MARK(N)
A__2NDSPOS(s(N), cons(X, Z)) → 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 remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(MARK(x1)) = 3A + 0A·x1

POL(from(x1)) = 4A + 1A·x1

POL(A__FROM(x1)) = 3A + 0A·x1

POL(mark(x1)) = -I + 0A·x1

POL(2ndspos(x1, x2)) = 3A + 3A·x1 + 1A·x2

POL(A__2NDSPOS(x1, x2)) = 3A + 1A·x1 + 1A·x2

POL(s(x1)) = -I + 0A·x1

POL(cons(x1, x2)) = 4A + 0A·x1 + 0A·x2

POL(cons2(x1, x2)) = 4A + -I·x1 + 0A·x2

POL(2ndsneg(x1, x2)) = 5A + 3A·x1 + 1A·x2

POL(A__2NDSNEG(x1, x2)) = 1A + 1A·x1 + 1A·x2

POL(plus(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(A__PLUS(x1, x2)) = 3A + 0A·x1 + 0A·x2

POL(0) = 1A

POL(times(x1, x2)) = -I + 1A·x1 + 0A·x2

POL(A__TIMES(x1, x2)) = 3A + 1A·x1 + 0A·x2

POL(a__times(x1, x2)) = -I + 1A·x1 + 0A·x2

POL(square(x1)) = 3A + 3A·x1

POL(A__SQUARE(x1)) = 3A + 2A·x1

POL(posrecip(x1)) = -I + 0A·x1

POL(negrecip(x1)) = -I + 0A·x1

POL(rcons(x1, x2)) = -I + 1A·x1 + 0A·x2

POL(a__from(x1)) = 4A + 1A·x1

POL(a__2ndspos(x1, x2)) = 3A + 3A·x1 + 1A·x2

POL(a__2ndsneg(x1, x2)) = 5A + 3A·x1 + 1A·x2

POL(pi(x1)) = 5A + 5A·x1

POL(a__pi(x1)) = 5A + 5A·x1

POL(a__plus(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(a__square(x1)) = 3A + 3A·x1

POL(nil) = 3A

POL(rnil) = 1A

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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))
a__plus(0, Y) → mark(Y)
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)))
mark(square(X)) → a__square(mark(X))
a__square(X) → a__times(mark(X), 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__times(0, Y) → 0
a__times(X1, X2) → times(X1, X2)
a__from(X) → from(X)
a__2ndspos(0, Z) → rnil
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__2ndsneg(0, Z) → rnil
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__pi(X) → pi(X)
a__plus(X1, X2) → plus(X1, X2)
a__square(X) → square(X)
a__plus(s(X), Y) → s(a__plus(mark(X), mark(Y)))
a__pi(X) → a__2ndspos(mark(X), a__from(0))
a__from(X) → cons(mark(X), from(s(X)))
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(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)))

(10) 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(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(square(X)) → A__SQUARE(mark(X))
A__SQUARE(X) → A__TIMES(mark(X), mark(X))
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
A__TIMES(s(X), Y) → 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__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), 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.

(11) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 3 less nodes.

(12) Complex Obligation (AND)

(13) 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)))

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.

(14) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


A__2NDSPOS(s(N), cons2(X, cons(Y, Z))) → A__2NDSNEG(mark(N), mark(Z))
A__2NDSNEG(s(N), cons2(X, cons(Y, Z))) → A__2NDSPOS(mark(N), mark(Z))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
A__2NDSPOS(x1, x2)  =  A__2NDSPOS(x1)
s(x1)  =  s(x1)
cons2(x1, x2)  =  cons2
cons(x1, x2)  =  cons
A__2NDSNEG(x1, x2)  =  A__2NDSNEG(x1)
mark(x1)  =  x1
from(x1)  =  from(x1)
a__from(x1)  =  a__from(x1)
2ndspos(x1, x2)  =  x1
a__2ndspos(x1, x2)  =  x1
2ndsneg(x1, x2)  =  2ndsneg
a__2ndsneg(x1, x2)  =  a__2ndsneg
pi(x1)  =  x1
a__pi(x1)  =  x1
plus(x1, x2)  =  plus(x1, x2)
a__plus(x1, x2)  =  a__plus(x1, x2)
0  =  0
times(x1, x2)  =  times(x1, x2)
a__times(x1, x2)  =  a__times(x1, x2)
square(x1)  =  square(x1)
a__square(x1)  =  a__square(x1)
posrecip(x1)  =  posrecip
negrecip(x1)  =  negrecip
nil  =  nil
rnil  =  rnil
rcons(x1, x2)  =  x1

Recursive path order with status [RPO].
Quasi-Precedence:
[cons2, 2ndsneg, a2ndsneg] > [A2NDSPOS1, cons, A2NDSNEG1] > [s1, posrecip, negrecip]
[cons2, 2ndsneg, a2ndsneg] > rnil > [s1, posrecip, negrecip]
[from1, afrom1] > [A2NDSPOS1, cons, A2NDSNEG1] > [s1, posrecip, negrecip]
0 > rnil > [s1, posrecip, negrecip]
[square1, asquare1] > [times2, atimes2] > [plus2, aplus2] > [s1, posrecip, negrecip]
nil > [s1, posrecip, negrecip]

Status:
A2NDSPOS1: [1]
s1: [1]
cons2: multiset
cons: multiset
A2NDSNEG1: [1]
from1: multiset
afrom1: multiset
2ndsneg: []
a2ndsneg: []
plus2: [1,2]
aplus2: [1,2]
0: multiset
times2: [1,2]
atimes2: [1,2]
square1: multiset
asquare1: multiset
posrecip: multiset
negrecip: []
nil: multiset
rnil: multiset


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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))
a__plus(0, Y) → mark(Y)
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)))
mark(square(X)) → a__square(mark(X))
a__square(X) → a__times(mark(X), 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(0, Z) → rnil
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__2ndsneg(0, Z) → rnil
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__pi(X) → pi(X)
a__plus(X1, X2) → plus(X1, X2)
a__times(0, Y) → 0
a__times(X1, X2) → times(X1, X2)
a__square(X) → square(X)
a__plus(s(X), Y) → s(a__plus(mark(X), mark(Y)))
a__pi(X) → a__2ndspos(mark(X), a__from(0))
a__from(X) → cons(mark(X), from(s(X)))
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(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)))

(15) 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.

(16) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(17) TRUE

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MARK(2ndspos(X1, X2)) → MARK(X2)
MARK(2ndspos(X1, X2)) → MARK(X1)
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(square(X)) → A__SQUARE(mark(X))
A__SQUARE(X) → A__TIMES(mark(X), mark(X))
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
A__TIMES(s(X), Y) → 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__PLUS(s(X), Y) → 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.

(19) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


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(MARK(x1)) = 3A + 4A·x1

POL(2ndspos(x1, x2)) = -I + 5A·x1 + 5A·x2

POL(plus(x1, x2)) = -I + 1A·x1 + 0A·x2

POL(A__PLUS(x1, x2)) = 2A + 4A·x1 + 4A·x2

POL(mark(x1)) = -I + 0A·x1

POL(0) = 0A

POL(times(x1, x2)) = -I + 1A·x1 + 1A·x2

POL(A__TIMES(x1, x2)) = 3A + 5A·x1 + 5A·x2

POL(s(x1)) = 0A + 0A·x1

POL(a__times(x1, x2)) = -I + 1A·x1 + 1A·x2

POL(square(x1)) = -I + 1A·x1

POL(A__SQUARE(x1)) = 3A + 5A·x1

POL(posrecip(x1)) = -I + 5A·x1

POL(negrecip(x1)) = -I + 0A·x1

POL(cons(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(cons2(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(rcons(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(from(x1)) = 0A + 0A·x1

POL(a__from(x1)) = 0A + 0A·x1

POL(a__2ndspos(x1, x2)) = -I + 5A·x1 + 5A·x2

POL(2ndsneg(x1, x2)) = 0A + 5A·x1 + 5A·x2

POL(a__2ndsneg(x1, x2)) = 0A + 5A·x1 + 5A·x2

POL(pi(x1)) = 5A + 5A·x1

POL(a__pi(x1)) = 5A + 5A·x1

POL(a__plus(x1, x2)) = -I + 1A·x1 + 0A·x2

POL(a__square(x1)) = -I + 1A·x1

POL(nil) = 1A

POL(rnil) = 4A

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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))
a__plus(0, Y) → mark(Y)
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)))
mark(square(X)) → a__square(mark(X))
a__square(X) → a__times(mark(X), 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__times(0, Y) → 0
a__times(X1, X2) → times(X1, X2)
a__from(X) → from(X)
a__2ndspos(0, Z) → rnil
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__2ndsneg(0, Z) → rnil
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__pi(X) → pi(X)
a__plus(X1, X2) → plus(X1, X2)
a__square(X) → square(X)
a__plus(s(X), Y) → s(a__plus(mark(X), mark(Y)))
a__pi(X) → a__2ndspos(mark(X), a__from(0))
a__from(X) → cons(mark(X), from(s(X)))
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(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)))

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MARK(2ndspos(X1, X2)) → MARK(X2)
MARK(2ndspos(X1, X2)) → MARK(X1)
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(square(X)) → A__SQUARE(mark(X))
A__SQUARE(X) → A__TIMES(mark(X), mark(X))
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
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__PLUS(s(X), Y) → 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.

(21) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(2ndspos(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)) = 5A + 5A·x1

POL(2ndspos(x1, x2)) = 4A + 4A·x1 + 0A·x2

POL(plus(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(A__PLUS(x1, x2)) = 5A + 5A·x1 + 5A·x2

POL(mark(x1)) = 0A + 0A·x1

POL(0) = 4A

POL(times(x1, x2)) = 0A + 0A·x1 + 0A·x2

POL(A__TIMES(x1, x2)) = 5A + 5A·x1 + 5A·x2

POL(s(x1)) = 1A + 0A·x1

POL(a__times(x1, x2)) = 0A + 0A·x1 + 0A·x2

POL(square(x1)) = 1A + 0A·x1

POL(A__SQUARE(x1)) = 5A + 5A·x1

POL(posrecip(x1)) = -I + 0A·x1

POL(negrecip(x1)) = -I + 0A·x1

POL(cons(x1, x2)) = 2A + 0A·x1 + 0A·x2

POL(cons2(x1, x2)) = 5A + 0A·x1 + 0A·x2

POL(rcons(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(from(x1)) = 2A + 1A·x1

POL(a__from(x1)) = 2A + 1A·x1

POL(a__2ndspos(x1, x2)) = 4A + 4A·x1 + 0A·x2

POL(2ndsneg(x1, x2)) = 5A + 4A·x1 + 0A·x2

POL(a__2ndsneg(x1, x2)) = 5A + 4A·x1 + 0A·x2

POL(pi(x1)) = 5A + 5A·x1

POL(a__pi(x1)) = 5A + 5A·x1

POL(a__plus(x1, x2)) = 0A + 0A·x1 + 0A·x2

POL(a__square(x1)) = 1A + 0A·x1

POL(nil) = 2A

POL(rnil) = 1A

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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))
a__plus(0, Y) → mark(Y)
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)))
mark(square(X)) → a__square(mark(X))
a__square(X) → a__times(mark(X), 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__times(0, Y) → 0
a__times(X1, X2) → times(X1, X2)
a__from(X) → from(X)
a__2ndspos(0, Z) → rnil
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__2ndsneg(0, Z) → rnil
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__pi(X) → pi(X)
a__plus(X1, X2) → plus(X1, X2)
a__square(X) → square(X)
a__plus(s(X), Y) → s(a__plus(mark(X), mark(Y)))
a__pi(X) → a__2ndspos(mark(X), a__from(0))
a__from(X) → cons(mark(X), from(s(X)))
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(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)))

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MARK(2ndspos(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(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(square(X)) → A__SQUARE(mark(X))
A__SQUARE(X) → A__TIMES(mark(X), mark(X))
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
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__PLUS(s(X), Y) → 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.

(23) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


A__SQUARE(X) → A__TIMES(mark(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 + 1A·x1

POL(2ndspos(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(plus(x1, x2)) = -I + 1A·x1 + 0A·x2

POL(A__PLUS(x1, x2)) = 0A + 1A·x1 + 1A·x2

POL(mark(x1)) = -I + 0A·x1

POL(0) = 0A

POL(times(x1, x2)) = -I + 0A·x1 + 3A·x2

POL(A__TIMES(x1, x2)) = 0A + 1A·x1 + 4A·x2

POL(s(x1)) = -I + 0A·x1

POL(a__times(x1, x2)) = -I + 0A·x1 + 3A·x2

POL(square(x1)) = 3A + 4A·x1

POL(A__SQUARE(x1)) = 4A + 5A·x1

POL(posrecip(x1)) = -I + 0A·x1

POL(negrecip(x1)) = -I + 0A·x1

POL(cons(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(cons2(x1, x2)) = -I + -I·x1 + 0A·x2

POL(rcons(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(from(x1)) = 3A + 5A·x1

POL(a__from(x1)) = 3A + 5A·x1

POL(a__2ndspos(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(2ndsneg(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(a__2ndsneg(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(pi(x1)) = 5A + 3A·x1

POL(a__pi(x1)) = 5A + 3A·x1

POL(a__plus(x1, x2)) = -I + 1A·x1 + 0A·x2

POL(a__square(x1)) = 3A + 4A·x1

POL(nil) = 1A

POL(rnil) = 0A

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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))
a__plus(0, Y) → mark(Y)
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)))
mark(square(X)) → a__square(mark(X))
a__square(X) → a__times(mark(X), 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__times(0, Y) → 0
a__times(X1, X2) → times(X1, X2)
a__from(X) → from(X)
a__2ndspos(0, Z) → rnil
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__2ndsneg(0, Z) → rnil
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__pi(X) → pi(X)
a__plus(X1, X2) → plus(X1, X2)
a__square(X) → square(X)
a__plus(s(X), Y) → s(a__plus(mark(X), mark(Y)))
a__pi(X) → a__2ndspos(mark(X), a__from(0))
a__from(X) → cons(mark(X), from(s(X)))
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(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)))

(24) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MARK(2ndspos(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(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(square(X)) → A__SQUARE(mark(X))
A__TIMES(s(X), Y) → A__TIMES(mark(X), mark(Y))
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__PLUS(s(X), Y) → 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.

(25) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(26) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(0, Y) → MARK(Y)
MARK(2ndspos(X1, X2)) → 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__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(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__PLUS(s(X), Y) → MARK(Y)
A__TIMES(s(X), Y) → A__TIMES(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.

(27) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


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(MARK(x1)) = 5A + 3A·x1

POL(plus(x1, x2)) = 5A + 1A·x1 + 0A·x2

POL(A__PLUS(x1, x2)) = 5A + 4A·x1 + 3A·x2

POL(mark(x1)) = 4A + 0A·x1

POL(0) = 0A

POL(2ndspos(x1, x2)) = -I + -I·x1 + 0A·x2

POL(times(x1, x2)) = 5A + 0A·x1 + 1A·x2

POL(A__TIMES(x1, x2)) = 5A + 3A·x1 + 4A·x2

POL(s(x1)) = 5A + 0A·x1

POL(a__times(x1, x2)) = 5A + 0A·x1 + 1A·x2

POL(posrecip(x1)) = -I + 0A·x1

POL(negrecip(x1)) = -I + 0A·x1

POL(cons(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(cons2(x1, x2)) = -I + -I·x1 + 0A·x2

POL(rcons(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(from(x1)) = 5A + 0A·x1

POL(a__from(x1)) = 5A + 0A·x1

POL(a__2ndspos(x1, x2)) = 4A + -I·x1 + 0A·x2

POL(2ndsneg(x1, x2)) = 4A + -I·x1 + 0A·x2

POL(a__2ndsneg(x1, x2)) = 4A + -I·x1 + 0A·x2

POL(pi(x1)) = 5A + -I·x1

POL(a__pi(x1)) = 5A + -I·x1

POL(a__plus(x1, x2)) = 5A + 1A·x1 + 0A·x2

POL(square(x1)) = 5A + 1A·x1

POL(a__square(x1)) = 5A + 1A·x1

POL(nil) = 3A

POL(rnil) = 1A

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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))
a__plus(0, Y) → mark(Y)
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)))
mark(square(X)) → a__square(mark(X))
a__square(X) → a__times(mark(X), 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__times(0, Y) → 0
a__times(X1, X2) → times(X1, X2)
a__from(X) → from(X)
a__2ndspos(0, Z) → rnil
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__2ndsneg(0, Z) → rnil
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__pi(X) → pi(X)
a__plus(X1, X2) → plus(X1, X2)
a__square(X) → square(X)
a__plus(s(X), Y) → s(a__plus(mark(X), mark(Y)))
a__pi(X) → a__2ndspos(mark(X), a__from(0))
a__from(X) → cons(mark(X), from(s(X)))
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(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)))

(28) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(0, Y) → MARK(Y)
MARK(2ndspos(X1, X2)) → 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__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
MARK(times(X1, X2)) → MARK(X1)
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__PLUS(s(X), Y) → MARK(Y)
A__TIMES(s(X), Y) → A__TIMES(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.

(29) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


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(plus(x1, x2)) = 5A + 0A·x1 + 0A·x2

POL(A__PLUS(x1, x2)) = 0A + 0A·x1 + 0A·x2

POL(mark(x1)) = -I + 0A·x1

POL(0) = 0A

POL(2ndspos(x1, x2)) = 1A + 0A·x1 + 0A·x2

POL(times(x1, x2)) = 5A + 0A·x1 + 1A·x2

POL(A__TIMES(x1, x2)) = 5A + 0A·x1 + 1A·x2

POL(s(x1)) = -I + 0A·x1

POL(a__times(x1, x2)) = 5A + 0A·x1 + 1A·x2

POL(posrecip(x1)) = 1A + 1A·x1

POL(negrecip(x1)) = -I + 2A·x1

POL(cons(x1, x2)) = 0A + 2A·x1 + 0A·x2

POL(cons2(x1, x2)) = -I + -I·x1 + 0A·x2

POL(rcons(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(from(x1)) = 3A + 3A·x1

POL(a__from(x1)) = 3A + 3A·x1

POL(a__2ndspos(x1, x2)) = 1A + 0A·x1 + 0A·x2

POL(2ndsneg(x1, x2)) = 1A + 0A·x1 + 0A·x2

POL(a__2ndsneg(x1, x2)) = 1A + 0A·x1 + 0A·x2

POL(pi(x1)) = 3A + 0A·x1

POL(a__pi(x1)) = 3A + 0A·x1

POL(a__plus(x1, x2)) = 5A + 0A·x1 + 0A·x2

POL(square(x1)) = 5A + 3A·x1

POL(a__square(x1)) = 5A + 3A·x1

POL(nil) = 0A

POL(rnil) = 1A

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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))
a__plus(0, Y) → mark(Y)
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)))
mark(square(X)) → a__square(mark(X))
a__square(X) → a__times(mark(X), 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__times(0, Y) → 0
a__times(X1, X2) → times(X1, X2)
a__from(X) → from(X)
a__2ndspos(0, Z) → rnil
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__2ndsneg(0, Z) → rnil
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__pi(X) → pi(X)
a__plus(X1, X2) → plus(X1, X2)
a__square(X) → square(X)
a__plus(s(X), Y) → s(a__plus(mark(X), mark(Y)))
a__pi(X) → a__2ndspos(mark(X), a__from(0))
a__from(X) → cons(mark(X), from(s(X)))
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(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)))

(30) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(0, Y) → MARK(Y)
MARK(2ndspos(X1, X2)) → 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__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(cons(X1, X2)) → MARK(X1)
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))

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,JAR06].


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: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(MARK(x1)) = 0A + 0A·x1

POL(plus(x1, x2)) = 2A + -I·x1 + 0A·x2

POL(A__PLUS(x1, x2)) = 0A + -I·x1 + 0A·x2

POL(mark(x1)) = -I + 0A·x1

POL(0) = 0A

POL(2ndspos(x1, x2)) = -I + 5A·x1 + 0A·x2

POL(times(x1, x2)) = 2A + 1A·x1 + -I·x2

POL(A__TIMES(x1, x2)) = 2A + 1A·x1 + -I·x2

POL(s(x1)) = -I + 0A·x1

POL(a__times(x1, x2)) = 2A + 1A·x1 + -I·x2

POL(negrecip(x1)) = -I + 0A·x1

POL(cons(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(cons2(x1, x2)) = -I + -I·x1 + 0A·x2

POL(rcons(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(from(x1)) = -I + 0A·x1

POL(a__from(x1)) = -I + 0A·x1

POL(a__2ndspos(x1, x2)) = -I + 5A·x1 + 0A·x2

POL(2ndsneg(x1, x2)) = -I + 5A·x1 + 0A·x2

POL(a__2ndsneg(x1, x2)) = -I + 5A·x1 + 0A·x2

POL(pi(x1)) = 0A + 5A·x1

POL(a__pi(x1)) = 0A + 5A·x1

POL(a__plus(x1, x2)) = 2A + -I·x1 + 0A·x2

POL(square(x1)) = 5A + 2A·x1

POL(a__square(x1)) = 5A + 2A·x1

POL(posrecip(x1)) = -I + 0A·x1

POL(nil) = 0A

POL(rnil) = 4A

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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))
a__plus(0, Y) → mark(Y)
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)))
mark(square(X)) → a__square(mark(X))
a__square(X) → a__times(mark(X), 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__times(0, Y) → 0
a__times(X1, X2) → times(X1, X2)
a__from(X) → from(X)
a__2ndspos(0, Z) → rnil
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__2ndsneg(0, Z) → rnil
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__pi(X) → pi(X)
a__plus(X1, X2) → plus(X1, X2)
a__square(X) → square(X)
a__plus(s(X), Y) → s(a__plus(mark(X), mark(Y)))
a__pi(X) → a__2ndspos(mark(X), a__from(0))
a__from(X) → cons(mark(X), from(s(X)))
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(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)))

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(0, Y) → MARK(Y)
MARK(2ndspos(X1, X2)) → 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__PLUS(s(X), Y) → A__PLUS(mark(X), mark(Y))
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__PLUS(s(X), Y) → MARK(Y)
A__TIMES(s(X), Y) → A__TIMES(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.

(33) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(2ndspos(X1, X2)) → MARK(X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(MARK(x1)) = 4A + 2A·x1

POL(plus(x1, x2)) = -I + -I·x1 + 0A·x2

POL(A__PLUS(x1, x2)) = 4A + -I·x1 + 2A·x2

POL(mark(x1)) = -I + 0A·x1

POL(0) = 0A

POL(2ndspos(x1, x2)) = 4A + -I·x1 + 5A·x2

POL(times(x1, x2)) = 1A + -I·x1 + -I·x2

POL(A__TIMES(x1, x2)) = 4A + -I·x1 + -I·x2

POL(s(x1)) = -I + 0A·x1

POL(a__times(x1, x2)) = 1A + -I·x1 + -I·x2

POL(negrecip(x1)) = -I + 0A·x1

POL(cons(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(cons2(x1, x2)) = -I + -I·x1 + 0A·x2

POL(rcons(x1, x2)) = 1A + 0A·x1 + 0A·x2

POL(from(x1)) = 0A + 0A·x1

POL(a__from(x1)) = 0A + 0A·x1

POL(a__2ndspos(x1, x2)) = 4A + -I·x1 + 5A·x2

POL(2ndsneg(x1, x2)) = 4A + -I·x1 + 5A·x2

POL(a__2ndsneg(x1, x2)) = 4A + -I·x1 + 5A·x2

POL(pi(x1)) = 5A + -I·x1

POL(a__pi(x1)) = 5A + -I·x1

POL(a__plus(x1, x2)) = -I + -I·x1 + 0A·x2

POL(square(x1)) = 1A + 1A·x1

POL(a__square(x1)) = 1A + 1A·x1

POL(posrecip(x1)) = 0A + 5A·x1

POL(nil) = 2A

POL(rnil) = 3A

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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))
a__plus(0, Y) → mark(Y)
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)))
mark(square(X)) → a__square(mark(X))
a__square(X) → a__times(mark(X), 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__times(0, Y) → 0
a__times(X1, X2) → times(X1, X2)
a__from(X) → from(X)
a__2ndspos(0, Z) → rnil
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__2ndsneg(0, Z) → rnil
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__pi(X) → pi(X)
a__plus(X1, X2) → plus(X1, X2)
a__square(X) → square(X)
a__plus(s(X), Y) → s(a__plus(mark(X), mark(Y)))
a__pi(X) → a__2ndspos(mark(X), a__from(0))
a__from(X) → cons(mark(X), from(s(X)))
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(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)))

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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(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__PLUS(s(X), Y) → MARK(Y)
A__TIMES(s(X), Y) → A__TIMES(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.

(35) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


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(MARK(x1)) = -I + 0A·x1

POL(plus(x1, x2)) = 5A + -I·x1 + 0A·x2

POL(A__PLUS(x1, x2)) = 2A + -I·x1 + 0A·x2

POL(mark(x1)) = -I + 0A·x1

POL(0) = 0A

POL(times(x1, x2)) = 5A + 3A·x1 + -I·x2

POL(A__TIMES(x1, x2)) = 5A + 3A·x1 + -I·x2

POL(s(x1)) = -I + 0A·x1

POL(a__times(x1, x2)) = 5A + 3A·x1 + -I·x2

POL(negrecip(x1)) = -I + 4A·x1

POL(cons(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(cons2(x1, x2)) = -I + -I·x1 + 0A·x2

POL(rcons(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(from(x1)) = 0A + 0A·x1

POL(a__from(x1)) = 0A + 0A·x1

POL(2ndspos(x1, x2)) = 0A + 0A·x1 + 5A·x2

POL(a__2ndspos(x1, x2)) = 0A + 0A·x1 + 5A·x2

POL(2ndsneg(x1, x2)) = 0A + 0A·x1 + 5A·x2

POL(a__2ndsneg(x1, x2)) = 0A + 0A·x1 + 5A·x2

POL(pi(x1)) = 5A + 1A·x1

POL(a__pi(x1)) = 5A + 1A·x1

POL(a__plus(x1, x2)) = 5A + -I·x1 + 0A·x2

POL(square(x1)) = 5A + 5A·x1

POL(a__square(x1)) = 5A + 5A·x1

POL(posrecip(x1)) = 0A + 3A·x1

POL(nil) = 4A

POL(rnil) = 0A

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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))
a__plus(0, Y) → mark(Y)
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)))
mark(square(X)) → a__square(mark(X))
a__square(X) → a__times(mark(X), 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__times(0, Y) → 0
a__times(X1, X2) → times(X1, X2)
a__from(X) → from(X)
a__2ndspos(0, Z) → rnil
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__2ndsneg(0, Z) → rnil
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__pi(X) → pi(X)
a__plus(X1, X2) → plus(X1, X2)
a__square(X) → square(X)
a__plus(s(X), Y) → s(a__plus(mark(X), mark(Y)))
a__pi(X) → a__2ndspos(mark(X), a__from(0))
a__from(X) → cons(mark(X), from(s(X)))
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(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)))

(36) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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(cons(X1, X2)) → MARK(X1)
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))

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,JAR06].


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 Order [NEGPOLO,POLO] with Interpretation:
POL( A__PLUS(x1, x2) ) = x2 + 1

POL( A__TIMES(x1, x2) ) = 2

POL( mark(x1) ) = x1

POL( from(x1) ) = x1 + 1

POL( a__from(x1) ) = x1 + 1

POL( 2ndspos(x1, x2) ) = 0

POL( a__2ndspos(x1, x2) ) = 0

POL( 2ndsneg(x1, x2) ) = 0

POL( a__2ndsneg(x1, x2) ) = max{0, -1}

POL( pi(x1) ) = 0

POL( a__pi(x1) ) = max{0, -2}

POL( plus(x1, x2) ) = x2

POL( a__plus(x1, x2) ) = x2

POL( 0 ) = 0

POL( times(x1, x2) ) = 1

POL( a__times(x1, x2) ) = 1

POL( s(x1) ) = x1

POL( square(x1) ) = 2x1 + 2

POL( a__square(x1) ) = 2x1 + 2

POL( posrecip(x1) ) = max{0, -2}

POL( negrecip(x1) ) = max{0, -2}

POL( nil ) = 0

POL( cons(x1, x2) ) = x1

POL( cons2(x1, x2) ) = 2x2 + 1

POL( rnil ) = 0

POL( rcons(x1, x2) ) = 2x1 + x2

POL( MARK(x1) ) = x1 + 1


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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))
a__plus(0, Y) → mark(Y)
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)))
mark(square(X)) → a__square(mark(X))
a__square(X) → a__times(mark(X), 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__times(0, Y) → 0
a__times(X1, X2) → times(X1, X2)
a__from(X) → from(X)
a__2ndspos(0, Z) → rnil
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__2ndsneg(0, Z) → rnil
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__pi(X) → pi(X)
a__plus(X1, X2) → plus(X1, X2)
a__square(X) → square(X)
a__plus(s(X), Y) → s(a__plus(mark(X), mark(Y)))
a__pi(X) → a__2ndspos(mark(X), a__from(0))
a__from(X) → cons(mark(X), from(s(X)))
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(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)))

(38) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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(cons(X1, X2)) → MARK(X1)
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))

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,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(cons(X1, X2)) → MARK(X1)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( A__PLUS(x1, x2) ) = x2 + 1

POL( A__TIMES(x1, x2) ) = 1

POL( mark(x1) ) = x1

POL( from(x1) ) = 2x1 + 1

POL( a__from(x1) ) = 2x1 + 1

POL( 2ndspos(x1, x2) ) = 0

POL( a__2ndspos(x1, x2) ) = 0

POL( 2ndsneg(x1, x2) ) = 0

POL( a__2ndsneg(x1, x2) ) = 0

POL( pi(x1) ) = 2

POL( a__pi(x1) ) = 2

POL( plus(x1, x2) ) = 2x2

POL( a__plus(x1, x2) ) = 2x2

POL( 0 ) = 0

POL( times(x1, x2) ) = 0

POL( a__times(x1, x2) ) = max{0, -1}

POL( s(x1) ) = x1

POL( square(x1) ) = 0

POL( a__square(x1) ) = 0

POL( posrecip(x1) ) = 0

POL( negrecip(x1) ) = max{0, -1}

POL( nil ) = 0

POL( cons(x1, x2) ) = x1 + 1

POL( cons2(x1, x2) ) = x2

POL( rnil ) = 0

POL( rcons(x1, x2) ) = 2x1 + 2x2

POL( MARK(x1) ) = x1 + 1


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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))
a__plus(0, Y) → mark(Y)
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)))
mark(square(X)) → a__square(mark(X))
a__square(X) → a__times(mark(X), 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__times(0, Y) → 0
a__times(X1, X2) → times(X1, X2)
a__from(X) → from(X)
a__2ndspos(0, Z) → rnil
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__2ndsneg(0, Z) → rnil
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__pi(X) → pi(X)
a__plus(X1, X2) → plus(X1, X2)
a__square(X) → square(X)
a__plus(s(X), Y) → s(a__plus(mark(X), mark(Y)))
a__pi(X) → a__2ndspos(mark(X), a__from(0))
a__from(X) → cons(mark(X), from(s(X)))
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(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)))

(40) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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))

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,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(plus(X1, X2)) → A__PLUS(mark(X1), mark(X2))
A__PLUS(0, Y) → MARK(Y)
MARK(plus(X1, X2)) → 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))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
MARK(x1)  =  x1
plus(x1, x2)  =  plus(x1, x2)
A__PLUS(x1, x2)  =  A__PLUS(x1, x2)
mark(x1)  =  x1
0  =  0
times(x1, x2)  =  times(x1, x2)
A__TIMES(x1, x2)  =  A__TIMES(x1, x2)
s(x1)  =  s(x1)
a__times(x1, x2)  =  a__times(x1, x2)
rcons(x1, x2)  =  rcons(x1, x2)
from(x1)  =  from(x1)
a__from(x1)  =  a__from(x1)
2ndspos(x1, x2)  =  2ndspos(x1)
a__2ndspos(x1, x2)  =  a__2ndspos(x1)
2ndsneg(x1, x2)  =  2ndsneg(x1)
a__2ndsneg(x1, x2)  =  a__2ndsneg(x1)
pi(x1)  =  pi(x1)
a__pi(x1)  =  a__pi(x1)
a__plus(x1, x2)  =  a__plus(x1, x2)
square(x1)  =  square(x1)
a__square(x1)  =  a__square(x1)
posrecip(x1)  =  posrecip
negrecip(x1)  =  negrecip
nil  =  nil
cons(x1, x2)  =  cons(x1)
cons2(x1, x2)  =  cons2(x2)
rnil  =  rnil

Recursive path order with status [RPO].
Quasi-Precedence:
[from1, afrom1, pi1, api1, cons1] > [2ndspos1, a2ndspos1, 2ndsneg1, a2ndsneg1, negrecip] > [0, s1, rcons2, posrecip, rnil]
[square1, asquare1] > [times2, ATIMES2, atimes2] > [plus2, aplus2] > APLUS2 > [0, s1, rcons2, posrecip, rnil]
nil > [0, s1, rcons2, posrecip, rnil]
cons21 > [2ndspos1, a2ndspos1, 2ndsneg1, a2ndsneg1, negrecip] > [0, s1, rcons2, posrecip, rnil]

Status:
plus2: [2,1]
APLUS2: [1,2]
0: multiset
times2: [2,1]
ATIMES2: [2,1]
s1: [1]
atimes2: [2,1]
rcons2: [1,2]
from1: multiset
afrom1: multiset
2ndspos1: multiset
a2ndspos1: multiset
2ndsneg1: multiset
a2ndsneg1: multiset
pi1: multiset
api1: multiset
aplus2: [2,1]
square1: [1]
asquare1: [1]
posrecip: multiset
negrecip: multiset
nil: multiset
cons1: multiset
cons21: multiset
rnil: multiset


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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))
a__plus(0, Y) → mark(Y)
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)))
mark(square(X)) → a__square(mark(X))
a__square(X) → a__times(mark(X), 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__times(0, Y) → 0
a__times(X1, X2) → times(X1, X2)
a__from(X) → from(X)
a__2ndspos(0, Z) → rnil
a__2ndspos(X1, X2) → 2ndspos(X1, X2)
a__2ndsneg(0, Z) → rnil
a__2ndsneg(X1, X2) → 2ndsneg(X1, X2)
a__pi(X) → pi(X)
a__plus(X1, X2) → plus(X1, X2)
a__square(X) → square(X)
a__plus(s(X), Y) → s(a__plus(mark(X), mark(Y)))
a__pi(X) → a__2ndspos(mark(X), a__from(0))
a__from(X) → cons(mark(X), from(s(X)))
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(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)))

(42) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MARK(times(X1, X2)) → A__TIMES(mark(X1), 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.

(43) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(44) TRUE