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:00 minutes