Term Rewriting System R:
[X, Z, N, Y, X1, X2]
afrom(X) -> cons(mark(X), from(s(X)))
afrom(X) -> from(X)
a2ndspos(0, Z) -> rnil
a2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a2ndsneg(mark(N), mark(Z)))
a2ndspos(X1, X2) -> 2ndspos(X1, X2)
a2ndsneg(0, Z) -> rnil
a2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a2ndspos(mark(N), mark(Z)))
a2ndsneg(X1, X2) -> 2ndsneg(X1, X2)
api(X) -> a2ndspos(mark(X), afrom(0))
api(X) -> pi(X)
aplus(0, Y) -> mark(Y)
aplus(s(X), Y) -> s(aplus(mark(X), mark(Y)))
aplus(X1, X2) -> plus(X1, X2)
atimes(0, Y) -> 0
atimes(s(X), Y) -> aplus(mark(Y), atimes(mark(X), mark(Y)))
atimes(X1, X2) -> times(X1, X2)
asquare(X) -> atimes(mark(X), mark(X))
asquare(X) -> square(X)
mark(from(X)) -> afrom(mark(X))
mark(2ndspos(X1, X2)) -> a2ndspos(mark(X1), mark(X2))
mark(2ndsneg(X1, X2)) -> a2ndsneg(mark(X1), mark(X2))
mark(pi(X)) -> api(mark(X))
mark(plus(X1, X2)) -> aplus(mark(X1), mark(X2))
mark(times(X1, X2)) -> atimes(mark(X1), mark(X2))
mark(square(X)) -> asquare(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(rnil) -> rnil
mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2))

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

AFROM(X) -> MARK(X)
A2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Y)
A2NDSPOS(s(N), cons(X, cons(Y, Z))) -> A2NDSNEG(mark(N), mark(Z))
A2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(N)
A2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Z)
A2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Y)
A2NDSNEG(s(N), cons(X, cons(Y, Z))) -> A2NDSPOS(mark(N), mark(Z))
A2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(N)
A2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Z)
API(X) -> A2NDSPOS(mark(X), afrom(0))
API(X) -> MARK(X)
API(X) -> AFROM(0)
APLUS(0, Y) -> MARK(Y)
APLUS(s(X), Y) -> APLUS(mark(X), mark(Y))
APLUS(s(X), Y) -> MARK(X)
APLUS(s(X), Y) -> MARK(Y)
ATIMES(s(X), Y) -> APLUS(mark(Y), atimes(mark(X), mark(Y)))
ATIMES(s(X), Y) -> MARK(Y)
ATIMES(s(X), Y) -> ATIMES(mark(X), mark(Y))
ATIMES(s(X), Y) -> MARK(X)
ASQUARE(X) -> ATIMES(mark(X), mark(X))
ASQUARE(X) -> MARK(X)
MARK(from(X)) -> AFROM(mark(X))
MARK(from(X)) -> MARK(X)
MARK(2ndspos(X1, X2)) -> A2NDSPOS(mark(X1), mark(X2))
MARK(2ndspos(X1, X2)) -> MARK(X1)
MARK(2ndspos(X1, X2)) -> MARK(X2)
MARK(2ndsneg(X1, X2)) -> A2NDSNEG(mark(X1), mark(X2))
MARK(2ndsneg(X1, X2)) -> MARK(X1)
MARK(2ndsneg(X1, X2)) -> MARK(X2)
MARK(pi(X)) -> API(mark(X))
MARK(pi(X)) -> MARK(X)
MARK(plus(X1, X2)) -> APLUS(mark(X1), mark(X2))
MARK(plus(X1, X2)) -> MARK(X1)
MARK(plus(X1, X2)) -> MARK(X2)
MARK(times(X1, X2)) -> ATIMES(mark(X1), mark(X2))
MARK(times(X1, X2)) -> MARK(X1)
MARK(times(X1, X2)) -> MARK(X2)
MARK(square(X)) -> ASQUARE(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(rcons(X1, X2)) -> MARK(X1)
MARK(rcons(X1, X2)) -> MARK(X2)

Furthermore, R contains one SCC.


   R
DPs
       →DP Problem 1
Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

API(X) -> AFROM(0)
API(X) -> MARK(X)
A2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Z)
A2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(N)
A2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Z)
APLUS(s(X), Y) -> MARK(Y)
ASQUARE(X) -> MARK(X)
ATIMES(s(X), Y) -> MARK(X)
ATIMES(s(X), Y) -> ATIMES(mark(X), mark(Y))
MARK(rcons(X1, X2)) -> MARK(X2)
MARK(rcons(X1, X2)) -> MARK(X1)
MARK(cons(X1, X2)) -> MARK(X1)
MARK(negrecip(X)) -> MARK(X)
MARK(posrecip(X)) -> MARK(X)
MARK(s(X)) -> MARK(X)
MARK(square(X)) -> MARK(X)
ATIMES(s(X), Y) -> MARK(Y)
ASQUARE(X) -> ATIMES(mark(X), mark(X))
MARK(square(X)) -> ASQUARE(mark(X))
MARK(times(X1, X2)) -> MARK(X2)
MARK(times(X1, X2)) -> MARK(X1)
APLUS(s(X), Y) -> MARK(X)
APLUS(s(X), Y) -> APLUS(mark(X), mark(Y))
ATIMES(s(X), Y) -> APLUS(mark(Y), atimes(mark(X), mark(Y)))
MARK(times(X1, X2)) -> ATIMES(mark(X1), mark(X2))
MARK(plus(X1, X2)) -> MARK(X2)
MARK(plus(X1, X2)) -> MARK(X1)
APLUS(0, Y) -> MARK(Y)
MARK(plus(X1, X2)) -> APLUS(mark(X1), mark(X2))
MARK(pi(X)) -> MARK(X)
A2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(N)
A2NDSNEG(s(N), cons(X, cons(Y, Z))) -> A2NDSPOS(mark(N), mark(Z))
A2NDSPOS(s(N), cons(X, cons(Y, Z))) -> A2NDSNEG(mark(N), mark(Z))
API(X) -> A2NDSPOS(mark(X), afrom(0))
MARK(pi(X)) -> API(mark(X))
MARK(2ndsneg(X1, X2)) -> MARK(X2)
MARK(2ndsneg(X1, X2)) -> MARK(X1)
A2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Y)
MARK(2ndsneg(X1, X2)) -> A2NDSNEG(mark(X1), mark(X2))
MARK(2ndspos(X1, X2)) -> MARK(X2)
MARK(2ndspos(X1, X2)) -> MARK(X1)
A2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Y)
MARK(2ndspos(X1, X2)) -> A2NDSPOS(mark(X1), mark(X2))
MARK(from(X)) -> MARK(X)
MARK(from(X)) -> AFROM(mark(X))
AFROM(X) -> MARK(X)


