Termination Proof using AProVE

Term Rewriting System R:
[x, y, z]
f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

F(f(f(a, b), c), x) -> F(b, f(a, f(c, f(b, x))))
F(f(f(a, b), c), x) -> F(a, f(c, f(b, x)))
F(f(f(a, b), c), x) -> F(c, f(b, x))
F(f(f(a, b), c), x) -> F(b, x)
F(x, f(y, z)) -> F(f(x, y), z)
F(x, f(y, z)) -> F(x, y)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Modular Removal of Rules

Dependency Pairs:

F(f(f(a, b), c), x) -> F(b, x)
F(f(f(a, b), c), x) -> F(c, f(b, x))
F(x, f(y, z)) -> F(x, y)
F(f(f(a, b), c), x) -> F(a, f(c, f(b, x)))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), x) -> F(b, f(a, f(c, f(b, x))))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

We have the following set of usable rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

To remove rules and DPs from this DP problem we used the following monotonic and C_E-compatible order: Polynomial ordering.
Polynomial interpretation:

POL(c) = 0

POL(b) = 0

POL(a) = 1

POL(F(x₁, x₂)) = 1 + x₁ + x₂

POL(f(x₁, x₂)) = x₁ + x₂

We have the following set D of usable symbols: {c, b, a, F, f}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

F(f(f(a, b), c), x) -> F(b, x)
F(f(f(a, b), c), x) -> F(c, f(b, x))

No Rules can be deleted.

The result of this processor delivers one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳MRR

           →DP Problem 2

             ↳Negative Polynomial Order

Dependency Pairs:

F(x, f(y, z)) -> F(x, y)
F(f(f(a, b), c), x) -> F(a, f(c, f(b, x)))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), x) -> F(b, f(a, f(c, f(b, x))))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

F(f(f(a, b), c), x) -> F(b, f(a, f(c, f(b, x))))

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

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Used ordering:
Polynomial Order with Interpretation:

POL( F(x₁, x₂) ) = x₁

POL( f(x₁, x₂) ) = x₁

POL( a ) = 1

POL( b ) = 0

This results in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳MRR

           →DP Problem 2

             ↳Neg POLO

...

               →DP Problem 3

                 ↳Narrowing Transformation

Dependency Pairs:

F(x, f(y, z)) -> F(x, y)
F(f(f(a, b), c), x) -> F(a, f(c, f(b, x)))
F(x, f(y, z)) -> F(f(x, y), z)

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

F(f(f(a, b), c), x) -> F(a, f(c, f(b, x)))

two new Dependency Pairs are created:

