YES
proof of Transformed_CSR_04_ExAppendixB_AEL03_GM.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 jera 20211004 unpublished


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

(0) QTRS
(1) DependencyPairsProof [EQUIVALENT, 0 ms]
(2) QDP
(3) QDPOrderProof [EQUIVALENT, 338 ms]
(4) QDP
(5) QDPOrderProof [EQUIVALENT, 331 ms]
(6) QDP
(7) DependencyGraphProof [EQUIVALENT, 0 ms]
(8) QDP
(9) QDPOrderProof [EQUIVALENT, 280 ms]
(10) QDP
(11) DependencyGraphProof [EQUIVALENT, 0 ms]
(12) AND
    (13) QDP
        (14) QDPOrderProof [EQUIVALENT, 344 ms]
        (15) QDP
        (16) DependencyGraphProof [EQUIVALENT, 0 ms]
        (17) TRUE
    (18) QDP
        (19) QDPOrderProof [EQUIVALENT, 258 ms]
        (20) QDP
        (21) QDPOrderProof [EQUIVALENT, 163 ms]
        (22) QDP
        (23) QDPOrderProof [EQUIVALENT, 221 ms]
        (24) QDP
        (25) DependencyGraphProof [EQUIVALENT, 0 ms]
        (26) QDP
        (27) QDPOrderProof [EQUIVALENT, 272 ms]
        (28) QDP
        (29) QDPOrderProof [EQUIVALENT, 208 ms]
        (30) QDP
        (31) QDPOrderProof [EQUIVALENT, 164 ms]
        (32) QDP
        (33) QDPOrderProof [EQUIVALENT, 165 ms]
        (34) QDP
        (35) QDPOrderProof [EQUIVALENT, 132 ms]
        (36) QDP
        (37) QDPOrderProof [EQUIVALENT, 102 ms]
        (38) QDP
        (39) QDPOrderProof [EQUIVALENT, 93 ms]
        (40) QDP
        (41) QDPOrderProof [EQUIVALENT, 350 ms]
        (42) QDP
        (43) DependencyGraphProof [EQUIVALENT, 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)
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)
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(x_1)) =  	[[4A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(MARK(x_1)) =  	[[4A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(A__2NDSPOS(x_1, x_2)) =  	[[4A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(s(x_1)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(cons(x_1, x_2)) =  	[[1A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(mark(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(cons2(x_1, x_2)) =  	[[1A]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(A__2NDSNEG(x_1, x_2)) =  	[[4A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(A__PI(x_1)) =  	[[5A]] 	 +  	[[3A]] 	* 	x_1
>>>

   <<<
 POL(a__from(x_1)) =  	[[4A]] 	 +  	[[4A]] 	* 	x_1
>>>

   <<<
 POL(0) =  	[[0A]]
>>>

   <<<
 POL(A__PLUS(x_1, x_2)) =  	[[4A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(A__TIMES(x_1, x_2)) =  	[[5A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(a__times(x_1, x_2)) =  	[[5A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(A__SQUARE(x_1)) =  	[[5A]] 	 +  	[[2A]] 	* 	x_1
>>>

   <<<
 POL(from(x_1)) =  	[[4A]] 	 +  	[[4A]] 	* 	x_1
>>>

   <<<
 POL(2ndspos(x_1, x_2)) =  	[[3A]] 	 +  	[[5A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(2ndsneg(x_1, x_2)) =  	[[4A]] 	 +  	[[5A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(pi(x_1)) =  	[[5A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 POL(plus(x_1, x_2)) =  	[[4A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(times(x_1, x_2)) =  	[[5A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(square(x_1)) =  	[[5A]] 	 +  	[[3A]] 	* 	x_1
>>>

   <<<
 POL(posrecip(x_1)) =  	[[5A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(negrecip(x_1)) =  	[[5A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(rcons(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(a__2ndspos(x_1, x_2)) =  	[[3A]] 	 +  	[[5A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(a__2ndsneg(x_1, x_2)) =  	[[4A]] 	 +  	[[5A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(a__pi(x_1)) =  	[[5A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 POL(a__plus(x_1, x_2)) =  	[[4A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(a__square(x_1)) =  	[[5A]] 	 +  	[[3A]] 	* 	x_1
>>>

   <<<
 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)
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(x_1)) =  	[[4A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(MARK(x_1)) =  	[[1A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(A__2NDSPOS(x_1, x_2)) =  	[[1A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(s(x_1)) =  	[[1A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(cons(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(mark(x_1)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(cons2(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(A__2NDSNEG(x_1, x_2)) =  	[[1A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(A__PI(x_1)) =  	[[4A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(a__from(x_1)) =  	[[4A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(0) =  	[[1A]]
>>>

   <<<
 POL(A__PLUS(x_1, x_2)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(A__TIMES(x_1, x_2)) =  	[[4A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[3A]] 	* 	x_2
>>>

   <<<
 POL(a__times(x_1, x_2)) =  	[[4A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[3A]] 	* 	x_2
>>>

   <<<
 POL(A__SQUARE(x_1)) =  	[[4A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 POL(from(x_1)) =  	[[4A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(2ndspos(x_1, x_2)) =  	[[1A]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(2ndsneg(x_1, x_2)) =  	[[1A]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(pi(x_1)) =  	[[5A]] 	 +  	[[2A]] 	* 	x_1
>>>

   <<<
 POL(plus(x_1, x_2)) =  	[[4A]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(times(x_1, x_2)) =  	[[4A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[3A]] 	* 	x_2
>>>

   <<<
 POL(square(x_1)) =  	[[5A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 POL(posrecip(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(negrecip(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(rcons(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(a__2ndspos(x_1, x_2)) =  	[[1A]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(a__2ndsneg(x_1, x_2)) =  	[[1A]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(a__pi(x_1)) =  	[[5A]] 	 +  	[[2A]] 	* 	x_1
>>>

   <<<
 POL(a__plus(x_1, x_2)) =  	[[4A]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(a__square(x_1)) =  	[[5A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 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)
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)
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(x_1)) =  	[[3A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(from(x_1)) =  	[[4A]] 	 +  	[[1A]] 	* 	x_1
>>>

   <<<
 POL(A__FROM(x_1)) =  	[[3A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(mark(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(2ndspos(x_1, x_2)) =  	[[3A]] 	 +  	[[3A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(A__2NDSPOS(x_1, x_2)) =  	[[3A]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(s(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(cons(x_1, x_2)) =  	[[4A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(cons2(x_1, x_2)) =  	[[4A]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(2ndsneg(x_1, x_2)) =  	[[5A]] 	 +  	[[3A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(A__2NDSNEG(x_1, x_2)) =  	[[1A]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(plus(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(A__PLUS(x_1, x_2)) =  	[[3A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(0) =  	[[1A]]
>>>

   <<<
 POL(times(x_1, x_2)) =  	[[-I]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(A__TIMES(x_1, x_2)) =  	[[3A]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(a__times(x_1, x_2)) =  	[[-I]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(square(x_1)) =  	[[3A]] 	 +  	[[3A]] 	* 	x_1
>>>

   <<<
 POL(A__SQUARE(x_1)) =  	[[3A]] 	 +  	[[2A]] 	* 	x_1
>>>

   <<<
 POL(posrecip(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(negrecip(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(rcons(x_1, x_2)) =  	[[-I]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(a__from(x_1)) =  	[[4A]] 	 +  	[[1A]] 	* 	x_1
>>>

   <<<
 POL(a__2ndspos(x_1, x_2)) =  	[[3A]] 	 +  	[[3A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(a__2ndsneg(x_1, x_2)) =  	[[5A]] 	 +  	[[3A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(pi(x_1)) =  	[[5A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 POL(a__pi(x_1)) =  	[[5A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 POL(a__plus(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(a__square(x_1)) =  	[[3A]] 	 +  	[[3A]] 	* 	x_1
>>>

   <<<
 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)
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)
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, a__2ndsneg] > [A__2NDSPOS_1, cons, A__2NDSNEG_1] > [s_1, posrecip, negrecip]
[cons2, 2ndsneg, a__2ndsneg] > rnil > [s_1, posrecip, negrecip]
[from_1, a__from_1] > [A__2NDSPOS_1, cons, A__2NDSNEG_1] > [s_1, posrecip, negrecip]
0 > rnil > [s_1, posrecip, negrecip]
[square_1, a__square_1] > [times_2, a__times_2] > [plus_2, a__plus_2] > [s_1, posrecip, negrecip]
nil > [s_1, posrecip, negrecip]

Status: A__2NDSPOS_1: [1]
s_1: [1]
cons2: multiset status
cons: multiset status
A__2NDSNEG_1: [1]
from_1: multiset status
a__from_1: multiset status
2ndsneg: []
a__2ndsneg: []
plus_2: [1,2]
a__plus_2: [1,2]
0: multiset status
times_2: [1,2]
a__times_2: [1,2]
square_1: multiset status
a__square_1: multiset status
posrecip: multiset status
negrecip: []
nil: multiset status
rnil: multiset status


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)
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)
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(x_1)) =  	[[3A]] 	 +  	[[4A]] 	* 	x_1
>>>

   <<<
 POL(2ndspos(x_1, x_2)) =  	[[-I]] 	 +  	[[5A]] 	* 	x_1 	 +  	[[5A]] 	* 	x_2
>>>

   <<<
 POL(plus(x_1, x_2)) =  	[[-I]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(A__PLUS(x_1, x_2)) =  	[[2A]] 	 +  	[[4A]] 	* 	x_1 	 +  	[[4A]] 	* 	x_2
>>>

   <<<
 POL(mark(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(0) =  	[[0A]]
>>>

   <<<
 POL(times(x_1, x_2)) =  	[[-I]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(A__TIMES(x_1, x_2)) =  	[[3A]] 	 +  	[[5A]] 	* 	x_1 	 +  	[[5A]] 	* 	x_2
>>>

   <<<
 POL(s(x_1)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(a__times(x_1, x_2)) =  	[[-I]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(square(x_1)) =  	[[-I]] 	 +  	[[1A]] 	* 	x_1
>>>

   <<<
 POL(A__SQUARE(x_1)) =  	[[3A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 POL(posrecip(x_1)) =  	[[-I]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 POL(negrecip(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(cons(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(cons2(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(rcons(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(from(x_1)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(a__from(x_1)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(a__2ndspos(x_1, x_2)) =  	[[-I]] 	 +  	[[5A]] 	* 	x_1 	 +  	[[5A]] 	* 	x_2
>>>

   <<<
 POL(2ndsneg(x_1, x_2)) =  	[[0A]] 	 +  	[[5A]] 	* 	x_1 	 +  	[[5A]] 	* 	x_2
>>>

   <<<
 POL(a__2ndsneg(x_1, x_2)) =  	[[0A]] 	 +  	[[5A]] 	* 	x_1 	 +  	[[5A]] 	* 	x_2
>>>

   <<<
 POL(pi(x_1)) =  	[[5A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 POL(a__pi(x_1)) =  	[[5A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 POL(a__plus(x_1, x_2)) =  	[[-I]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(a__square(x_1)) =  	[[-I]] 	 +  	[[1A]] 	* 	x_1
>>>

   <<<
 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)
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(x_1)) =  	[[5A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 POL(2ndspos(x_1, x_2)) =  	[[4A]] 	 +  	[[4A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(plus(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(A__PLUS(x_1, x_2)) =  	[[5A]] 	 +  	[[5A]] 	* 	x_1 	 +  	[[5A]] 	* 	x_2
>>>

   <<<
 POL(mark(x_1)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(0) =  	[[4A]]
>>>

   <<<
 POL(times(x_1, x_2)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(A__TIMES(x_1, x_2)) =  	[[5A]] 	 +  	[[5A]] 	* 	x_1 	 +  	[[5A]] 	* 	x_2
>>>

   <<<
 POL(s(x_1)) =  	[[1A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(a__times(x_1, x_2)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(square(x_1)) =  	[[1A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(A__SQUARE(x_1)) =  	[[5A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 POL(posrecip(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(negrecip(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(cons(x_1, x_2)) =  	[[2A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(cons2(x_1, x_2)) =  	[[5A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(rcons(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(from(x_1)) =  	[[2A]] 	 +  	[[1A]] 	* 	x_1
>>>

   <<<
 POL(a__from(x_1)) =  	[[2A]] 	 +  	[[1A]] 	* 	x_1
>>>

   <<<
 POL(a__2ndspos(x_1, x_2)) =  	[[4A]] 	 +  	[[4A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(2ndsneg(x_1, x_2)) =  	[[5A]] 	 +  	[[4A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(a__2ndsneg(x_1, x_2)) =  	[[5A]] 	 +  	[[4A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(pi(x_1)) =  	[[5A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 POL(a__pi(x_1)) =  	[[5A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 POL(a__plus(x_1, x_2)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(a__square(x_1)) =  	[[1A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 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)
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(x_1)) =  	[[0A]] 	 +  	[[1A]] 	* 	x_1
>>>

   <<<
 POL(2ndspos(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(plus(x_1, x_2)) =  	[[-I]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(A__PLUS(x_1, x_2)) =  	[[0A]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(mark(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(0) =  	[[0A]]
>>>

   <<<
 POL(times(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[3A]] 	* 	x_2
>>>

   <<<
 POL(A__TIMES(x_1, x_2)) =  	[[0A]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[4A]] 	* 	x_2
>>>

   <<<
 POL(s(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(a__times(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[3A]] 	* 	x_2
>>>

   <<<
 POL(square(x_1)) =  	[[3A]] 	 +  	[[4A]] 	* 	x_1
>>>

   <<<
 POL(A__SQUARE(x_1)) =  	[[4A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 POL(posrecip(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(negrecip(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(cons(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(cons2(x_1, x_2)) =  	[[-I]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(rcons(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(from(x_1)) =  	[[3A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 POL(a__from(x_1)) =  	[[3A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 POL(a__2ndspos(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(2ndsneg(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(a__2ndsneg(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(pi(x_1)) =  	[[5A]] 	 +  	[[3A]] 	* 	x_1
>>>

   <<<
 POL(a__pi(x_1)) =  	[[5A]] 	 +  	[[3A]] 	* 	x_1
>>>

   <<<
 POL(a__plus(x_1, x_2)) =  	[[-I]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(a__square(x_1)) =  	[[3A]] 	 +  	[[4A]] 	* 	x_1
>>>

   <<<
 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)
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)
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(x_1)) =  	[[5A]] 	 +  	[[3A]] 	* 	x_1
>>>

   <<<
 POL(plus(x_1, x_2)) =  	[[5A]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(A__PLUS(x_1, x_2)) =  	[[5A]] 	 +  	[[4A]] 	* 	x_1 	 +  	[[3A]] 	* 	x_2
>>>

   <<<
 POL(mark(x_1)) =  	[[4A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(0) =  	[[0A]]
>>>

   <<<
 POL(2ndspos(x_1, x_2)) =  	[[-I]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(times(x_1, x_2)) =  	[[5A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(A__TIMES(x_1, x_2)) =  	[[5A]] 	 +  	[[3A]] 	* 	x_1 	 +  	[[4A]] 	* 	x_2
>>>

   <<<
 POL(s(x_1)) =  	[[5A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(a__times(x_1, x_2)) =  	[[5A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(posrecip(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(negrecip(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(cons(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(cons2(x_1, x_2)) =  	[[-I]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(rcons(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(from(x_1)) =  	[[5A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(a__from(x_1)) =  	[[5A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(a__2ndspos(x_1, x_2)) =  	[[4A]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(2ndsneg(x_1, x_2)) =  	[[4A]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(a__2ndsneg(x_1, x_2)) =  	[[4A]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(pi(x_1)) =  	[[5A]] 	 +  	[[-I]] 	* 	x_1
>>>

   <<<
 POL(a__pi(x_1)) =  	[[5A]] 	 +  	[[-I]] 	* 	x_1
>>>

   <<<
 POL(a__plus(x_1, x_2)) =  	[[5A]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(square(x_1)) =  	[[5A]] 	 +  	[[1A]] 	* 	x_1
>>>

   <<<
 POL(a__square(x_1)) =  	[[5A]] 	 +  	[[1A]] 	* 	x_1
>>>

   <<<
 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)
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(x_1)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(plus(x_1, x_2)) =  	[[5A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(A__PLUS(x_1, x_2)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(mark(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(0) =  	[[0A]]
>>>

   <<<
 POL(2ndspos(x_1, x_2)) =  	[[1A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(times(x_1, x_2)) =  	[[5A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(A__TIMES(x_1, x_2)) =  	[[5A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(s(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(a__times(x_1, x_2)) =  	[[5A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[1A]] 	* 	x_2
>>>

   <<<
 POL(posrecip(x_1)) =  	[[1A]] 	 +  	[[1A]] 	* 	x_1
>>>

   <<<
 POL(negrecip(x_1)) =  	[[-I]] 	 +  	[[2A]] 	* 	x_1
>>>

   <<<
 POL(cons(x_1, x_2)) =  	[[0A]] 	 +  	[[2A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(cons2(x_1, x_2)) =  	[[-I]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(rcons(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(from(x_1)) =  	[[3A]] 	 +  	[[3A]] 	* 	x_1
>>>

   <<<
 POL(a__from(x_1)) =  	[[3A]] 	 +  	[[3A]] 	* 	x_1
>>>

   <<<
 POL(a__2ndspos(x_1, x_2)) =  	[[1A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(2ndsneg(x_1, x_2)) =  	[[1A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(a__2ndsneg(x_1, x_2)) =  	[[1A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(pi(x_1)) =  	[[3A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(a__pi(x_1)) =  	[[3A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(a__plus(x_1, x_2)) =  	[[5A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(square(x_1)) =  	[[5A]] 	 +  	[[3A]] 	* 	x_1
>>>

   <<<
 POL(a__square(x_1)) =  	[[5A]] 	 +  	[[3A]] 	* 	x_1
>>>

   <<<
 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)
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(x_1)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(plus(x_1, x_2)) =  	[[2A]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(A__PLUS(x_1, x_2)) =  	[[0A]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(mark(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(0) =  	[[0A]]
>>>

   <<<
 POL(2ndspos(x_1, x_2)) =  	[[-I]] 	 +  	[[5A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(times(x_1, x_2)) =  	[[2A]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[-I]] 	* 	x_2
>>>

   <<<
 POL(A__TIMES(x_1, x_2)) =  	[[2A]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[-I]] 	* 	x_2
>>>

   <<<
 POL(s(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(a__times(x_1, x_2)) =  	[[2A]] 	 +  	[[1A]] 	* 	x_1 	 +  	[[-I]] 	* 	x_2
>>>

   <<<
 POL(negrecip(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(cons(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(cons2(x_1, x_2)) =  	[[-I]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(rcons(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(from(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(a__from(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(a__2ndspos(x_1, x_2)) =  	[[-I]] 	 +  	[[5A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(2ndsneg(x_1, x_2)) =  	[[-I]] 	 +  	[[5A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(a__2ndsneg(x_1, x_2)) =  	[[-I]] 	 +  	[[5A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(pi(x_1)) =  	[[0A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 POL(a__pi(x_1)) =  	[[0A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 POL(a__plus(x_1, x_2)) =  	[[2A]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(square(x_1)) =  	[[5A]] 	 +  	[[2A]] 	* 	x_1
>>>

   <<<
 POL(a__square(x_1)) =  	[[5A]] 	 +  	[[2A]] 	* 	x_1
>>>

   <<<
 POL(posrecip(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 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)
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(x_1)) =  	[[4A]] 	 +  	[[2A]] 	* 	x_1
>>>

   <<<
 POL(plus(x_1, x_2)) =  	[[-I]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(A__PLUS(x_1, x_2)) =  	[[4A]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[2A]] 	* 	x_2
>>>

   <<<
 POL(mark(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(0) =  	[[0A]]
>>>

   <<<
 POL(2ndspos(x_1, x_2)) =  	[[4A]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[5A]] 	* 	x_2
>>>

   <<<
 POL(times(x_1, x_2)) =  	[[1A]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[-I]] 	* 	x_2
>>>

   <<<
 POL(A__TIMES(x_1, x_2)) =  	[[4A]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[-I]] 	* 	x_2
>>>

   <<<
 POL(s(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(a__times(x_1, x_2)) =  	[[1A]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[-I]] 	* 	x_2
>>>

   <<<
 POL(negrecip(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(cons(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(cons2(x_1, x_2)) =  	[[-I]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(rcons(x_1, x_2)) =  	[[1A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(from(x_1)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(a__from(x_1)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(a__2ndspos(x_1, x_2)) =  	[[4A]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[5A]] 	* 	x_2
>>>

   <<<
 POL(2ndsneg(x_1, x_2)) =  	[[4A]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[5A]] 	* 	x_2
>>>

   <<<
 POL(a__2ndsneg(x_1, x_2)) =  	[[4A]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[5A]] 	* 	x_2
>>>

   <<<
 POL(pi(x_1)) =  	[[5A]] 	 +  	[[-I]] 	* 	x_1
>>>

   <<<
 POL(a__pi(x_1)) =  	[[5A]] 	 +  	[[-I]] 	* 	x_1
>>>

   <<<
 POL(a__plus(x_1, x_2)) =  	[[-I]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(square(x_1)) =  	[[1A]] 	 +  	[[1A]] 	* 	x_1
>>>

   <<<
 POL(a__square(x_1)) =  	[[1A]] 	 +  	[[1A]] 	* 	x_1
>>>

   <<<
 POL(posrecip(x_1)) =  	[[0A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 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)
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(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(plus(x_1, x_2)) =  	[[5A]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(A__PLUS(x_1, x_2)) =  	[[2A]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(mark(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(0) =  	[[0A]]
>>>

   <<<
 POL(times(x_1, x_2)) =  	[[5A]] 	 +  	[[3A]] 	* 	x_1 	 +  	[[-I]] 	* 	x_2
>>>

   <<<
 POL(A__TIMES(x_1, x_2)) =  	[[5A]] 	 +  	[[3A]] 	* 	x_1 	 +  	[[-I]] 	* 	x_2
>>>

   <<<
 POL(s(x_1)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(a__times(x_1, x_2)) =  	[[5A]] 	 +  	[[3A]] 	* 	x_1 	 +  	[[-I]] 	* 	x_2
>>>

   <<<
 POL(negrecip(x_1)) =  	[[-I]] 	 +  	[[4A]] 	* 	x_1
>>>

   <<<
 POL(cons(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(cons2(x_1, x_2)) =  	[[-I]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(rcons(x_1, x_2)) =  	[[-I]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(from(x_1)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(a__from(x_1)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1
>>>

   <<<
 POL(2ndspos(x_1, x_2)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[5A]] 	* 	x_2
>>>

   <<<
 POL(a__2ndspos(x_1, x_2)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[5A]] 	* 	x_2
>>>

   <<<
 POL(2ndsneg(x_1, x_2)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[5A]] 	* 	x_2
>>>

   <<<
 POL(a__2ndsneg(x_1, x_2)) =  	[[0A]] 	 +  	[[0A]] 	* 	x_1 	 +  	[[5A]] 	* 	x_2
>>>

   <<<
 POL(pi(x_1)) =  	[[5A]] 	 +  	[[1A]] 	* 	x_1
>>>

   <<<
 POL(a__pi(x_1)) =  	[[5A]] 	 +  	[[1A]] 	* 	x_1
>>>

   <<<
 POL(a__plus(x_1, x_2)) =  	[[5A]] 	 +  	[[-I]] 	* 	x_1 	 +  	[[0A]] 	* 	x_2
>>>

   <<<
 POL(square(x_1)) =  	[[5A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 POL(a__square(x_1)) =  	[[5A]] 	 +  	[[5A]] 	* 	x_1
>>>

   <<<
 POL(posrecip(x_1)) =  	[[0A]] 	 +  	[[3A]] 	* 	x_1
>>>

   <<<
 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)
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_2(x_1, x_2) ) = x_2 + 1
POL( A__TIMES_2(x_1, x_2) ) = 2
POL( mark_1(x_1) ) = x_1
POL( from_1(x_1) ) = x_1 + 1
POL( a__from_1(x_1) ) = x_1 + 1
POL( 2ndspos_2(x_1, x_2) ) = 0
POL( a__2ndspos_2(x_1, x_2) ) = 0
POL( 2ndsneg_2(x_1, x_2) ) = 0
POL( a__2ndsneg_2(x_1, x_2) ) = max{0, -1}
POL( pi_1(x_1) ) = 0
POL( a__pi_1(x_1) ) = max{0, -2}
POL( plus_2(x_1, x_2) ) = x_2
POL( a__plus_2(x_1, x_2) ) = x_2
POL( 0 ) = 0
POL( times_2(x_1, x_2) ) = 1
POL( a__times_2(x_1, x_2) ) = 1
POL( s_1(x_1) ) = x_1
POL( square_1(x_1) ) = 2x_1 + 2
POL( a__square_1(x_1) ) = 2x_1 + 2
POL( posrecip_1(x_1) ) = max{0, -2}
POL( negrecip_1(x_1) ) = max{0, -2}
POL( nil ) = 0
POL( cons_2(x_1, x_2) ) = x_1
POL( cons2_2(x_1, x_2) ) = 2x_2 + 1
POL( rnil ) = 0
POL( rcons_2(x_1, x_2) ) = 2x_1 + x_2
POL( MARK_1(x_1) ) = x_1 + 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)
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_2(x_1, x_2) ) = x_2 + 1
POL( A__TIMES_2(x_1, x_2) ) = 1
POL( mark_1(x_1) ) = x_1
POL( from_1(x_1) ) = 2x_1 + 1
POL( a__from_1(x_1) ) = 2x_1 + 1
POL( 2ndspos_2(x_1, x_2) ) = 0
POL( a__2ndspos_2(x_1, x_2) ) = 0
POL( 2ndsneg_2(x_1, x_2) ) = 0
POL( a__2ndsneg_2(x_1, x_2) ) = 0
POL( pi_1(x_1) ) = 2
POL( a__pi_1(x_1) ) = 2
POL( plus_2(x_1, x_2) ) = 2x_2
POL( a__plus_2(x_1, x_2) ) = 2x_2
POL( 0 ) = 0
POL( times_2(x_1, x_2) ) = 0
POL( a__times_2(x_1, x_2) ) = max{0, -1}
POL( s_1(x_1) ) = x_1
POL( square_1(x_1) ) = 0
POL( a__square_1(x_1) ) = 0
POL( posrecip_1(x_1) ) = 0
POL( negrecip_1(x_1) ) = max{0, -1}
POL( nil ) = 0
POL( cons_2(x_1, x_2) ) = x_1 + 1
POL( cons2_2(x_1, x_2) ) = x_2
POL( rnil ) = 0
POL( rcons_2(x_1, x_2) ) = 2x_1 + 2x_2
POL( MARK_1(x_1) ) = x_1 + 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)
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: [from_1, a__from_1, pi_1, a__pi_1, cons_1] > [2ndspos_1, a__2ndspos_1, 2ndsneg_1, a__2ndsneg_1, negrecip] > [0, s_1, rcons_2, posrecip, rnil]
[square_1, a__square_1] > [times_2, A__TIMES_2, a__times_2] > [plus_2, a__plus_2] > A__PLUS_2 > [0, s_1, rcons_2, posrecip, rnil]
nil > [0, s_1, rcons_2, posrecip, rnil]
cons2_1 > [2ndspos_1, a__2ndspos_1, 2ndsneg_1, a__2ndsneg_1, negrecip] > [0, s_1, rcons_2, posrecip, rnil]

Status: plus_2: [2,1]
A__PLUS_2: [1,2]
0: multiset status
times_2: [2,1]
A__TIMES_2: [2,1]
s_1: [1]
a__times_2: [2,1]
rcons_2: [1,2]
from_1: multiset status
a__from_1: multiset status
2ndspos_1: multiset status
a__2ndspos_1: multiset status
2ndsneg_1: multiset status
a__2ndsneg_1: multiset status
pi_1: multiset status
a__pi_1: multiset status
a__plus_2: [2,1]
square_1: [1]
a__square_1: [1]
posrecip: multiset status
negrecip: multiset status
nil: multiset status
cons_1: multiset status
cons2_1: multiset status
rnil: multiset status


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)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
----------------------------------------

(44)
TRUE