Termination Proof using AProVE

Term Rewriting System R:
[x, y, z]
f(f(a, a), x) -> f(a, f(b, f(a, 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(a, a), x) -> F(a, f(b, f(a, x)))
F(f(a, a), x) -> F(b, f(a, x))
F(f(a, a), x) -> F(a, 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(a, a), x) -> F(a, x)
F(x, f(y, z)) -> F(x, y)
F(f(a, a), x) -> F(b, f(a, x))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(a, a), x) -> F(a, f(b, f(a, x)))

Rules:

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

Strategy:

innermost

We have the following set of usable rules:

f(f(a, a), x) -> f(a, f(b, f(a, 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(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: {b, a, F, f}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

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

No Rules can be deleted.

The result of this processor delivers one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳MRR

           →DP Problem 2

             ↳Narrowing Transformation

Dependency Pairs:

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

Rules:

f(f(a, a), x) -> f(a, f(b, f(a, 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(a, a), x) -> F(a, f(b, f(a, x)))

two new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳MRR

           →DP Problem 2

             ↳Nar

...

               →DP Problem 3

                 ↳Semantic Labelling

Dependency Pairs:

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

Rules:

f(f(a, a), x) -> f(a, f(b, f(a, 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₁) = 1

f(x₀, x₁) = 1

a = 0

b = 1

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

     ↳DPs

       →DP Problem 1

         ↳MRR

           →DP Problem 2

             ↳Nar

...

               →DP Problem 4

                 ↳Modular Removal of Rules

Dependency Pairs:

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

Rules:

f₁₀(f₀₀(a, a), x) -> f₀₁(a, f₁₁(b, f₀₀(a, 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₀₀(a, a), x) -> f₀₁(a, f₁₁(b, f₀₁(a, 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_11(x₁, x₂)) = x₁ + x₂

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

We have the following set D of usable symbols: {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)

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

             ↳Nar

...

               →DP Problem 5

                 ↳Unlabel

Dependency Pairs:

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

Rules:

f₁₀(f₀₀(a, a), x) -> f₀₁(a, f₁₁(b, f₀₀(a, 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₀₀(a, a), x) -> f₀₁(a, f₁₁(b, f₀₁(a, 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

             ↳Nar

...

               →DP Problem 6

                 ↳Semantic Labelling

Dependency Pairs:

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

Rules:

f(f(a, a), x) -> f(a, f(b, f(a, 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

F(x₀, x₁) = 1 + x₀

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

     ↳DPs

       →DP Problem 1

         ↳MRR

           →DP Problem 2

             ↳Nar

...

               →DP Problem 7

                 ↳Modular Removal of Rules

Dependency Pairs:

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

Rules:

f₁₀(f₁₁(a, a), x) -> f₁₀(a, f₀₁(b, f₁₀(a, x)))
f₁₀(x, f₀₀(y, z)) -> f₁₀(f₁₀(x, y), z)
f₁₀(x, f₀₁(y, z)) -> f₁₁(f₁₀(x, y), z)
f₁₁(f₁₁(a, a), x) -> f₁₀(a, f₀₁(b, f₁₁(a, 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₀₀(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_00(x₁, x₂)) = x₁ + x₂

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

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

We have the following set D of usable symbols: {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)

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

             ↳Nar

...

               →DP Problem 8

                 ↳Modular Removal of Rules

Dependency Pairs:

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

Rules:

f₁₀(f₁₁(a, a), x) -> f₁₀(a, f₀₁(b, f₁₀(a, x)))
f₁₀(x, f₀₀(y, z)) -> f₁₀(f₁₀(x, y), z)
f₁₀(x, f₀₁(y, z)) -> f₁₁(f₁₀(x, y), z)
f₁₁(f₁₁(a, a), x) -> f₁₀(a, f₀₁(b, f₁₁(a, 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₀₀(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_10(x₁, x₂)) = x₁ + x₂

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

We have the following set D of usable symbols: {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)

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

             ↳Nar

...

               →DP Problem 9

                 ↳Modular Removal of Rules

Dependency Pairs:

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

Rules:

f₁₀(f₁₁(a, a), x) -> f₁₀(a, f₀₁(b, f₁₀(a, x)))
f₁₀(x, f₀₀(y, z)) -> f₁₀(f₁₀(x, y), z)
f₁₀(x, f₀₁(y, z)) -> f₁₁(f₁₀(x, y), z)
f₁₁(f₁₁(a, a), x) -> f₁₀(a, f₀₁(b, f₁₁(a, 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₀₀(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_11(x₁, x₂)) = x₁ + x₂

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

We have the following set D of usable symbols: {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)

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

             ↳Nar

...

               →DP Problem 10

                 ↳Modular Removal of Rules

Dependency Pairs:

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

Rules:

f₁₀(f₁₁(a, a), x) -> f₁₀(a, f₀₁(b, f₁₀(a, x)))
f₁₀(x, f₀₀(y, z)) -> f₁₀(f₁₀(x, y), z)
f₁₀(x, f₀₁(y, z)) -> f₁₁(f₁₀(x, y), z)
f₁₁(f₁₁(a, a), x) -> f₁₀(a, f₀₁(b, f₁₁(a, 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₀₀(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₀₀(x, f₀₁(y, z)) -> f₀₁(f₀₀(x, y), z)
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₂)) = x₁ + x₂

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

POL(b) = 0

POL(f_10(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₀₀, b, f₀₁, F₁₀, a}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

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

The following rules can be deleted as they contain symbols in their lhs which do not occur in D:

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

6 non usable rules have been deleted.

The result of this processor delivers one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳MRR

           →DP Problem 2

             ↳Nar

...

               →DP Problem 11

                 ↳Modular Removal of Rules

Dependency Pairs:

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

Rules:

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_00(x₁, x₂)) = x₁ + x₂

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

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

We have the following set D of usable symbols: {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)

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.

Innermost Termination of R successfully shown.
Duration:
0:31 minutes

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_11(x₁, x₂))	= x₁ + x₂
POL(f_10(x₁, x₂))	= x₁ + x₂

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