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`
`         ↳Narrowing Transformation`

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

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

ALEQ(s(X), s(Y)) -> ALEQ(mark(X), mark(Y))
16 new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem:

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳Nar`
`           →DP Problem 2`
`             ↳Narrowing Transformation`

Dependency Pairs:

ALEQ(s(X), s(s(X''))) -> ALEQ(mark(X), s(mark(X'')))
ALEQ(s(X), s(diff(X1', X2'))) -> ALEQ(mark(X), adiff(mark(X1'), mark(X2')))
ALEQ(s(X), s(if(X1', X2', X3'))) -> ALEQ(mark(X), aif(mark(X1'), X2', X3'))
ALEQ(s(X), s(leq(X1', X2'))) -> ALEQ(mark(X), aleq(mark(X1'), mark(X2')))
ALEQ(s(X), s(p(X''))) -> ALEQ(mark(X), ap(mark(X'')))
ALEQ(s(s(X'')), s(Y)) -> ALEQ(s(mark(X'')), mark(Y))
ALEQ(s(diff(X1', X2')), s(Y)) -> ALEQ(adiff(mark(X1'), mark(X2')), mark(Y))
ALEQ(s(if(X1', X2', X3')), s(Y)) -> ALEQ(aif(mark(X1'), X2', X3'), mark(Y))
ALEQ(s(leq(X1', X2')), s(Y)) -> ALEQ(aleq(mark(X1'), mark(X2')), mark(Y))
ALEQ(s(p(X'')), s(Y)) -> ALEQ(ap(mark(X'')), mark(Y))
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)
MARK(leq(X1, X2)) -> ALEQ(mark(X1), mark(X2))
MARK(p(X)) -> MARK(X)
AP(s(X)) -> MARK(X)
MARK(p(X)) -> AP(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)
mark(0) -> 0
mark(s(X)) -> s(mark(X))
mark(true) -> true
mark(false) -> false

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

16 new Dependency Pairs are created:

ADIFF(leq(X1', X2'), Y) -> ALEQ(aleq(mark(X1'), mark(X2')), mark(Y))
ADIFF(if(X1', X2', X3'), Y) -> ALEQ(aif(mark(X1'), X2', X3'), mark(Y))
ADIFF(X, leq(X1', X2')) -> ALEQ(mark(X), aleq(mark(X1'), mark(X2')))
ADIFF(X, if(X1', X2', X3')) -> ALEQ(mark(X), aif(mark(X1'), X2', X3'))

