Termination Proof using AProVE

Term Rewriting System R:
[X, Y, X1, X2, X3]
a_{_f}(X) -> a_{_if}(mark(X), c, f(true))
a_{_f}(X) -> f(X)
a_{_if}(true, X, Y) -> mark(X)
a_{_if}(false, X, Y) -> mark(Y)
a_{_if}(X1, X2, X3) -> if(X1, X2, X3)
mark(f(X)) -> a_{_f}(mark(X))
mark(if(X1, X2, X3)) -> a_{_if}(mark(X1), mark(X2), X3)
mark(c) -> c
mark(true) -> true
mark(false) -> false

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

A_{_F}(X) -> A_{_IF}(mark(X), c, f(true))
A_{_F}(X) -> MARK(X)
A_{_IF}(true, X, Y) -> MARK(X)
A_{_IF}(false, X, Y) -> MARK(Y)
MARK(f(X)) -> A_{_F}(mark(X))
MARK(f(X)) -> MARK(X)
MARK(if(X1, X2, X3)) -> A_{_IF}(mark(X1), mark(X2), X3)
MARK(if(X1, X2, X3)) -> MARK(X1)
MARK(if(X1, X2, X3)) -> MARK(X2)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Narrowing Transformation

Dependency Pairs:

MARK(if(X1, X2, X3)) -> 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), mark(X2), X3)
MARK(f(X)) -> MARK(X)
A_{_F}(X) -> MARK(X)
MARK(f(X)) -> A_{_F}(mark(X))
A_{_IF}(true, X, Y) -> MARK(X)
A_{_F}(X) -> A_{_IF}(mark(X), c, f(true))

Rules:

a_{_f}(X) -> a_{_if}(mark(X), c, f(true))
a_{_f}(X) -> f(X)
a_{_if}(true, X, Y) -> mark(X)
a_{_if}(false, X, Y) -> mark(Y)
a_{_if}(X1, X2, X3) -> if(X1, X2, X3)
mark(f(X)) -> a_{_f}(mark(X))
mark(if(X1, X2, X3)) -> a_{_if}(mark(X1), mark(X2), X3)
mark(c) -> c
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_{_F}(X) -> A_{_IF}(mark(X), c, f(true))

five new Dependency Pairs are created:

A_{_F}(f(X'')) -> A_{_IF}(a_{_f}(mark(X'')), c, f(true))
A_{_F}(if(X1', X2', X3')) -> A_{_IF}(a_{_if}(mark(X1'), mark(X2'), X3'), c, f(true))
A_{_F}(c) -> A_{_IF}(c, c, f(true))
A_{_F}(true) -> A_{_IF}(true, c, f(true))
A_{_F}(false) -> A_{_IF}(false, c, f(true))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Narrowing Transformation

Dependency Pairs:

A_{_F}(false) -> A_{_IF}(false, c, f(true))
A_{_F}(true) -> A_{_IF}(true, c, f(true))
A_{_F}(if(X1', X2', X3')) -> A_{_IF}(a_{_if}(mark(X1'), mark(X2'), X3'), c, f(true))
A_{_F}(f(X'')) -> A_{_IF}(a_{_f}(mark(X'')), c, f(true))
A_{_IF}(false, X, Y) -> MARK(Y)
MARK(if(X1, X2, X3)) -> MARK(X1)
A_{_IF}(true, X, Y) -> MARK(X)
MARK(if(X1, X2, X3)) -> A_{_IF}(mark(X1), mark(X2), X3)
MARK(f(X)) -> MARK(X)
A_{_F}(X) -> MARK(X)
MARK(f(X)) -> A_{_F}(mark(X))
MARK(if(X1, X2, X3)) -> MARK(X2)

Rules:

a_{_f}(X) -> a_{_if}(mark(X), c, f(true))
a_{_f}(X) -> f(X)
a_{_if}(true, X, Y) -> mark(X)
a_{_if}(false, X, Y) -> mark(Y)
a_{_if}(X1, X2, X3) -> if(X1, X2, X3)
mark(f(X)) -> a_{_f}(mark(X))
mark(if(X1, X2, X3)) -> a_{_if}(mark(X1), mark(X2), X3)
mark(c) -> c
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

