Termination Proof using AProVE

Term Rewriting System R:
[X, Y, X1, X2, X3]
a_{_p}(0) -> 0
a_{_p}(s(X)) -> mark(X)
a_{_p}(X) -> p(X)
a_{_leq}(0, Y) -> true
a_{_leq}(s(X), 0) -> false
a_{_leq}(s(X), s(Y)) -> a_{_leq}(mark(X), mark(Y))
a_{_leq}(X1, X2) -> leq(X1, X2)
a_{_if}(true, X, Y) -> mark(X)
a_{_if}(false, X, Y) -> mark(Y)
a_{_if}(X1, X2, X3) -> if(X1, X2, X3)
a_{_diff}(X, Y) -> a_{_if}(a_{_leq}(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
a_{_diff}(X1, X2) -> diff(X1, X2)
mark(p(X)) -> a_{_p}(mark(X))
mark(leq(X1, X2)) -> a_{_leq}(mark(X1), mark(X2))
mark(if(X1, X2, X3)) -> a_{_if}(mark(X1), X2, X3)
mark(diff(X1, X2)) -> a_{_diff}(mark(X1), mark(X2))
mark(0) -> 0
mark(s(X)) -> s(mark(X))
mark(true) -> true
mark(false) -> false

Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

A_{_P}(s(X)) -> MARK(X)
A_{_LEQ}(s(X), s(Y)) -> A_{_LEQ}(mark(X), mark(Y))
A_{_LEQ}(s(X), s(Y)) -> MARK(X)
A_{_LEQ}(s(X), s(Y)) -> MARK(Y)
A_{_IF}(true, X, Y) -> MARK(X)
A_{_IF}(false, X, Y) -> MARK(Y)
A_{_DIFF}(X, Y) -> A_{_IF}(a_{_leq}(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
A_{_DIFF}(X, Y) -> A_{_LEQ}(mark(X), mark(Y))
A_{_DIFF}(X, Y) -> MARK(X)
A_{_DIFF}(X, Y) -> MARK(Y)
MARK(p(X)) -> A_{_P}(mark(X))
MARK(p(X)) -> MARK(X)
MARK(leq(X1, X2)) -> A_{_LEQ}(mark(X1), mark(X2))
MARK(leq(X1, X2)) -> MARK(X1)
MARK(leq(X1, X2)) -> MARK(X2)
MARK(if(X1, X2, X3)) -> A_{_IF}(mark(X1), X2, X3)
MARK(if(X1, X2, X3)) -> MARK(X1)
MARK(diff(X1, X2)) -> A_{_DIFF}(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.

     ↳DPs

       →DP Problem 1

         ↳Narrowing Transformation

Dependency Pairs:

A_{_DIFF}(X, Y) -> MARK(Y)
A_{_DIFF}(X, Y) -> MARK(X)
A_{_LEQ}(s(X), s(Y)) -> MARK(Y)
A_{_DIFF}(X, Y) -> A_{_LEQ}(mark(X), mark(Y))
MARK(s(X)) -> MARK(X)
MARK(diff(X1, X2)) -> MARK(X2)
MARK(diff(X1, X2)) -> MARK(X1)
A_{_IF}(false, X, Y) -> MARK(Y)
A_{_DIFF}(X, Y) -> A_{_IF}(a_{_leq}(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
MARK(diff(X1, X2)) -> A_{_DIFF}(mark(X1), mark(X2))
MARK(if(X1, X2, X3)) -> MARK(X1)
A_{_IF}(true, X, Y) -> MARK(X)
MARK(if(X1, X2, X3)) -> A_{_IF}(mark(X1), X2, X3)
MARK(leq(X1, X2)) -> MARK(X2)
MARK(leq(X1, X2)) -> MARK(X1)
A_{_LEQ}(s(X), s(Y)) -> MARK(X)
A_{_LEQ}(s(X), s(Y)) -> A_{_LEQ}(mark(X), mark(Y))
MARK(leq(X1, X2)) -> A_{_LEQ}(mark(X1), mark(X2))
MARK(p(X)) -> MARK(X)
MARK(p(X)) -> A_{_P}(mark(X))
A_{_P}(s(X)) -> MARK(X)

Rules:

a_{_p}(0) -> 0
a_{_p}(s(X)) -> mark(X)
a_{_p}(X) -> p(X)
a_{_leq}(0, Y) -> true
a_{_leq}(s(X), 0) -> false
a_{_leq}(s(X), s(Y)) -> a_{_leq}(mark(X), mark(Y))
a_{_leq}(X1, X2) -> leq(X1, X2)
a_{_if}(true, X, Y) -> mark(X)
a_{_if}(false, X, Y) -> mark(Y)
a_{_if}(X1, X2, X3) -> if(X1, X2, X3)
a_{_diff}(X, Y) -> a_{_if}(a_{_leq}(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
a_{_diff}(X1, X2) -> diff(X1, X2)
mark(p(X)) -> a_{_p}(mark(X))
mark(leq(X1, X2)) -> a_{_leq}(mark(X1), mark(X2))
mark(if(X1, X2, X3)) -> a_{_if}(mark(X1), X2, X3)
mark(diff(X1, X2)) -> a_{_diff}(mark(X1), mark(X2))
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

A_{_LEQ}(s(X), s(Y)) -> A_{_LEQ}(mark(X), mark(Y))

16 new Dependency Pairs are created:

A_{_LEQ}(s(p(X'')), s(Y)) -> A_{_LEQ}(a_{_p}(mark(X'')), mark(Y))
A_{_LEQ}(s(leq(X1', X2')), s(Y)) -> A_{_LEQ}(a_{_leq}(mark(X1'), mark(X2')), mark(Y))
A_{_LEQ}(s(if(X1', X2', X3')), s(Y)) -> A_{_LEQ}(a_{_if}(mark(X1'), X2', X3'), mark(Y))
A_{_LEQ}(s(diff(X1', X2')), s(Y)) -> A_{_LEQ}(a_{_diff}(mark(X1'), mark(X2')), mark(Y))
A_{_LEQ}(s(0), s(Y)) -> A_{_LEQ}(0, mark(Y))
A_{_LEQ}(s(s(X'')), s(Y)) -> A_{_LEQ}(s(mark(X'')), mark(Y))
A_{_LEQ}(s(true), s(Y)) -> A_{_LEQ}(true, mark(Y))
A_{_LEQ}(s(false), s(Y)) -> A_{_LEQ}(false, mark(Y))
A_{_LEQ}(s(X), s(p(X''))) -> A_{_LEQ}(mark(X), a_{_p}(mark(X'')))
A_{_LEQ}(s(X), s(leq(X1', X2'))) -> A_{_LEQ}(mark(X), a_{_leq}(mark(X1'), mark(X2')))
A_{_LEQ}(s(X), s(if(X1', X2', X3'))) -> A_{_LEQ}(mark(X), a_{_if}(mark(X1'), X2', X3'))
A_{_LEQ}(s(X), s(diff(X1', X2'))) -> A_{_LEQ}(mark(X), a_{_diff}(mark(X1'), mark(X2')))
A_{_LEQ}(s(X), s(0)) -> A_{_LEQ}(mark(X), 0)
A_{_LEQ}(s(X), s(s(X''))) -> A_{_LEQ}(mark(X), s(mark(X'')))
A_{_LEQ}(s(X), s(true)) -> A_{_LEQ}(mark(X), true)
A_{_LEQ}(s(X), s(false)) -> A_{_LEQ}(mark(X), false)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Narrowing Transformation

Dependency Pairs:

A_{_DIFF}(X, Y) -> MARK(X)
A_{_LEQ}(s(X), s(s(X''))) -> A_{_LEQ}(mark(X), s(mark(X'')))
A_{_LEQ}(s(X), s(diff(X1', X2'))) -> A_{_LEQ}(mark(X), a_{_diff}(mark(X1'), mark(X2')))
A_{_LEQ}(s(X), s(if(X1', X2', X3'))) -> A_{_LEQ}(mark(X), a_{_if}(mark(X1'), X2', X3'))
A_{_LEQ}(s(X), s(leq(X1', X2'))) -> A_{_LEQ}(mark(X), a_{_leq}(mark(X1'), mark(X2')))
A_{_LEQ}(s(X), s(p(X''))) -> A_{_LEQ}(mark(X), a_{_p}(mark(X'')))
A_{_LEQ}(s(s(X'')), s(Y)) -> A_{_LEQ}(s(mark(X'')), mark(Y))
A_{_LEQ}(s(diff(X1', X2')), s(Y)) -> A_{_LEQ}(a_{_diff}(mark(X1'), mark(X2')), mark(Y))
A_{_LEQ}(s(if(X1', X2', X3')), s(Y)) -> A_{_LEQ}(a_{_if}(mark(X1'), X2', X3'), mark(Y))
A_{_LEQ}(s(leq(X1', X2')), s(Y)) -> A_{_LEQ}(a_{_leq}(mark(X1'), mark(X2')), mark(Y))
A_{_LEQ}(s(p(X'')), s(Y)) -> A_{_LEQ}(a_{_p}(mark(X'')), mark(Y))
A_{_LEQ}(s(X), s(Y)) -> MARK(Y)
A_{_DIFF}(X, Y) -> A_{_LEQ}(mark(X), mark(Y))
MARK(s(X)) -> MARK(X)
MARK(diff(X1, X2)) -> MARK(X2)
MARK(diff(X1, X2)) -> MARK(X1)
A_{_IF}(false, X, Y) -> MARK(Y)
A_{_DIFF}(X, Y) -> A_{_IF}(a_{_leq}(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
MARK(diff(X1, X2)) -> A_{_DIFF}(mark(X1), mark(X2))
MARK(if(X1, X2, X3)) -> MARK(X1)
A_{_IF}(true, X, Y) -> MARK(X)
MARK(if(X1, X2, X3)) -> A_{_IF}(mark(X1), X2, X3)
MARK(leq(X1, X2)) -> MARK(X2)
MARK(leq(X1, X2)) -> MARK(X1)
A_{_LEQ}(s(X), s(Y)) -> MARK(X)
MARK(leq(X1, X2)) -> A_{_LEQ}(mark(X1), mark(X2))
MARK(p(X)) -> MARK(X)
A_{_P}(s(X)) -> MARK(X)
MARK(p(X)) -> A_{_P}(mark(X))
A_{_DIFF}(X, Y) -> MARK(Y)

Rules:

a_{_p}(0) -> 0
a_{_p}(s(X)) -> mark(X)
a_{_p}(X) -> p(X)
a_{_leq}(0, Y) -> true
a_{_leq}(s(X), 0) -> false
a_{_leq}(s(X), s(Y)) -> a_{_leq}(mark(X), mark(Y))
a_{_leq}(X1, X2) -> leq(X1, X2)
a_{_if}(true, X, Y) -> mark(X)
a_{_if}(false, X, Y) -> mark(Y)
a_{_if}(X1, X2, X3) -> if(X1, X2, X3)
a_{_diff}(X, Y) -> a_{_if}(a_{_leq}(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
a_{_diff}(X1, X2) -> diff(X1, X2)
mark(p(X)) -> a_{_p}(mark(X))
mark(leq(X1, X2)) -> a_{_leq}(mark(X1), mark(X2))
mark(if(X1, X2, X3)) -> a_{_if}(mark(X1), X2, X3)
mark(diff(X1, X2)) -> a_{_diff}(mark(X1), mark(X2))
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

A_{_DIFF}(X, Y) -> A_{_LEQ}(mark(X), mark(Y))

16 new Dependency Pairs are created:

A_{_DIFF}(p(X''), Y) -> A_{_LEQ}(a_{_p}(mark(X'')), mark(Y))
A_{_DIFF}(leq(X1', X2'), Y) -> A_{_LEQ}(a_{_leq}(mark(X1'), mark(X2')), mark(Y))
A_{_DIFF}(if(X1', X2', X3'), Y) -> A_{_LEQ}(a_{_if}(mark(X1'), X2', X3'), mark(Y))
A_{_DIFF}(diff(X1', X2'), Y) -> A_{_LEQ}(a_{_diff}(mark(X1'), mark(X2')), mark(Y))
A_{_DIFF}(0, Y) -> A_{_LEQ}(0, mark(Y))
A_{_DIFF}(s(X''), Y) -> A_{_LEQ}(s(mark(X'')), mark(Y))
A_{_DIFF}(true, Y) -> A_{_LEQ}(true, mark(Y))
A_{_DIFF}(false, Y) -> A_{_LEQ}(false, mark(Y))
A_{_DIFF}(X, p(X'')) -> A_{_LEQ}(mark(X), a_{_p}(mark(X'')))
A_{_DIFF}(X, leq(X1', X2')) -> A_{_LEQ}(mark(X), a_{_leq}(mark(X1'), mark(X2')))
A_{_DIFF}(X, if(X1', X2', X3')) -> A_{_LEQ}(mark(X), a_{_if}(mark(X1'), X2', X3'))
A_{_DIFF}(X, diff(X1', X2')) -> A_{_LEQ}(mark(X), a_{_diff}(mark(X1'), mark(X2')))
A_{_DIFF}(X, 0) -> A_{_LEQ}(mark(X), 0)
A_{_DIFF}(X, s(X'')) -> A_{_LEQ}(mark(X), s(mark(X'')))
A_{_DIFF}(X, true) -> A_{_LEQ}(mark(X), true)
A_{_DIFF}(X, false) -> A_{_LEQ}(mark(X), false)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 3

                 ↳Narrowing Transformation

Dependency Pairs:

A_{_DIFF}(X, s(X'')) -> A_{_LEQ}(mark(X), s(mark(X'')))
A_{_DIFF}(X, diff(X1', X2')) -> A_{_LEQ}(mark(X), a_{_diff}(mark(X1'), mark(X2')))
A_{_DIFF}(X, if(X1', X2', X3')) -> A_{_LEQ}(mark(X), a_{_if}(mark(X1'), X2', X3'))
A_{_DIFF}(X, leq(X1', X2')) -> A_{_LEQ}(mark(X), a_{_leq}(mark(X1'), mark(X2')))
A_{_DIFF}(X, p(X'')) -> A_{_LEQ}(mark(X), a_{_p}(mark(X'')))
A_{_DIFF}(s(X''), Y) -> A_{_LEQ}(s(mark(X'')), mark(Y))
A_{_DIFF}(diff(X1', X2'), Y) -> A_{_LEQ}(a_{_diff}(mark(X1'), mark(X2')), mark(Y))
A_{_DIFF}(if(X1', X2', X3'), Y) -> A_{_LEQ}(a_{_if}(mark(X1'), X2', X3'), mark(Y))
A_{_DIFF}(leq(X1', X2'), Y) -> A_{_LEQ}(a_{_leq}(mark(X1'), mark(X2')), mark(Y))
A_{_LEQ}(s(X), s(s(X''))) -> A_{_LEQ}(mark(X), s(mark(X'')))
A_{_LEQ}(s(X), s(diff(X1', X2'))) -> A_{_LEQ}(mark(X), a_{_diff}(mark(X1'), mark(X2')))
A_{_LEQ}(s(X), s(if(X1', X2', X3'))) -> A_{_LEQ}(mark(X), a_{_if}(mark(X1'), X2', X3'))
A_{_LEQ}(s(X), s(leq(X1', X2'))) -> A_{_LEQ}(mark(X), a_{_leq}(mark(X1'), mark(X2')))
A_{_LEQ}(s(X), s(p(X''))) -> A_{_LEQ}(mark(X), a_{_p}(mark(X'')))
A_{_LEQ}(s(s(X'')), s(Y)) -> A_{_LEQ}(s(mark(X'')), mark(Y))
A_{_LEQ}(s(diff(X1', X2')), s(Y)) -> A_{_LEQ}(a_{_diff}(mark(X1'), mark(X2')), mark(Y))
A_{_LEQ}(s(if(X1', X2', X3')), s(Y)) -> A_{_LEQ}(a_{_if}(mark(X1'), X2', X3'), mark(Y))
A_{_LEQ}(s(leq(X1', X2')), s(Y)) -> A_{_LEQ}(a_{_leq}(mark(X1'), mark(X2')), mark(Y))
A_{_LEQ}(s(p(X'')), s(Y)) -> A_{_LEQ}(a_{_p}(mark(X'')), mark(Y))
A_{_LEQ}(s(X), s(Y)) -> MARK(Y)
A_{_DIFF}(p(X''), Y) -> A_{_LEQ}(a_{_p}(mark(X'')), mark(Y))
A_{_DIFF}(X, Y) -> MARK(Y)
MARK(s(X)) -> MARK(X)
MARK(diff(X1, X2)) -> MARK(X2)
MARK(diff(X1, X2)) -> MARK(X1)
A_{_IF}(false, X, Y) -> MARK(Y)
A_{_DIFF}(X, Y) -> A_{_IF}(a_{_leq}(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
MARK(diff(X1, X2)) -> A_{_DIFF}(mark(X1), mark(X2))
MARK(if(X1, X2, X3)) -> MARK(X1)
A_{_IF}(true, X, Y) -> MARK(X)
MARK(if(X1, X2, X3)) -> A_{_IF}(mark(X1), X2, X3)
MARK(leq(X1, X2)) -> MARK(X2)
MARK(leq(X1, X2)) -> MARK(X1)
A_{_LEQ}(s(X), s(Y)) -> MARK(X)
MARK(leq(X1, X2)) -> A_{_LEQ}(mark(X1), mark(X2))
MARK(p(X)) -> MARK(X)
A_{_P}(s(X)) -> MARK(X)
MARK(p(X)) -> A_{_P}(mark(X))
A_{_DIFF}(X, Y) -> MARK(X)

Rules:

a_{_p}(0) -> 0
a_{_p}(s(X)) -> mark(X)
a_{_p}(X) -> p(X)
a_{_leq}(0, Y) -> true
a_{_leq}(s(X), 0) -> false
a_{_leq}(s(X), s(Y)) -> a_{_leq}(mark(X), mark(Y))
a_{_leq}(X1, X2) -> leq(X1, X2)
a_{_if}(true, X, Y) -> mark(X)
a_{_if}(false, X, Y) -> mark(Y)
a_{_if}(X1, X2, X3) -> if(X1, X2, X3)
a_{_diff}(X, Y) -> a_{_if}(a_{_leq}(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
a_{_diff}(X1, X2) -> diff(X1, X2)
mark(p(X)) -> a_{_p}(mark(X))
mark(leq(X1, X2)) -> a_{_leq}(mark(X1), mark(X2))
mark(if(X1, X2, X3)) -> a_{_if}(mark(X1), X2, X3)
mark(diff(X1, X2)) -> a_{_diff}(mark(X1), mark(X2))
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)) -> A_{_P}(mark(X))

eight new Dependency Pairs are created:

MARK(p(p(X''))) -> A_{_P}(a_{_p}(mark(X'')))
MARK(p(leq(X1', X2'))) -> A_{_P}(a_{_leq}(mark(X1'), mark(X2')))
MARK(p(if(X1', X2', X3'))) -> A_{_P}(a_{_if}(mark(X1'), X2', X3'))
MARK(p(diff(X1', X2'))) -> A_{_P}(a_{_diff}(mark(X1'), mark(X2')))
MARK(p(0)) -> A_{_P}(0)
MARK(p(s(X''))) -> A_{_P}(s(mark(X'')))
MARK(p(true)) -> A_{_P}(true)
MARK(p(false)) -> A_{_P}(false)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 4

                 ↳Narrowing Transformation

Dependency Pairs:

Rules:

a_{_p}(0) -> 0
a_{_p}(s(X)) -> mark(X)
a_{_p}(X) -> p(X)
a_{_leq}(0, Y) -> true
a_{_leq}(s(X), 0) -> false
a_{_leq}(s(X), s(Y)) -> a_{_leq}(mark(X), mark(Y))
a_{_leq}(X1, X2) -> leq(X1, X2)
a_{_if}(true, X, Y) -> mark(X)
a_{_if}(false, X, Y) -> mark(Y)
a_{_if}(X1, X2, X3) -> if(X1, X2, X3)
a_{_diff}(X, Y) -> a_{_if}(a_{_leq}(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
a_{_diff}(X1, X2) -> diff(X1, X2)
mark(p(X)) -> a_{_p}(mark(X))
mark(leq(X1, X2)) -> a_{_leq}(mark(X1), mark(X2))
mark(if(X1, X2, X3)) -> a_{_if}(mark(X1), X2, X3)
mark(diff(X1, X2)) -> a_{_diff}(mark(X1), mark(X2))
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)) -> A_{_LEQ}(mark(X1), mark(X2))

16 new Dependency Pairs are created:

MARK(leq(p(X'), X2)) -> A_{_LEQ}(a_{_p}(mark(X')), mark(X2))
MARK(leq(leq(X1'', X2''), X2)) -> A_{_LEQ}(a_{_leq}(mark(X1''), mark(X2'')), mark(X2))
MARK(leq(if(X1'', X2'', X3'), X2)) -> A_{_LEQ}(a_{_if}(mark(X1''), X2'', X3'), mark(X2))
MARK(leq(diff(X1'', X2''), X2)) -> A_{_LEQ}(a_{_diff}(mark(X1''), mark(X2'')), mark(X2))
MARK(leq(0, X2)) -> A_{_LEQ}(0, mark(X2))
MARK(leq(s(X'), X2)) -> A_{_LEQ}(s(mark(X')), mark(X2))
MARK(leq(true, X2)) -> A_{_LEQ}(true, mark(X2))
MARK(leq(false, X2)) -> A_{_LEQ}(false, mark(X2))
MARK(leq(X1, p(X'))) -> A_{_LEQ}(mark(X1), a_{_p}(mark(X')))
MARK(leq(X1, leq(X1'', X2''))) -> A_{_LEQ}(mark(X1), a_{_leq}(mark(X1''), mark(X2'')))
MARK(leq(X1, if(X1'', X2'', X3'))) -> A_{_LEQ}(mark(X1), a_{_if}(mark(X1''), X2'', X3'))
MARK(leq(X1, diff(X1'', X2''))) -> A_{_LEQ}(mark(X1), a_{_diff}(mark(X1''), mark(X2'')))
MARK(leq(X1, 0)) -> A_{_LEQ}(mark(X1), 0)
MARK(leq(X1, s(X'))) -> A_{_LEQ}(mark(X1), s(mark(X')))
MARK(leq(X1, true)) -> A_{_LEQ}(mark(X1), true)
MARK(leq(X1, false)) -> A_{_LEQ}(mark(X1), false)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 5

                 ↳Narrowing Transformation

Dependency Pairs:

A_{_DIFF}(X, s(X'')) -> A_{_LEQ}(mark(X), s(mark(X'')))
A_{_DIFF}(X, if(X1', X2', X3')) -> A_{_LEQ}(mark(X), a_{_if}(mark(X1'), X2', X3'))
A_{_DIFF}(X, leq(X1', X2')) -> A_{_LEQ}(mark(X), a_{_leq}(mark(X1'), mark(X2')))
A_{_DIFF}(X, p(X'')) -> A_{_LEQ}(mark(X), a_{_p}(mark(X'')))
A_{_DIFF}(s(X''), Y) -> A_{_LEQ}(s(mark(X'')), mark(Y))
A_{_DIFF}(diff(X1', X2'), Y) -> A_{_LEQ}(a_{_diff}(mark(X1'), mark(X2')), mark(Y))
A_{_DIFF}(if(X1', X2', X3'), Y) -> A_{_LEQ}(a_{_if}(mark(X1'), X2', X3'), mark(Y))
A_{_DIFF}(leq(X1', X2'), Y) -> A_{_LEQ}(a_{_leq}(mark(X1'), mark(X2')), mark(Y))
A_{_DIFF}(p(X''), Y) -> A_{_LEQ}(a_{_p}(mark(X'')), mark(Y))
A_{_DIFF}(X, Y) -> MARK(Y)
A_{_DIFF}(X, Y) -> MARK(X)
MARK(leq(X1, s(X'))) -> A_{_LEQ}(mark(X1), s(mark(X')))
MARK(leq(X1, diff(X1'', X2''))) -> A_{_LEQ}(mark(X1), a_{_diff}(mark(X1''), mark(X2'')))
MARK(leq(X1, if(X1'', X2'', X3'))) -> A_{_LEQ}(mark(X1), a_{_if}(mark(X1''), X2'', X3'))
MARK(leq(X1, leq(X1'', X2''))) -> A_{_LEQ}(mark(X1), a_{_leq}(mark(X1''), mark(X2'')))
MARK(leq(X1, p(X'))) -> A_{_LEQ}(mark(X1), a_{_p}(mark(X')))
MARK(leq(s(X'), X2)) -> A_{_LEQ}(s(mark(X')), mark(X2))
MARK(leq(diff(X1'', X2''), X2)) -> A_{_LEQ}(a_{_diff}(mark(X1''), mark(X2'')), mark(X2))
MARK(leq(if(X1'', X2'', X3'), X2)) -> A_{_LEQ}(a_{_if}(mark(X1''), X2'', X3'), mark(X2))
A_{_LEQ}(s(X), s(s(X''))) -> A_{_LEQ}(mark(X), s(mark(X'')))
A_{_LEQ}(s(X), s(diff(X1', X2'))) -> A_{_LEQ}(mark(X), a_{_diff}(mark(X1'), mark(X2')))
A_{_LEQ}(s(X), s(if(X1', X2', X3'))) -> A_{_LEQ}(mark(X), a_{_if}(mark(X1'), X2', X3'))
A_{_LEQ}(s(X), s(leq(X1', X2'))) -> A_{_LEQ}(mark(X), a_{_leq}(mark(X1'), mark(X2')))
A_{_LEQ}(s(X), s(p(X''))) -> A_{_LEQ}(mark(X), a_{_p}(mark(X'')))
A_{_LEQ}(s(s(X'')), s(Y)) -> A_{_LEQ}(s(mark(X'')), mark(Y))
A_{_LEQ}(s(diff(X1', X2')), s(Y)) -> A_{_LEQ}(a_{_diff}(mark(X1'), mark(X2')), mark(Y))
A_{_LEQ}(s(if(X1', X2', X3')), s(Y)) -> A_{_LEQ}(a_{_if}(mark(X1'), X2', X3'), mark(Y))
A_{_LEQ}(s(leq(X1', X2')), s(Y)) -> A_{_LEQ}(a_{_leq}(mark(X1'), mark(X2')), mark(Y))
A_{_LEQ}(s(p(X'')), s(Y)) -> A_{_LEQ}(a_{_p}(mark(X'')), mark(Y))
MARK(leq(leq(X1'', X2''), X2)) -> A_{_LEQ}(a_{_leq}(mark(X1''), mark(X2'')), mark(X2))
A_{_LEQ}(s(X), s(Y)) -> MARK(Y)
MARK(leq(p(X'), X2)) -> A_{_LEQ}(a_{_p}(mark(X')), mark(X2))
MARK(p(s(X''))) -> A_{_P}(s(mark(X'')))
MARK(p(diff(X1', X2'))) -> A_{_P}(a_{_diff}(mark(X1'), mark(X2')))
MARK(p(if(X1', X2', X3'))) -> A_{_P}(a_{_if}(mark(X1'), X2', X3'))
MARK(p(leq(X1', X2'))) -> A_{_P}(a_{_leq}(mark(X1'), mark(X2')))
A_{_P}(s(X)) -> MARK(X)
MARK(p(p(X''))) -> A_{_P}(a_{_p}(mark(X'')))
MARK(s(X)) -> MARK(X)
MARK(diff(X1, X2)) -> MARK(X2)
MARK(diff(X1, X2)) -> MARK(X1)
A_{_IF}(false, X, Y) -> MARK(Y)
A_{_DIFF}(X, Y) -> A_{_IF}(a_{_leq}(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
MARK(diff(X1, X2)) -> A_{_DIFF}(mark(X1), mark(X2))
MARK(if(X1, X2, X3)) -> MARK(X1)
A_{_IF}(true, X, Y) -> MARK(X)
MARK(if(X1, X2, X3)) -> A_{_IF}(mark(X1), X2, X3)
MARK(leq(X1, X2)) -> MARK(X2)
MARK(leq(X1, X2)) -> MARK(X1)
MARK(p(X)) -> MARK(X)
A_{_LEQ}(s(X), s(Y)) -> MARK(X)
A_{_DIFF}(X, diff(X1', X2')) -> A_{_LEQ}(mark(X), a_{_diff}(mark(X1'), mark(X2')))

Rules:

a_{_p}(0) -> 0
a_{_p}(s(X)) -> mark(X)
a_{_p}(X) -> p(X)
a_{_leq}(0, Y) -> true
a_{_leq}(s(X), 0) -> false
a_{_leq}(s(X), s(Y)) -> a_{_leq}(mark(X), mark(Y))
a_{_leq}(X1, X2) -> leq(X1, X2)
a_{_if}(true, X, Y) -> mark(X)
a_{_if}(false, X, Y) -> mark(Y)
a_{_if}(X1, X2, X3) -> if(X1, X2, X3)
a_{_diff}(X, Y) -> a_{_if}(a_{_leq}(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
a_{_diff}(X1, X2) -> diff(X1, X2)
mark(p(X)) -> a_{_p}(mark(X))
mark(leq(X1, X2)) -> a_{_leq}(mark(X1), mark(X2))
mark(if(X1, X2, X3)) -> a_{_if}(mark(X1), X2, X3)
mark(diff(X1, X2)) -> a_{_diff}(mark(X1), mark(X2))
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)) -> A_{_IF}(mark(X1), X2, X3)

eight new Dependency Pairs are created:

MARK(if(p(X'), X2, X3)) -> A_{_IF}(a_{_p}(mark(X')), X2, X3)
MARK(if(leq(X1'', X2''), X2, X3)) -> A_{_IF}(a_{_leq}(mark(X1''), mark(X2'')), X2, X3)
MARK(if(if(X1'', X2'', X3''), X2, X3)) -> A_{_IF}(a_{_if}(mark(X1''), X2'', X3''), X2, X3)
MARK(if(diff(X1'', X2''), X2, X3)) -> A_{_IF}(a_{_diff}(mark(X1''), mark(X2'')), X2, X3)
MARK(if(0, X2, X3)) -> A_{_IF}(0, X2, X3)
MARK(if(s(X'), X2, X3)) -> A_{_IF}(s(mark(X')), X2, X3)
MARK(if(true, X2, X3)) -> A_{_IF}(true, X2, X3)
MARK(if(false, X2, X3)) -> A_{_IF}(false, X2, X3)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 6

                 ↳Negative Polynomial Order

Dependency Pairs:

A_{_DIFF}(X, diff(X1', X2')) -> A_{_LEQ}(mark(X), a_{_diff}(mark(X1'), mark(X2')))
A_{_DIFF}(X, if(X1', X2', X3')) -> A_{_LEQ}(mark(X), a_{_if}(mark(X1'), X2', X3'))
A_{_DIFF}(X, leq(X1', X2')) -> A_{_LEQ}(mark(X), a_{_leq}(mark(X1'), mark(X2')))
A_{_DIFF}(X, p(X'')) -> A_{_LEQ}(mark(X), a_{_p}(mark(X'')))
A_{_DIFF}(s(X''), Y) -> A_{_LEQ}(s(mark(X'')), mark(Y))
A_{_DIFF}(diff(X1', X2'), Y) -> A_{_LEQ}(a_{_diff}(mark(X1'), mark(X2')), mark(Y))
A_{_DIFF}(if(X1', X2', X3'), Y) -> A_{_LEQ}(a_{_if}(mark(X1'), X2', X3'), mark(Y))
A_{_DIFF}(leq(X1', X2'), Y) -> A_{_LEQ}(a_{_leq}(mark(X1'), mark(X2')), mark(Y))
A_{_DIFF}(p(X''), Y) -> A_{_LEQ}(a_{_p}(mark(X'')), mark(Y))
A_{_DIFF}(X, Y) -> MARK(Y)
A_{_DIFF}(X, Y) -> MARK(X)
MARK(if(false, X2, X3)) -> A_{_IF}(false, X2, X3)
MARK(if(true, X2, X3)) -> A_{_IF}(true, X2, X3)
MARK(if(diff(X1'', X2''), X2, X3)) -> A_{_IF}(a_{_diff}(mark(X1''), mark(X2'')), X2, X3)
MARK(if(if(X1'', X2'', X3''), X2, X3)) -> A_{_IF}(a_{_if}(mark(X1''), X2'', X3''), X2, X3)
MARK(if(leq(X1'', X2''), X2, X3)) -> A_{_IF}(a_{_leq}(mark(X1''), mark(X2'')), X2, X3)
A_{_IF}(false, X, Y) -> MARK(Y)
MARK(if(p(X'), X2, X3)) -> A_{_IF}(a_{_p}(mark(X')), X2, X3)
MARK(leq(X1, s(X'))) -> A_{_LEQ}(mark(X1), s(mark(X')))
MARK(leq(X1, diff(X1'', X2''))) -> A_{_LEQ}(mark(X1), a_{_diff}(mark(X1''), mark(X2'')))
MARK(leq(X1, if(X1'', X2'', X3'))) -> A_{_LEQ}(mark(X1), a_{_if}(mark(X1''), X2'', X3'))
MARK(leq(X1, leq(X1'', X2''))) -> A_{_LEQ}(mark(X1), a_{_leq}(mark(X1''), mark(X2'')))
MARK(leq(X1, p(X'))) -> A_{_LEQ}(mark(X1), a_{_p}(mark(X')))
MARK(leq(s(X'), X2)) -> A_{_LEQ}(s(mark(X')), mark(X2))
MARK(leq(diff(X1'', X2''), X2)) -> A_{_LEQ}(a_{_diff}(mark(X1''), mark(X2'')), mark(X2))
MARK(leq(if(X1'', X2'', X3'), X2)) -> A_{_LEQ}(a_{_if}(mark(X1''), X2'', X3'), mark(X2))
A_{_LEQ}(s(X), s(s(X''))) -> A_{_LEQ}(mark(X), s(mark(X'')))
A_{_LEQ}(s(X), s(diff(X1', X2'))) -> A_{_LEQ}(mark(X), a_{_diff}(mark(X1'), mark(X2')))
A_{_LEQ}(s(X), s(if(X1', X2', X3'))) -> A_{_LEQ}(mark(X), a_{_if}(mark(X1'), X2', X3'))
A_{_LEQ}(s(X), s(leq(X1', X2'))) -> A_{_LEQ}(mark(X), a_{_leq}(mark(X1'), mark(X2')))
A_{_LEQ}(s(X), s(p(X''))) -> A_{_LEQ}(mark(X), a_{_p}(mark(X'')))
A_{_LEQ}(s(s(X'')), s(Y)) -> A_{_LEQ}(s(mark(X'')), mark(Y))
A_{_LEQ}(s(diff(X1', X2')), s(Y)) -> A_{_LEQ}(a_{_diff}(mark(X1'), mark(X2')), mark(Y))
A_{_LEQ}(s(if(X1', X2', X3')), s(Y)) -> A_{_LEQ}(a_{_if}(mark(X1'), X2', X3'), mark(Y))
A_{_LEQ}(s(leq(X1', X2')), s(Y)) -> A_{_LEQ}(a_{_leq}(mark(X1'), mark(X2')), mark(Y))
A_{_LEQ}(s(p(X'')), s(Y)) -> A_{_LEQ}(a_{_p}(mark(X'')), mark(Y))
MARK(leq(leq(X1'', X2''), X2)) -> A_{_LEQ}(a_{_leq}(mark(X1''), mark(X2'')), mark(X2))
A_{_LEQ}(s(X), s(Y)) -> MARK(Y)
MARK(leq(p(X'), X2)) -> A_{_LEQ}(a_{_p}(mark(X')), mark(X2))
MARK(p(s(X''))) -> A_{_P}(s(mark(X'')))
MARK(p(diff(X1', X2'))) -> A_{_P}(a_{_diff}(mark(X1'), mark(X2')))
MARK(p(if(X1', X2', X3'))) -> A_{_P}(a_{_if}(mark(X1'), X2', X3'))
MARK(p(leq(X1', X2'))) -> A_{_P}(a_{_leq}(mark(X1'), mark(X2')))
A_{_P}(s(X)) -> MARK(X)
MARK(p(p(X''))) -> A_{_P}(a_{_p}(mark(X'')))
MARK(s(X)) -> MARK(X)
MARK(diff(X1, X2)) -> MARK(X2)
MARK(diff(X1, X2)) -> MARK(X1)
A_{_IF}(true, X, Y) -> MARK(X)
A_{_DIFF}(X, Y) -> A_{_IF}(a_{_leq}(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
MARK(diff(X1, X2)) -> A_{_DIFF}(mark(X1), mark(X2))
MARK(if(X1, X2, X3)) -> MARK(X1)
MARK(leq(X1, X2)) -> MARK(X2)
MARK(leq(X1, X2)) -> MARK(X1)
MARK(p(X)) -> MARK(X)
A_{_LEQ}(s(X), s(Y)) -> MARK(X)
A_{_DIFF}(X, s(X'')) -> A_{_LEQ}(mark(X), s(mark(X'')))

Rules:

a_{_p}(0) -> 0
a_{_p}(s(X)) -> mark(X)
a_{_p}(X) -> p(X)
a_{_leq}(0, Y) -> true
a_{_leq}(s(X), 0) -> false
a_{_leq}(s(X), s(Y)) -> a_{_leq}(mark(X), mark(Y))
a_{_leq}(X1, X2) -> leq(X1, X2)
a_{_if}(true, X, Y) -> mark(X)
a_{_if}(false, X, Y) -> mark(Y)
a_{_if}(X1, X2, X3) -> if(X1, X2, X3)
a_{_diff}(X, Y) -> a_{_if}(a_{_leq}(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
a_{_diff}(X1, X2) -> diff(X1, X2)
mark(p(X)) -> a_{_p}(mark(X))
mark(leq(X1, X2)) -> a_{_leq}(mark(X1), mark(X2))
mark(if(X1, X2, X3)) -> a_{_if}(mark(X1), X2, X3)
mark(diff(X1, X2)) -> a_{_diff}(mark(X1), mark(X2))
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.

A_{_DIFF}(X, leq(X1', X2')) -> A_{_LEQ}(mark(X), a_{_leq}(mark(X1'), mark(X2')))
MARK(leq(X1, leq(X1'', X2''))) -> A_{_LEQ}(mark(X1), a_{_leq}(mark(X1''), mark(X2'')))
A_{_LEQ}(s(X), s(leq(X1', X2'))) -> A_{_LEQ}(mark(X), a_{_leq}(mark(X1'), mark(X2')))

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

mark(p(X)) -> a_{_p}(mark(X))
mark(leq(X1, X2)) -> a_{_leq}(mark(X1), mark(X2))
mark(if(X1, X2, X3)) -> a_{_if}(mark(X1), X2, X3)
mark(diff(X1, X2)) -> a_{_diff}(mark(X1), mark(X2))
mark(0) -> 0
mark(s(X)) -> s(mark(X))
mark(true) -> true
mark(false) -> false
a_{_diff}(X, Y) -> a_{_if}(a_{_leq}(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
a_{_diff}(X1, X2) -> diff(X1, X2)
a_{_if}(true, X, Y) -> mark(X)
a_{_if}(false, X, Y) -> mark(Y)
a_{_if}(X1, X2, X3) -> if(X1, X2, X3)
a_{_leq}(0, Y) -> true
a_{_leq}(s(X), 0) -> false
a_{_leq}(s(X), s(Y)) -> a_{_leq}(mark(X), mark(Y))
a_{_leq}(X1, X2) -> leq(X1, X2)
a_{_p}(0) -> 0
a_{_p}(s(X)) -> mark(X)
a_{_p}(X) -> p(X)

Used ordering:
Polynomial Order with Interpretation:

POL( A_{_DIFF}(x₁, x₂) ) = 1

POL( A_{_LEQ}(x₁, x₂) ) = x₂

POL( a_{_leq}(x₁, x₂) ) = 0

POL( MARK(x₁) ) = 1

POL( mark(x₁) ) = 1

POL( a_{_p}(x₁) ) = 1

POL( s(x₁) ) = 1

POL( a_{_diff}(x₁, x₂) ) = 1

POL( A_{_IF}(x₁, ..., x₃) ) = 1

POL( A_{_P}(x₁) ) = 1

POL( a_{_if}(x₁, ..., x₃) ) = 1

POL( 0 ) = 0

POL( true ) = 0

POL( false ) = 0

POL( diff(x₁, x₂) ) = 0

POL( if(x₁, ..., x₃) ) = 0

POL( leq(x₁, x₂) ) = 0

POL( p(x₁) ) = 0

This results in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 7

                 ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

A_{_DIFF}(X, diff(X1', X2')) -> A_{_LEQ}(mark(X), a_{_diff}(mark(X1'), mark(X2')))
A_{_DIFF}(X, if(X1', X2', X3')) -> A_{_LEQ}(mark(X), a_{_if}(mark(X1'), X2', X3'))
A_{_DIFF}(X, p(X'')) -> A_{_LEQ}(mark(X), a_{_p}(mark(X'')))
A_{_DIFF}(s(X''), Y) -> A_{_LEQ}(s(mark(X'')), mark(Y))
A_{_DIFF}(diff(X1', X2'), Y) -> A_{_LEQ}(a_{_diff}(mark(X1'), mark(X2')), mark(Y))
A_{_DIFF}(if(X1', X2', X3'), Y) -> A_{_LEQ}(a_{_if}(mark(X1'), X2', X3'), mark(Y))
A_{_DIFF}(leq(X1', X2'), Y) -> A_{_LEQ}(a_{_leq}(mark(X1'), mark(X2')), mark(Y))
A_{_DIFF}(p(X''), Y) -> A_{_LEQ}(a_{_p}(mark(X'')), mark(Y))
A_{_DIFF}(X, Y) -> MARK(Y)
A_{_DIFF}(X, Y) -> MARK(X)
MARK(if(false, X2, X3)) -> A_{_IF}(false, X2, X3)
MARK(if(true, X2, X3)) -> A_{_IF}(true, X2, X3)
MARK(if(diff(X1'', X2''), X2, X3)) -> A_{_IF}(a_{_diff}(mark(X1''), mark(X2'')), X2, X3)
MARK(if(if(X1'', X2'', X3''), X2, X3)) -> A_{_IF}(a_{_if}(mark(X1''), X2'', X3''), X2, X3)
MARK(if(leq(X1'', X2''), X2, X3)) -> A_{_IF}(a_{_leq}(mark(X1''), mark(X2'')), X2, X3)
A_{_IF}(false, X, Y) -> MARK(Y)
MARK(if(p(X'), X2, X3)) -> A_{_IF}(a_{_p}(mark(X')), X2, X3)
MARK(leq(X1, s(X'))) -> A_{_LEQ}(mark(X1), s(mark(X')))
MARK(leq(X1, diff(X1'', X2''))) -> A_{_LEQ}(mark(X1), a_{_diff}(mark(X1''), mark(X2'')))
MARK(leq(X1, if(X1'', X2'', X3'))) -> A_{_LEQ}(mark(X1), a_{_if}(mark(X1''), X2'', X3'))
MARK(leq(X1, p(X'))) -> A_{_LEQ}(mark(X1), a_{_p}(mark(X')))
MARK(leq(s(X'), X2)) -> A_{_LEQ}(s(mark(X')), mark(X2))
MARK(leq(diff(X1'', X2''), X2)) -> A_{_LEQ}(a_{_diff}(mark(X1''), mark(X2'')), mark(X2))
MARK(leq(if(X1'', X2'', X3'), X2)) -> A_{_LEQ}(a_{_if}(mark(X1''), X2'', X3'), mark(X2))
A_{_LEQ}(s(X), s(s(X''))) -> A_{_LEQ}(mark(X), s(mark(X'')))
A_{_LEQ}(s(X), s(diff(X1', X2'))) -> A_{_LEQ}(mark(X), a_{_diff}(mark(X1'), mark(X2')))
A_{_LEQ}(s(X), s(if(X1', X2', X3'))) -> A_{_LEQ}(mark(X), a_{_if}(mark(X1'), X2', X3'))
A_{_LEQ}(s(X), s(p(X''))) -> A_{_LEQ}(mark(X), a_{_p}(mark(X'')))
A_{_LEQ}(s(s(X'')), s(Y)) -> A_{_LEQ}(s(mark(X'')), mark(Y))
A_{_LEQ}(s(diff(X1', X2')), s(Y)) -> A_{_LEQ}(a_{_diff}(mark(X1'), mark(X2')), mark(Y))
A_{_LEQ}(s(if(X1', X2', X3')), s(Y)) -> A_{_LEQ}(a_{_if}(mark(X1'), X2', X3'), mark(Y))
A_{_LEQ}(s(leq(X1', X2')), s(Y)) -> A_{_LEQ}(a_{_leq}(mark(X1'), mark(X2')), mark(Y))
A_{_LEQ}(s(p(X'')), s(Y)) -> A_{_LEQ}(a_{_p}(mark(X'')), mark(Y))
MARK(leq(leq(X1'', X2''), X2)) -> A_{_LEQ}(a_{_leq}(mark(X1''), mark(X2'')), mark(X2))
A_{_LEQ}(s(X), s(Y)) -> MARK(Y)
MARK(leq(p(X'), X2)) -> A_{_LEQ}(a_{_p}(mark(X')), mark(X2))
MARK(p(s(X''))) -> A_{_P}(s(mark(X'')))
MARK(p(diff(X1', X2'))) -> A_{_P}(a_{_diff}(mark(X1'), mark(X2')))
MARK(p(if(X1', X2', X3'))) -> A_{_P}(a_{_if}(mark(X1'), X2', X3'))
MARK(p(leq(X1', X2'))) -> A_{_P}(a_{_leq}(mark(X1'), mark(X2')))
A_{_P}(s(X)) -> MARK(X)
MARK(p(p(X''))) -> A_{_P}(a_{_p}(mark(X'')))
MARK(s(X)) -> MARK(X)
MARK(diff(X1, X2)) -> MARK(X2)
MARK(diff(X1, X2)) -> MARK(X1)
A_{_IF}(true, X, Y) -> MARK(X)
A_{_DIFF}(X, Y) -> A_{_IF}(a_{_leq}(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
MARK(diff(X1, X2)) -> A_{_DIFF}(mark(X1), mark(X2))
MARK(if(X1, X2, X3)) -> MARK(X1)
MARK(leq(X1, X2)) -> MARK(X2)
MARK(leq(X1, X2)) -> MARK(X1)
MARK(p(X)) -> MARK(X)
A_{_LEQ}(s(X), s(Y)) -> MARK(X)
A_{_DIFF}(X, s(X'')) -> A_{_LEQ}(mark(X), s(mark(X'')))

Rules:

a_{_p}(0) -> 0
a_{_p}(s(X)) -> mark(X)
a_{_p}(X) -> p(X)
a_{_leq}(0, Y) -> true
a_{_leq}(s(X), 0) -> false
a_{_leq}(s(X), s(Y)) -> a_{_leq}(mark(X), mark(Y))
a_{_leq}(X1, X2) -> leq(X1, X2)
a_{_if}(true, X, Y) -> mark(X)
a_{_if}(false, X, Y) -> mark(Y)
a_{_if}(X1, X2, X3) -> if(X1, X2, X3)
a_{_diff}(X, Y) -> a_{_if}(a_{_leq}(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
a_{_diff}(X1, X2) -> diff(X1, X2)
mark(p(X)) -> a_{_p}(mark(X))
mark(leq(X1, X2)) -> a_{_leq}(mark(X1), mark(X2))
mark(if(X1, X2, X3)) -> a_{_if}(mark(X1), X2, X3)
mark(diff(X1, X2)) -> a_{_diff}(mark(X1), mark(X2))
mark(0) -> 0
mark(s(X)) -> s(mark(X))
mark(true) -> true
mark(false) -> false

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