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

         ↳Polynomial Ordering

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

The following dependency pair can be strictly oriented:

A_{_IF}(false, X, Y) -> MARK(Y)

Additionally, the following usable rules for innermost can be oriented:

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

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(if(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(c) = 0

POL(MARK(x₁)) = x₁

POL(false) = 1

POL(a__if(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(true) = 0

POL(A__F(x₁)) = x₁

POL(mark(x₁)) = x₁

POL(f(x₁)) = x₁

POL(a__f(x₁)) = x₁

POL(A__IF(x₁, x₂, x₃)) = x₁ + x₂ + x₃

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 2

             ↳Polynomial Ordering

Dependency Pairs:

MARK(if(X1, X2, X3)) -> MARK(X2)
MARK(if(X1, X2, X3)) -> MARK(X1)
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

The following dependency pairs can be strictly oriented:

MARK(f(X)) -> MARK(X)
MARK(f(X)) -> A_{_F}(mark(X))

Additionally, the following usable rules for innermost can be oriented:

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

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(if(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(c) = 0

POL(MARK(x₁)) = x₁

POL(false) = 0

POL(a__if(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(true) = 0

POL(A__F(x₁)) = x₁

POL(mark(x₁)) = x₁

POL(f(x₁)) = 1 + x₁

POL(a__f(x₁)) = 1 + x₁

POL(A__IF(x₁, x₂, x₃)) = x₂

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 2

             ↳Polo

...

               →DP Problem 3

                 ↳Dependency Graph

Dependency Pairs:

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

Using the Dependency Graph the DP problem was split into 1 DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 2

             ↳Polo

...

               →DP Problem 4

                 ↳Narrowing Transformation

Dependency Pairs:

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(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

         ↳Polo

           →DP Problem 2

             ↳Polo

...

               →DP Problem 5

                 ↳Polynomial Ordering

Dependency Pairs:

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

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

The following dependency pair can be strictly oriented:

MARK(if(f(X'), X2, X3)) -> A_{_IF}(a_{_f}(mark(X')), mark(X2), X3)

Additionally, the following usable rules for innermost can be oriented:

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

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(if(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(c) = 0

POL(MARK(x₁)) = x₁

POL(false) = 0

POL(a__if(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(true) = 0

POL(mark(x₁)) = x₁

POL(f(x₁)) = 1 + x₁

POL(a__f(x₁)) = 1 + x₁

POL(A__IF(x₁, x₂, x₃)) = x₂

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 2

             ↳Polo

...

               →DP Problem 6

                 ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

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(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(X1, X2, X3)) -> MARK(X2)
MARK(if(X1, X2, X3)) -> MARK(X1)

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:03 minutes

POL(if(x₁, x₂, x₃))	= x₁ + x₂ + x₃
POL(c)	= 0
POL(MARK(x₁))	= x₁
POL(false)	= 1
POL(a__if(x₁, x₂, x₃))	= x₁ + x₂ + x₃
POL(true)	= 0
POL(A__F(x₁))	= x₁
POL(mark(x₁))	= x₁
POL(f(x₁))	= x₁
POL(a__f(x₁))	= x₁
POL(A__IF(x₁, x₂, x₃))	= x₁ + x₂ + x₃