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

Innermost 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

Strategy:

innermost

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

Strategy:

innermost

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

A_{_DIFF}(X, Y) -> A_{_IF}(a_{_leq}(mark(X), mark(Y)), 0, s(diff(p(X), Y)))

17 new Dependency Pairs are created:

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

Strategy:

innermost

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 4

                 ↳Remaining Obligation(s)

The following remains to be proven:
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, true) -> A_{_IF}(a_{_leq}(mark(X), true), 0, s(diff(p(X), true)))
A_{_DIFF}(X, s(X'')) -> A_{_IF}(a_{_leq}(mark(X), s(mark(X''))), 0, s(diff(p(X), s(X''))))
A_{_DIFF}(X, 0) -> A_{_IF}(a_{_leq}(mark(X), 0), 0, s(diff(p(X), 0)))
A_{_DIFF}(X, diff(X1', X2')) -> A_{_IF}(a_{_leq}(mark(X), a_{_diff}(mark(X1'), mark(X2'))), 0, s(diff(p(X), diff(X1', X2'))))
A_{_DIFF}(X, if(X1', X2', X3')) -> A_{_IF}(a_{_leq}(mark(X), a_{_if}(mark(X1'), X2', X3')), 0, s(diff(p(X), if(X1', X2', X3'))))
A_{_DIFF}(X, leq(X1', X2')) -> A_{_IF}(a_{_leq}(mark(X), a_{_leq}(mark(X1'), mark(X2'))), 0, s(diff(p(X), leq(X1', X2'))))
A_{_DIFF}(X, p(X'')) -> A_{_IF}(a_{_leq}(mark(X), a_{_p}(mark(X''))), 0, s(diff(p(X), p(X''))))
A_{_DIFF}(false, Y) -> A_{_IF}(a_{_leq}(false, mark(Y)), 0, s(diff(p(false), Y)))
A_{_DIFF}(true, Y) -> A_{_IF}(a_{_leq}(true, mark(Y)), 0, s(diff(p(true), Y)))
A_{_DIFF}(s(X''), Y) -> A_{_IF}(a_{_leq}(s(mark(X'')), mark(Y)), 0, s(diff(p(s(X'')), Y)))
A_{_DIFF}(0, Y) -> A_{_IF}(a_{_leq}(0, mark(Y)), 0, s(diff(p(0), Y)))
A_{_DIFF}(diff(X1', X2'), Y) -> A_{_IF}(a_{_leq}(a_{_diff}(mark(X1'), mark(X2')), mark(Y)), 0, s(diff(p(diff(X1', X2')), Y)))
A_{_DIFF}(if(X1', X2', X3'), Y) -> A_{_IF}(a_{_leq}(a_{_if}(mark(X1'), X2', X3'), mark(Y)), 0, s(diff(p(if(X1', X2', X3')), Y)))
A_{_DIFF}(leq(X1', X2'), Y) -> A_{_IF}(a_{_leq}(a_{_leq}(mark(X1'), mark(X2')), mark(Y)), 0, s(diff(p(leq(X1', X2')), Y)))
A_{_DIFF}(p(X''), Y) -> A_{_IF}(a_{_leq}(a_{_p}(mark(X'')), mark(Y)), 0, s(diff(p(p(X'')), 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_{_DIFF}(X, Y) -> MARK(X)
MARK(diff(X1, X2)) -> A_{_DIFF}(mark(X1), mark(X2))
MARK(if(X1, X2, X3)) -> MARK(X1)
A_{_IF}(false, X, Y) -> MARK(Y)
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_{_IF}(true, X, Y) -> MARK(X)
A_{_DIFF}(X, false) -> A_{_IF}(a_{_leq}(mark(X), false), 0, s(diff(p(X), false)))

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

Strategy:

innermost

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