MARK(if(X1, X2, X3)) -> A_{_IF}(mark(X1), mark(X2), X3)

10 new Dependency Pairs are created:

MARK(if(f(X'), X2, X3)) -> A_{_IF}(a_{_f}(mark(X')), mark(X2), X3)
MARK(if(if(X1'', X2'', X3''), X2, X3)) -> A_{_IF}(a_{_if}(mark(X1''), mark(X2''), X3''), mark(X2), X3)
MARK(if(c, X2, X3)) -> A_{_IF}(c, mark(X2), X3)
MARK(if(true, X2, X3)) -> A_{_IF}(true, mark(X2), X3)
MARK(if(false, X2, X3)) -> A_{_IF}(false, mark(X2), X3)
MARK(if(X1, f(X'), X3)) -> A_{_IF}(mark(X1), a_{_f}(mark(X')), X3)
MARK(if(X1, if(X1'', X2'', X3''), X3)) -> A_{_IF}(mark(X1), a_{_if}(mark(X1''), mark(X2''), X3''), X3)
MARK(if(X1, c, X3)) -> A_{_IF}(mark(X1), c, X3)
MARK(if(X1, true, X3)) -> A_{_IF}(mark(X1), true, X3)
MARK(if(X1, false, X3)) -> A_{_IF}(mark(X1), false, X3)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 3

                 ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

A_{_F}(true) -> A_{_IF}(true, c, f(true))
A_{_F}(if(X1', X2', X3')) -> A_{_IF}(a_{_if}(mark(X1'), mark(X2'), X3'), c, f(true))
A_{_F}(f(X'')) -> A_{_IF}(a_{_f}(mark(X'')), c, f(true))
MARK(if(X1, false, X3)) -> A_{_IF}(mark(X1), false, X3)
MARK(if(X1, true, X3)) -> A_{_IF}(mark(X1), true, X3)
MARK(if(X1, c, X3)) -> A_{_IF}(mark(X1), c, X3)
MARK(if(X1, if(X1'', X2'', X3''), X3)) -> A_{_IF}(mark(X1), a_{_if}(mark(X1''), mark(X2''), X3''), X3)
MARK(if(X1, f(X'), X3)) -> A_{_IF}(mark(X1), a_{_f}(mark(X')), X3)
MARK(if(false, X2, X3)) -> A_{_IF}(false, mark(X2), X3)
MARK(if(true, X2, X3)) -> A_{_IF}(true, mark(X2), X3)
MARK(if(if(X1'', X2'', X3''), X2, X3)) -> A_{_IF}(a_{_if}(mark(X1''), mark(X2''), X3''), mark(X2), X3)
A_{_IF}(true, X, Y) -> MARK(X)
MARK(if(f(X'), X2, X3)) -> A_{_IF}(a_{_f}(mark(X')), mark(X2), X3)
MARK(if(X1, X2, X3)) -> MARK(X2)
MARK(if(X1, X2, X3)) -> MARK(X1)
MARK(f(X)) -> MARK(X)
A_{_F}(X) -> MARK(X)
MARK(f(X)) -> A_{_F}(mark(X))
A_{_IF}(false, X, Y) -> MARK(Y)
A_{_F}(false) -> A_{_IF}(false, c, f(true))

Rules:

a_{_f}(X) -> a_{_if}(mark(X), c, f(true))
a_{_f}(X) -> f(X)
a_{_if}(true, X, Y) -> mark(X)
a_{_if}(false, X, Y) -> mark(Y)
a_{_if}(X1, X2, X3) -> if(X1, X2, X3)
mark(f(X)) -> a_{_f}(mark(X))
mark(if(X1, X2, X3)) -> a_{_if}(mark(X1), mark(X2), X3)
mark(c) -> c
mark(true) -> true
mark(false) -> false

Strategy:

innermost

Innermost Termination of R could not be shown.
Duration:
0:05 minutes