The transformation is resulting in one new DP problem:

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳Nar`
`           →DP Problem 2`
`             ↳Nar`
`             ...`
`               →DP Problem 3`
`                 ↳Narrowing Transformation`

Dependency Pairs:

ADIFF(X, if(X1', X2', X3')) -> ALEQ(mark(X), aif(mark(X1'), X2', X3'))
ADIFF(X, leq(X1', X2')) -> ALEQ(mark(X), aleq(mark(X1'), mark(X2')))
ADIFF(if(X1', X2', X3'), Y) -> ALEQ(aif(mark(X1'), X2', X3'), mark(Y))
ADIFF(leq(X1', X2'), Y) -> ALEQ(aleq(mark(X1'), mark(X2')), mark(Y))
ALEQ(s(X), s(s(X''))) -> ALEQ(mark(X), s(mark(X'')))
ALEQ(s(X), s(diff(X1', X2'))) -> ALEQ(mark(X), adiff(mark(X1'), mark(X2')))
ALEQ(s(X), s(if(X1', X2', X3'))) -> ALEQ(mark(X), aif(mark(X1'), X2', X3'))
ALEQ(s(X), s(leq(X1', X2'))) -> ALEQ(mark(X), aleq(mark(X1'), mark(X2')))
ALEQ(s(X), s(p(X''))) -> ALEQ(mark(X), ap(mark(X'')))
ALEQ(s(s(X'')), s(Y)) -> ALEQ(s(mark(X'')), mark(Y))
ALEQ(s(diff(X1', X2')), s(Y)) -> ALEQ(adiff(mark(X1'), mark(X2')), mark(Y))
ALEQ(s(if(X1', X2', X3')), s(Y)) -> ALEQ(aif(mark(X1'), X2', X3'), mark(Y))
ALEQ(s(leq(X1', X2')), s(Y)) -> ALEQ(aleq(mark(X1'), mark(X2')), mark(Y))
ALEQ(s(p(X'')), s(Y)) -> ALEQ(ap(mark(X'')), mark(Y))
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)
MARK(leq(X1, X2)) -> ALEQ(mark(X1), mark(X2))
MARK(p(X)) -> MARK(X)
AP(s(X)) -> MARK(X)
MARK(p(X)) -> AP(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)
mark(0) -> 0
mark(s(X)) -> s(mark(X))
mark(true) -> true
mark(false) -> false

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

MARK(p(X)) -> AP(mark(X))
eight new Dependency Pairs are created:

MARK(p(p(X''))) -> AP(ap(mark(X'')))
MARK(p(leq(X1', X2'))) -> AP(aleq(mark(X1'), mark(X2')))
MARK(p(if(X1', X2', X3'))) -> AP(aif(mark(X1'), X2', X3'))
MARK(p(0)) -> AP(0)
MARK(p(s(X''))) -> AP(s(mark(X'')))
MARK(p(true)) -> AP(true)
MARK(p(false)) -> AP(false)

The transformation is resulting in one new DP problem:

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳Nar`
`           →DP Problem 2`
`             ↳Nar`
`             ...`
`               →DP Problem 4`
`                 ↳Narrowing Transformation`

Dependency Pairs:

ADIFF(X, if(X1', X2', X3')) -> ALEQ(mark(X), aif(mark(X1'), X2', X3'))
ADIFF(X, leq(X1', X2')) -> ALEQ(mark(X), aleq(mark(X1'), mark(X2')))
ADIFF(if(X1', X2', X3'), Y) -> ALEQ(aif(mark(X1'), X2', X3'), mark(Y))
ADIFF(leq(X1', X2'), Y) -> ALEQ(aleq(mark(X1'), mark(X2')), mark(Y))
ALEQ(s(X), s(s(X''))) -> ALEQ(mark(X), s(mark(X'')))
ALEQ(s(X), s(diff(X1', X2'))) -> ALEQ(mark(X), adiff(mark(X1'), mark(X2')))
ALEQ(s(X), s(if(X1', X2', X3'))) -> ALEQ(mark(X), aif(mark(X1'), X2', X3'))
ALEQ(s(X), s(leq(X1', X2'))) -> ALEQ(mark(X), aleq(mark(X1'), mark(X2')))
ALEQ(s(X), s(p(X''))) -> ALEQ(mark(X), ap(mark(X'')))
ALEQ(s(s(X'')), s(Y)) -> ALEQ(s(mark(X'')), mark(Y))
ALEQ(s(diff(X1', X2')), s(Y)) -> ALEQ(adiff(mark(X1'), mark(X2')), mark(Y))
ALEQ(s(if(X1', X2', X3')), s(Y)) -> ALEQ(aif(mark(X1'), X2', X3'), mark(Y))
ALEQ(s(leq(X1', X2')), s(Y)) -> ALEQ(aleq(mark(X1'), mark(X2')), mark(Y))
ALEQ(s(p(X'')), s(Y)) -> ALEQ(ap(mark(X'')), mark(Y))
MARK(p(s(X''))) -> AP(s(mark(X'')))
MARK(p(if(X1', X2', X3'))) -> AP(aif(mark(X1'), X2', X3'))
MARK(p(leq(X1', X2'))) -> AP(aleq(mark(X1'), mark(X2')))
AP(s(X)) -> MARK(X)
MARK(p(p(X''))) -> AP(ap(mark(X'')))
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(Y)
MARK(leq(X1, X2)) -> ALEQ(mark(X1), mark(X2))
MARK(p(X)) -> MARK(X)
ALEQ(s(X), s(Y)) -> 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)
mark(0) -> 0
mark(s(X)) -> s(mark(X))
mark(true) -> true
mark(false) -> false

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