F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(f(f(a, b), c), f(y', z')) -> F(a, f(c, f(f(b, y'), z')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳MRR

           →DP Problem 2

             ↳Neg POLO

...

               →DP Problem 4

                 ↳Semantic Labelling

Dependency Pairs:

F(f(f(a, b), c), f(y', z')) -> F(a, f(c, f(f(b, y'), z')))
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(x, f(y, z)) -> F(f(x, y), z)
F(x, f(y, z)) -> F(x, y)

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

Using Semantic Labelling, the DP problem could be transformed. The following model was found:

f(x₀, x₁) = x₁

a = 1

b = 0

c = 0

F(x₀, x₁) = 1

From the dependency graph we obtain 2 (labeled) SCCs which each result in correspondingDP problem.

     ↳DPs

       →DP Problem 1

         ↳MRR

           →DP Problem 2

             ↳Neg POLO

...

               →DP Problem 5

                 ↳Modular Removal of Rules

Dependency Pairs:

F₀₁(x, f₁₁(y, z)) -> F₀₁(x, y)
F₀₁(x, f₀₁(y, z)) -> F₀₀(x, y)
F₀₀(x, f₁₀(y, z)) -> F₀₁(x, y)
F₀₀(x, f₀₀(y, z)) -> F₀₀(x, y)

Rules:

f₀₀(f₀₀(f₁₀(a, b), c), x) -> f₀₀(b, f₁₀(a, f₀₀(c, f₀₀(b, x))))
f₀₀(x, f₀₀(y, z)) -> f₀₀(f₀₀(x, y), z)
f₀₀(x, f₁₀(y, z)) -> f₁₀(f₀₁(x, y), z)
f₁₀(x, f₀₀(y, z)) -> f₀₀(f₁₀(x, y), z)
f₁₀(x, f₁₀(y, z)) -> f₁₀(f₁₁(x, y), z)
f₀₁(f₀₀(f₁₀(a, b), c), x) -> f₀₁(b, f₁₁(a, f₀₁(c, f₀₁(b, x))))
f₀₁(x, f₀₁(y, z)) -> f₀₁(f₀₀(x, y), z)
f₀₁(x, f₁₁(y, z)) -> f₁₁(f₀₁(x, y), z)
f₁₁(x, f₀₁(y, z)) -> f₀₁(f₁₀(x, y), z)
f₁₁(x, f₁₁(y, z)) -> f₁₁(f₁₁(x, y), z)

Strategy:

innermost

We have the following set of usable rules: none
To remove rules and DPs from this DP problem we used the following monotonic and C_E-compatible order: Polynomial ordering.
Polynomial interpretation:

POL(f_11(x₁, x₂)) = x₁ + x₂

POL(F_00(x₁, x₂)) = x₁ + x₂

POL(f_00(x₁, x₂)) = x₁ + x₂

POL(f_10(x₁, x₂)) = x₁ + x₂

POL(F_01(x₁, x₂)) = x₁ + x₂

POL(f_01(x₁, x₂)) = x₁ + x₂

We have the following set D of usable symbols: {F₀₀, F₀₁}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

F₀₁(x, f₁₁(y, z)) -> F₀₁(x, y)
F₀₁(x, f₀₁(y, z)) -> F₀₀(x, y)
F₀₀(x, f₁₀(y, z)) -> F₀₁(x, y)
F₀₀(x, f₀₀(y, z)) -> F₀₀(x, y)

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.

     ↳DPs

       →DP Problem 1

         ↳MRR

           →DP Problem 2

             ↳Neg POLO

...

               →DP Problem 6

                 ↳Modular Removal of Rules

Dependency Pairs:

F₁₁(x, f₁₁(y, z)) -> F₁₁(x, y)
F₁₁(x, f₀₁(y, z)) -> F₁₀(x, y)
F₀₁(f₀₀(f₁₀(a, b), c), x'') -> F₁₁(a, f₀₁(f₀₀(c, b), x''))
F₁₁(x, f₀₁(y, z)) -> F₀₁(f₁₀(x, y), z)
F₁₀(x, f₁₀(y, z)) -> F₁₁(x, y)
F₁₀(x, f₀₀(y, z)) -> F₁₀(x, y)
F₀₀(f₀₀(f₁₀(a, b), c), x'') -> F₁₀(a, f₀₀(f₀₀(c, b), x''))
F₁₀(x, f₀₀(y, z)) -> F₀₀(f₁₀(x, y), z)

Rules:

f₀₀(f₀₀(f₁₀(a, b), c), x) -> f₀₀(b, f₁₀(a, f₀₀(c, f₀₀(b, x))))
f₀₀(x, f₀₀(y, z)) -> f₀₀(f₀₀(x, y), z)
f₀₀(x, f₁₀(y, z)) -> f₁₀(f₀₁(x, y), z)
f₁₀(x, f₀₀(y, z)) -> f₀₀(f₁₀(x, y), z)
f₁₀(x, f₁₀(y, z)) -> f₁₀(f₁₁(x, y), z)
f₀₁(f₀₀(f₁₀(a, b), c), x) -> f₀₁(b, f₁₁(a, f₀₁(c, f₀₁(b, x))))
f₀₁(x, f₀₁(y, z)) -> f₀₁(f₀₀(x, y), z)
f₀₁(x, f₁₁(y, z)) -> f₁₁(f₀₁(x, y), z)
f₁₁(x, f₀₁(y, z)) -> f₀₁(f₁₀(x, y), z)
f₁₁(x, f₁₁(y, z)) -> f₁₁(f₁₁(x, y), z)

Strategy:

innermost

We have the following set of usable rules:

f₁₁(x, f₁₁(y, z)) -> f₁₁(f₁₁(x, y), z)
f₁₀(x, f₁₀(y, z)) -> f₁₀(f₁₁(x, y), z)
f₀₁(f₀₀(f₁₀(a, b), c), x) -> f₀₁(b, f₁₁(a, f₀₁(c, f₀₁(b, x))))
f₀₀(x, f₁₀(y, z)) -> f₁₀(f₀₁(x, y), z)
f₁₀(x, f₀₀(y, z)) -> f₀₀(f₁₀(x, y), z)
f₀₁(x, f₀₁(y, z)) -> f₀₁(f₀₀(x, y), z)
f₀₁(x, f₁₁(y, z)) -> f₁₁(f₀₁(x, y), z)
f₁₁(x, f₀₁(y, z)) -> f₀₁(f₁₀(x, y), z)
f₀₀(f₀₀(f₁₀(a, b), c), x) -> f₀₀(b, f₁₀(a, f₀₀(c, f₀₀(b, x))))
f₀₀(x, f₀₀(y, z)) -> f₀₀(f₀₀(x, y), z)

To remove rules and DPs from this DP problem we used the following monotonic and C_E-compatible order: Polynomial ordering.
Polynomial interpretation:

POL(f_11(x₁, x₂)) = 1 + x₁ + x₂

POL(c) = 0

POL(f_00(x₁, x₂)) = x₁ + x₂

POL(F_00(x₁, x₂)) = x₁ + x₂

POL(b) = 0

POL(F_11(x₁, x₂)) = 1 + x₁ + x₂

POL(f_10(x₁, x₂)) = 1 + x₁ + x₂

POL(f_01(x₁, x₂)) = x₁ + x₂

POL(F_01(x₁, x₂)) = x₁ + x₂

POL(F_10(x₁, x₂)) = 1 + x₁ + x₂

POL(a) = 0

We have the following set D of usable symbols: {f₁₁, c, F₀₀, f₀₀, b, F₁₁, f₁₀, F₀₁, f₀₁, F₁₀, a}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

F₁₁(x, f₁₁(y, z)) -> F₁₁(x, y)
F₁₀(x, f₁₀(y, z)) -> F₁₁(x, y)

No Rules can be deleted.

The result of this processor delivers two new DP problems.

     ↳DPs

       →DP Problem 1

         ↳MRR

           →DP Problem 2

             ↳Neg POLO

...

               →DP Problem 7

                 ↳Unlabel

Dependency Pairs:

F₁₀(x, f₀₀(y, z)) -> F₁₀(x, y)
F₀₀(f₀₀(f₁₀(a, b), c), x'') -> F₁₀(a, f₀₀(f₀₀(c, b), x''))
F₁₀(x, f₀₀(y, z)) -> F₀₀(f₁₀(x, y), z)

Rules:

f₀₀(f₀₀(f₁₀(a, b), c), x) -> f₀₀(b, f₁₀(a, f₀₀(c, f₀₀(b, x))))
f₀₀(x, f₀₀(y, z)) -> f₀₀(f₀₀(x, y), z)
f₀₀(x, f₁₀(y, z)) -> f₁₀(f₀₁(x, y), z)
f₁₀(x, f₀₀(y, z)) -> f₀₀(f₁₀(x, y), z)
f₁₀(x, f₁₀(y, z)) -> f₁₀(f₁₁(x, y), z)
f₀₁(f₀₀(f₁₀(a, b), c), x) -> f₀₁(b, f₁₁(a, f₀₁(c, f₀₁(b, x))))
f₀₁(x, f₀₁(y, z)) -> f₀₁(f₀₀(x, y), z)
f₀₁(x, f₁₁(y, z)) -> f₁₁(f₀₁(x, y), z)
f₁₁(x, f₀₁(y, z)) -> f₀₁(f₁₀(x, y), z)
f₁₁(x, f₁₁(y, z)) -> f₁₁(f₁₁(x, y), z)

Strategy:

innermost

Removed all semantic labels.

     ↳DPs

       →DP Problem 1

         ↳MRR

           →DP Problem 2

             ↳Neg POLO

...

               →DP Problem 10

                 ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pairs:
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(x, f(y, z)) -> F(x, y)

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:
innermost
Dependency Pairs:
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:
innermost

     ↳DPs

       →DP Problem 1

         ↳MRR

           →DP Problem 2

             ↳Neg POLO

...

               →DP Problem 8

                 ↳Unlabel

Dependency Pairs:

F₁₁(x, f₀₁(y, z)) -> F₀₁(f₁₀(x, y), z)
F₀₁(f₀₀(f₁₀(a, b), c), x'') -> F₁₁(a, f₀₁(f₀₀(c, b), x''))

Rules:

f₀₀(f₀₀(f₁₀(a, b), c), x) -> f₀₀(b, f₁₀(a, f₀₀(c, f₀₀(b, x))))
f₀₀(x, f₀₀(y, z)) -> f₀₀(f₀₀(x, y), z)
f₀₀(x, f₁₀(y, z)) -> f₁₀(f₀₁(x, y), z)
f₁₀(x, f₀₀(y, z)) -> f₀₀(f₁₀(x, y), z)
f₁₀(x, f₁₀(y, z)) -> f₁₀(f₁₁(x, y), z)
f₀₁(f₀₀(f₁₀(a, b), c), x) -> f₀₁(b, f₁₁(a, f₀₁(c, f₀₁(b, x))))
f₀₁(x, f₀₁(y, z)) -> f₀₁(f₀₀(x, y), z)
f₀₁(x, f₁₁(y, z)) -> f₁₁(f₀₁(x, y), z)
f₁₁(x, f₀₁(y, z)) -> f₀₁(f₁₀(x, y), z)
f₁₁(x, f₁₁(y, z)) -> f₁₁(f₁₁(x, y), z)

Strategy:

innermost

Removed all semantic labels.

     ↳DPs

       →DP Problem 1

         ↳MRR

           →DP Problem 2

             ↳Neg POLO

...

               →DP Problem 10

                 ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pairs:
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(x, f(y, z)) -> F(x, y)

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:
innermost
Dependency Pairs:
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:
innermost

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

POL(c)	= 0
POL(b)	= 0
POL(a)	= 1
POL(F(x₁, x₂))	= 1 + x₁ + x₂
POL(f(x₁, x₂))	= x₁ + x₂

POL(f_11(x₁, x₂))	= x₁ + x₂
POL(F_00(x₁, x₂))	= x₁ + x₂
POL(f_00(x₁, x₂))	= x₁ + x₂
POL(f_10(x₁, x₂))	= x₁ + x₂
POL(F_01(x₁, x₂))	= x₁ + x₂
POL(f_01(x₁, x₂))	= x₁ + x₂