Rules:


afrom(X) -> cons(mark(X), from(s(X)))
afrom(X) -> from(X)
a2ndspos(0, Z) -> rnil
a2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a2ndsneg(mark(N), mark(Z)))
a2ndspos(X1, X2) -> 2ndspos(X1, X2)
a2ndsneg(0, Z) -> rnil
a2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a2ndspos(mark(N), mark(Z)))
a2ndsneg(X1, X2) -> 2ndsneg(X1, X2)
api(X) -> a2ndspos(mark(X), afrom(0))
api(X) -> pi(X)
aplus(0, Y) -> mark(Y)
aplus(s(X), Y) -> s(aplus(mark(X), mark(Y)))
aplus(X1, X2) -> plus(X1, X2)
atimes(0, Y) -> 0
atimes(s(X), Y) -> aplus(mark(Y), atimes(mark(X), mark(Y)))
atimes(X1, X2) -> times(X1, X2)
asquare(X) -> atimes(mark(X), mark(X))
asquare(X) -> square(X)
mark(from(X)) -> afrom(mark(X))
mark(2ndspos(X1, X2)) -> a2ndspos(mark(X1), mark(X2))
mark(2ndsneg(X1, X2)) -> a2ndsneg(mark(X1), mark(X2))
mark(pi(X)) -> api(mark(X))
mark(plus(X1, X2)) -> aplus(mark(X1), mark(X2))
mark(times(X1, X2)) -> atimes(mark(X1), mark(X2))
mark(square(X)) -> asquare(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(rnil) -> rnil
mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2))


Strategy:

innermost



The Proof could not be continued due to a Timeout.
Innermost Termination of R could not be shown.
Duration:
1:02 minutes