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)))
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(0) -> 0
mark(s(X)) -> s(mark(X))
mark(true) -> true
mark(false) -> false

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

ALEQ(s(X), s(Y)) -> 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(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)))
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)