MARK(leq(X1, X2)) -> ALEQ(mark(X1), mark(X2))
16 new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem:

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳Nar`
`           →DP Problem 2`
`             ↳Nar`
`             ...`
`               →DP Problem 5`
`                 ↳Narrowing Transformation`

Dependency Pairs:

ADIFF(X, if(X1', X2', X3')) -> ALEQ(mark(X), aif(mark(X1'), X2', X3'))
ADIFF(X, leq(X1', X2')) -> ALEQ(mark(X), aleq(mark(X1'), mark(X2')))
ADIFF(if(X1', X2', X3'), Y) -> ALEQ(aif(mark(X1'), X2', X3'), mark(Y))
ADIFF(leq(X1', X2'), Y) -> ALEQ(aleq(mark(X1'), mark(X2')), mark(Y))
MARK(leq(X1, s(X'))) -> ALEQ(mark(X1), s(mark(X')))
MARK(leq(X1, diff(X1'', X2''))) -> ALEQ(mark(X1), adiff(mark(X1''), mark(X2'')))
MARK(leq(X1, if(X1'', X2'', X3'))) -> ALEQ(mark(X1), aif(mark(X1''), X2'', X3'))
MARK(leq(X1, leq(X1'', X2''))) -> ALEQ(mark(X1), aleq(mark(X1''), mark(X2'')))
MARK(leq(X1, p(X'))) -> ALEQ(mark(X1), ap(mark(X')))
MARK(leq(s(X'), X2)) -> ALEQ(s(mark(X')), mark(X2))
MARK(leq(diff(X1'', X2''), X2)) -> ALEQ(adiff(mark(X1''), mark(X2'')), mark(X2))
MARK(leq(if(X1'', X2'', X3'), X2)) -> ALEQ(aif(mark(X1''), X2'', X3'), mark(X2))
ALEQ(s(X), s(s(X''))) -> ALEQ(mark(X), s(mark(X'')))
ALEQ(s(X), s(diff(X1', X2'))) -> ALEQ(mark(X), adiff(mark(X1'), mark(X2')))
ALEQ(s(X), s(if(X1', X2', X3'))) -> ALEQ(mark(X), aif(mark(X1'), X2', X3'))
ALEQ(s(X), s(leq(X1', X2'))) -> ALEQ(mark(X), aleq(mark(X1'), mark(X2')))
ALEQ(s(X), s(p(X''))) -> ALEQ(mark(X), ap(mark(X'')))
ALEQ(s(s(X'')), s(Y)) -> ALEQ(s(mark(X'')), mark(Y))
ALEQ(s(diff(X1', X2')), s(Y)) -> ALEQ(adiff(mark(X1'), mark(X2')), mark(Y))
ALEQ(s(if(X1', X2', X3')), s(Y)) -> ALEQ(aif(mark(X1'), X2', X3'), mark(Y))
ALEQ(s(leq(X1', X2')), s(Y)) -> ALEQ(aleq(mark(X1'), mark(X2')), mark(Y))
ALEQ(s(p(X'')), s(Y)) -> ALEQ(ap(mark(X'')), mark(Y))
MARK(leq(leq(X1'', X2''), X2)) -> ALEQ(aleq(mark(X1''), mark(X2'')), mark(X2))
ALEQ(s(X), s(Y)) -> MARK(Y)
MARK(leq(p(X'), X2)) -> ALEQ(ap(mark(X')), mark(X2))
MARK(p(s(X''))) -> AP(s(mark(X'')))
MARK(p(if(X1', X2', X3'))) -> AP(aif(mark(X1'), X2', X3'))
MARK(p(leq(X1', X2'))) -> AP(aleq(mark(X1'), mark(X2')))
AP(s(X)) -> MARK(X)
MARK(p(p(X''))) -> AP(ap(mark(X'')))
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)
MARK(p(X)) -> MARK(X)
ALEQ(s(X), s(Y)) -> 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)
mark(0) -> 0
mark(s(X)) -> s(mark(X))
mark(true) -> true
mark(false) -> false

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

MARK(if(X1, X2, X3)) -> AIF(mark(X1), X2, X3)
eight new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem:

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳Nar`
`           →DP Problem 2`
`             ↳Nar`
`             ...`
`               →DP Problem 6`
`                 ↳Negative Polynomial Order`

