Term Rewriting System R:
[X, Y, X1, X2, X3]
ap(0) -> 0
ap(s(X)) -> mark(X)
ap(X) -> p(X)
aleq(0, Y) -> true
aleq(s(X), 0) -> false
aleq(s(X), s(Y)) -> aleq(mark(X), mark(Y))
aleq(X1, X2) -> leq(X1, X2)
aif(true, X, Y) -> mark(X)
aif(false, X, Y) -> mark(Y)
aif(X1, X2, X3) -> if(X1, X2, X3)
adiff(X, Y) -> aif(aleq(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
adiff(X1, X2) -> diff(X1, X2)
mark(p(X)) -> ap(mark(X))
mark(leq(X1, X2)) -> aleq(mark(X1), mark(X2))
mark(if(X1, X2, X3)) -> aif(mark(X1), X2, X3)
mark(diff(X1, X2)) -> adiff(mark(X1), mark(X2))
mark(0) -> 0
mark(s(X)) -> s(mark(X))
mark(true) -> true
mark(false) -> false

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

AP(s(X)) -> MARK(X)
ALEQ(s(X), s(Y)) -> ALEQ(mark(X), mark(Y))
ALEQ(s(X), s(Y)) -> MARK(X)
ALEQ(s(X), s(Y)) -> MARK(Y)
AIF(true, X, Y) -> MARK(X)
AIF(false, X, Y) -> MARK(Y)
ADIFF(X, Y) -> AIF(aleq(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
ADIFF(X, Y) -> ALEQ(mark(X), mark(Y))
ADIFF(X, Y) -> MARK(X)
ADIFF(X, Y) -> MARK(Y)
MARK(p(X)) -> AP(mark(X))
MARK(p(X)) -> MARK(X)
MARK(leq(X1, X2)) -> ALEQ(mark(X1), mark(X2))
MARK(leq(X1, X2)) -> MARK(X1)
MARK(leq(X1, X2)) -> MARK(X2)
MARK(if(X1, X2, X3)) -> AIF(mark(X1), X2, X3)
MARK(if(X1, X2, X3)) -> MARK(X1)
MARK(diff(X1, X2)) -> ADIFF(mark(X1), mark(X2))
MARK(diff(X1, X2)) -> MARK(X1)
MARK(diff(X1, X2)) -> MARK(X2)
MARK(s(X)) -> MARK(X)

Furthermore, R contains one SCC.


   R
DPs
       →DP Problem 1
Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

ADIFF(X, Y) -> MARK(Y)
ADIFF(X, Y) -> MARK(X)
ALEQ(s(X), s(Y)) -> MARK(Y)
ADIFF(X, Y) -> ALEQ(mark(X), mark(Y))
MARK(s(X)) -> MARK(X)
MARK(diff(X1, X2)) -> MARK(X2)
MARK(diff(X1, X2)) -> MARK(X1)
AIF(false, X, Y) -> MARK(Y)
ADIFF(X, Y) -> AIF(aleq(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
MARK(diff(X1, X2)) -> ADIFF(mark(X1), mark(X2))
MARK(if(X1, X2, X3)) -> MARK(X1)
AIF(true, X, Y) -> MARK(X)
MARK(if(X1, X2, X3)) -> AIF(mark(X1), X2, X3)
MARK(leq(X1, X2)) -> MARK(X2)
MARK(leq(X1, X2)) -> MARK(X1)
ALEQ(s(X), s(Y)) -> MARK(X)
ALEQ(s(X), s(Y)) -> ALEQ(mark(X), mark(Y))
MARK(leq(X1, X2)) -> ALEQ(mark(X1), mark(X2))
MARK(p(X)) -> MARK(X)
MARK(p(X)) -> AP(mark(X))
AP(s(X)) -> MARK(X)


Rules:


ap(0) -> 0
ap(s(X)) -> mark(X)
ap(X) -> p(X)
aleq(0, Y) -> true
aleq(s(X), 0) -> false
aleq(s(X), s(Y)) -> aleq(mark(X), mark(Y))
aleq(X1, X2) -> leq(X1, X2)
aif(true, X, Y) -> mark(X)
aif(false, X, Y) -> mark(Y)
aif(X1, X2, X3) -> if(X1, X2, X3)
adiff(X, Y) -> aif(aleq(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
adiff(X1, X2) -> diff(X1, X2)
mark(p(X)) -> ap(mark(X))
mark(leq(X1, X2)) -> aleq(mark(X1), mark(X2))
mark(if(X1, X2, X3)) -> aif(mark(X1), X2, X3)
mark(diff(X1, X2)) -> adiff(mark(X1), mark(X2))
mark(0) -> 0
mark(s(X)) -> s(mark(X))
mark(true) -> true
mark(false) -> false


Strategy:

innermost



Innermost Termination of R could not be shown.
Duration:
0:34 minutes