Dependency Pairs:

ADIFF(X, if(X1', X2', X3')) -> ALEQ(mark(X), aif(mark(X1'), X2', X3'))
ADIFF(X, leq(X1', X2')) -> ALEQ(mark(X), aleq(mark(X1'), mark(X2')))
ADIFF(if(X1', X2', X3'), Y) -> ALEQ(aif(mark(X1'), X2', X3'), mark(Y))
ADIFF(leq(X1', X2'), Y) -> ALEQ(aleq(mark(X1'), mark(X2')), mark(Y))
MARK(if(false, X2, X3)) -> AIF(false, X2, X3)
MARK(if(true, X2, X3)) -> AIF(true, X2, X3)
MARK(if(diff(X1'', X2''), X2, X3)) -> AIF(adiff(mark(X1''), mark(X2'')), X2, X3)
MARK(if(if(X1'', X2'', X3''), X2, X3)) -> AIF(aif(mark(X1''), X2'', X3''), X2, X3)
MARK(if(leq(X1'', X2''), X2, X3)) -> AIF(aleq(mark(X1''), mark(X2'')), X2, X3)
AIF(false, X, Y) -> MARK(Y)
MARK(if(p(X'), X2, X3)) -> AIF(ap(mark(X')), X2, X3)
MARK(leq(X1, s(X'))) -> ALEQ(mark(X1), s(mark(X')))
MARK(leq(X1, diff(X1'', X2''))) -> ALEQ(mark(X1), adiff(mark(X1''), mark(X2'')))
MARK(leq(X1, if(X1'', X2'', X3'))) -> ALEQ(mark(X1), aif(mark(X1''), X2'', X3'))
MARK(leq(X1, leq(X1'', X2''))) -> ALEQ(mark(X1), aleq(mark(X1''), mark(X2'')))
MARK(leq(X1, p(X'))) -> ALEQ(mark(X1), ap(mark(X')))
MARK(leq(s(X'), X2)) -> ALEQ(s(mark(X')), mark(X2))
MARK(leq(diff(X1'', X2''), X2)) -> ALEQ(adiff(mark(X1''), mark(X2'')), mark(X2))
MARK(leq(if(X1'', X2'', X3'), X2)) -> ALEQ(aif(mark(X1''), X2'', X3'), mark(X2))
ALEQ(s(X), s(s(X''))) -> ALEQ(mark(X), s(mark(X'')))
ALEQ(s(X), s(diff(X1', X2'))) -> ALEQ(mark(X), adiff(mark(X1'), mark(X2')))
ALEQ(s(X), s(if(X1', X2', X3'))) -> ALEQ(mark(X), aif(mark(X1'), X2', X3'))
ALEQ(s(X), s(leq(X1', X2'))) -> ALEQ(mark(X), aleq(mark(X1'), mark(X2')))
ALEQ(s(X), s(p(X''))) -> ALEQ(mark(X), ap(mark(X'')))
ALEQ(s(s(X'')), s(Y)) -> ALEQ(s(mark(X'')), mark(Y))
ALEQ(s(diff(X1', X2')), s(Y)) -> ALEQ(adiff(mark(X1'), mark(X2')), mark(Y))
ALEQ(s(if(X1', X2', X3')), s(Y)) -> ALEQ(aif(mark(X1'), X2', X3'), mark(Y))
ALEQ(s(leq(X1', X2')), s(Y)) -> ALEQ(aleq(mark(X1'), mark(X2')), mark(Y))
ALEQ(s(p(X'')), s(Y)) -> ALEQ(ap(mark(X'')), mark(Y))
MARK(leq(leq(X1'', X2''), X2)) -> ALEQ(aleq(mark(X1''), mark(X2'')), mark(X2))
ALEQ(s(X), s(Y)) -> MARK(Y)
MARK(leq(p(X'), X2)) -> ALEQ(ap(mark(X')), mark(X2))
MARK(p(s(X''))) -> AP(s(mark(X'')))
MARK(p(if(X1', X2', X3'))) -> AP(aif(mark(X1'), X2', X3'))
MARK(p(leq(X1', X2'))) -> AP(aleq(mark(X1'), mark(X2')))
AP(s(X)) -> MARK(X)
MARK(p(p(X''))) -> AP(ap(mark(X'')))
MARK(s(X)) -> MARK(X)
MARK(diff(X1, X2)) -> MARK(X2)
MARK(diff(X1, X2)) -> MARK(X1)
AIF(true, X, Y) -> MARK(X)
ADIFF(X, Y) -> AIF(aleq(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
MARK(if(X1, X2, X3)) -> MARK(X1)
MARK(leq(X1, X2)) -> MARK(X2)
MARK(leq(X1, X2)) -> MARK(X1)
MARK(p(X)) -> MARK(X)
ALEQ(s(X), s(Y)) -> 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)
mark(0) -> 0
mark(s(X)) -> s(mark(X))
mark(true) -> true
mark(false) -> false

The following Dependency Pairs can be strictly oriented using the given order.

ADIFF(X, leq(X1', X2')) -> ALEQ(mark(X), aleq(mark(X1'), mark(X2')))
MARK(leq(X1, leq(X1'', X2''))) -> ALEQ(mark(X1), aleq(mark(X1''), mark(X2'')))
ALEQ(s(X), s(leq(X1', X2'))) -> ALEQ(mark(X), aleq(mark(X1'), mark(X2')))

Moreover, the following usable rules (regarding the implicit AFS) are oriented.

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
adiff(X, Y) -> aif(aleq(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
aif(true, X, Y) -> mark(X)
aif(false, X, Y) -> mark(Y)
aif(X1, X2, X3) -> if(X1, X2, X3)
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)
ap(0) -> 0
ap(s(X)) -> mark(X)
ap(X) -> p(X)

Used ordering:
Polynomial Order with Interpretation:

POL( ADIFF(x1, x2) ) = 1

POL( ALEQ(x1, x2) ) = x2

POL( aleq(x1, x2) ) = 0

POL( MARK(x1) ) = 1

POL( mark(x1) ) = 1

POL( ap(x1) ) = 1

POL( s(x1) ) = 1

POL( adiff(x1, x2) ) = 1

POL( AIF(x1, ..., x3) ) = 1

POL( AP(x1) ) = 1

POL( aif(x1, ..., x3) ) = 1

POL( 0 ) = 0

POL( true ) = 0

POL( false ) = 0

POL( diff(x1, x2) ) = 0

POL( if(x1, ..., x3) ) = 0

POL( leq(x1, x2) ) = 0

POL( p(x1) ) = 0

This results in one new DP problem.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳Nar`
`           →DP Problem 2`
`             ↳Nar`
`             ...`
`               →DP Problem 7`
`                 ↳Remaining Obligation(s)`

The following remains to be proven:
Dependency Pairs:

ADIFF(X, if(X1', X2', X3')) -> ALEQ(mark(X), aif(mark(X1'), X2', X3'))
ADIFF(if(X1', X2', X3'), Y) -> ALEQ(aif(mark(X1'), X2', X3'), mark(Y))
ADIFF(leq(X1', X2'), Y) -> ALEQ(aleq(mark(X1'), mark(X2')), mark(Y))
MARK(if(false, X2, X3)) -> AIF(false, X2, X3)
MARK(if(true, X2, X3)) -> AIF(true, X2, X3)
MARK(if(diff(X1'', X2''), X2, X3)) -> AIF(adiff(mark(X1''), mark(X2'')), X2, X3)
MARK(if(if(X1'', X2'', X3''), X2, X3)) -> AIF(aif(mark(X1''), X2'', X3''), X2, X3)
MARK(if(leq(X1'', X2''), X2, X3)) -> AIF(aleq(mark(X1''), mark(X2'')), X2, X3)
AIF(false, X, Y) -> MARK(Y)
MARK(if(p(X'), X2, X3)) -> AIF(ap(mark(X')), X2, X3)
MARK(leq(X1, s(X'))) -> ALEQ(mark(X1), s(mark(X')))
MARK(leq(X1, diff(X1'', X2''))) -> ALEQ(mark(X1), adiff(mark(X1''), mark(X2'')))
MARK(leq(X1, if(X1'', X2'', X3'))) -> ALEQ(mark(X1), aif(mark(X1''), X2'', X3'))
MARK(leq(X1, p(X'))) -> ALEQ(mark(X1), ap(mark(X')))
MARK(leq(s(X'), X2)) -> ALEQ(s(mark(X')), mark(X2))
MARK(leq(diff(X1'', X2''), X2)) -> ALEQ(adiff(mark(X1''), mark(X2'')), mark(X2))
MARK(leq(if(X1'', X2'', X3'), X2)) -> ALEQ(aif(mark(X1''), X2'', X3'), mark(X2))
ALEQ(s(X), s(s(X''))) -> ALEQ(mark(X), s(mark(X'')))
ALEQ(s(X), s(diff(X1', X2'))) -> ALEQ(mark(X), adiff(mark(X1'), mark(X2')))
ALEQ(s(X), s(if(X1', X2', X3'))) -> ALEQ(mark(X), aif(mark(X1'), X2', X3'))
ALEQ(s(X), s(p(X''))) -> ALEQ(mark(X), ap(mark(X'')))
ALEQ(s(s(X'')), s(Y)) -> ALEQ(s(mark(X'')), mark(Y))
ALEQ(s(diff(X1', X2')), s(Y)) -> ALEQ(adiff(mark(X1'), mark(X2')), mark(Y))
ALEQ(s(if(X1', X2', X3')), s(Y)) -> ALEQ(aif(mark(X1'), X2', X3'), mark(Y))
ALEQ(s(leq(X1', X2')), s(Y)) -> ALEQ(aleq(mark(X1'), mark(X2')), mark(Y))
ALEQ(s(p(X'')), s(Y)) -> ALEQ(ap(mark(X'')), mark(Y))
MARK(leq(leq(X1'', X2''), X2)) -> ALEQ(aleq(mark(X1''), mark(X2'')), mark(X2))
ALEQ(s(X), s(Y)) -> MARK(Y)
MARK(leq(p(X'), X2)) -> ALEQ(ap(mark(X')), mark(X2))
MARK(p(s(X''))) -> AP(s(mark(X'')))
MARK(p(if(X1', X2', X3'))) -> AP(aif(mark(X1'), X2', X3'))
MARK(p(leq(X1', X2'))) -> AP(aleq(mark(X1'), mark(X2')))
AP(s(X)) -> MARK(X)
MARK(p(p(X''))) -> AP(ap(mark(X'')))
MARK(s(X)) -> MARK(X)
MARK(diff(X1, X2)) -> MARK(X2)
MARK(diff(X1, X2)) -> MARK(X1)
AIF(true, X, Y) -> MARK(X)
ADIFF(X, Y) -> AIF(aleq(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
MARK(if(X1, X2, X3)) -> MARK(X1)
MARK(leq(X1, X2)) -> MARK(X2)
MARK(leq(X1, X2)) -> MARK(X1)
MARK(p(X)) -> MARK(X)
ALEQ(s(X), s(Y)) -> 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)