Termination Proof using AProVE

Term Rewriting System R:
[x]
a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x

Innermost Termination of R to be shown.

TRS

     ↳Reversing

     ↳Rev

     ↳DPs

Rule(s) before reversing:

a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x

Rule(s) after reversing:

b'(a'(x)) -> a'(a'(b'(x)))
b'(v'(x)) -> x
a'(c'(x)) -> c'(c'(a'(x)))
a'(u'(x)) -> x
u'(a'(x)) -> x
c'(b'(x)) -> b'(b'(c'(x)))
c'(w'(x)) -> x
v'(b'(x)) -> x
w'(c'(x)) -> x

Trying another alternative:

TRS

     ↳Rev

     ↳Reversing

     ↳DPs

Rule(s) before reversing:

a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x

Rule(s) after reversing:

b'(a'(x)) -> a'(a'(b'(x)))
b'(v'(x)) -> x
a'(c'(x)) -> c'(c'(a'(x)))
a'(u'(x)) -> x
u'(a'(x)) -> x
c'(b'(x)) -> b'(b'(c'(x)))
c'(w'(x)) -> x
v'(b'(x)) -> x
w'(c'(x)) -> x

Trying another alternative:

TRS

     ↳Rev

     ↳Rev

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

A(b(x)) -> B(a(a(x)))
A(b(x)) -> A(a(x))
A(b(x)) -> A(x)
B(c(x)) -> C(b(b(x)))
B(c(x)) -> B(b(x))
B(c(x)) -> B(x)
C(a(x)) -> A(c(c(x)))
C(a(x)) -> C(c(x))
C(a(x)) -> C(x)

Furthermore, R contains one SCC.

TRS

     ↳Rev

     ↳Rev

     ↳DPs

       →DP Problem 1

         ↳Usable Rules (Innermost)

Dependency Pairs:

B(c(x)) -> B(x)
B(c(x)) -> B(b(x))
C(a(x)) -> C(x)
C(a(x)) -> C(c(x))
A(b(x)) -> A(x)
A(b(x)) -> A(a(x))
C(a(x)) -> A(c(c(x)))
B(c(x)) -> C(b(b(x)))
A(b(x)) -> B(a(a(x)))

Rules:

a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(c(x)) -> c(b(b(x)))
b(v(x)) -> x
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x

Strategy:

innermost

As we are in the innermost case, we can delete all 3 non-usable-rules.

TRS

     ↳Rev

     ↳Rev

     ↳DPs

       →DP Problem 1

         ↳UsableRules

           →DP Problem 2

             ↳Modular Removal of Rules

Dependency Pairs:

Rules:

a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(v(x)) -> x
b(c(x)) -> c(b(b(x)))
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x

Strategy:

innermost

We have the following set of usable rules:

a(b(x)) -> b(a(a(x)))
a(u(x)) -> x
b(v(x)) -> x
b(c(x)) -> c(b(b(x)))
c(a(x)) -> a(c(c(x)))
c(w(x)) -> x

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(x₁)) = x₁

POL(C(x₁)) = x₁

POL(B(x₁)) = x₁

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

POL(b(x₁)) = x₁

POL(a(x₁)) = x₁

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

POL(A(x₁)) = x₁

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

We have the following set D of usable symbols: {c, C, B, b, a, A}
No Dependency Pairs can be deleted.
The following rules can be deleted as they contain symbols in their lhs which do not occur in D:

a(u(x)) -> x
b(v(x)) -> x
c(w(x)) -> x

The result of this processor delivers one new DP problem.

TRS

     ↳Rev

     ↳Rev

     ↳DPs

       →DP Problem 1

         ↳UsableRules

           →DP Problem 2

             ↳MRR

...

               →DP Problem 3

                 ↳Negative Polynomial Order

Dependency Pairs:

Rules:

a(b(x)) -> b(a(a(x)))
b(c(x)) -> c(b(b(x)))
c(a(x)) -> a(c(c(x)))

Strategy:

innermost

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

B(c(x)) -> B(x)
B(c(x)) -> B(b(x))
B(c(x)) -> C(b(b(x)))

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

a(b(x)) -> b(a(a(x)))
c(a(x)) -> a(c(c(x)))
b(c(x)) -> c(b(b(x)))

Used ordering:
Polynomial Order with Interpretation:

POL( B(x₁) ) = x₁

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

POL( A(x₁) ) = 0

POL( a(x₁) ) = 0

POL( C(x₁) ) = 0

POL( b(x₁) ) = x₁

This results in one new DP problem.

TRS

     ↳Rev

     ↳Rev

     ↳DPs

       →DP Problem 1

         ↳UsableRules

           →DP Problem 2

             ↳MRR

...

               →DP Problem 4

                 ↳Dependency Graph

Dependency Pairs:

C(a(x)) -> C(x)
C(a(x)) -> C(c(x))
A(b(x)) -> A(x)
A(b(x)) -> A(a(x))
C(a(x)) -> A(c(c(x)))
A(b(x)) -> B(a(a(x)))

Rules:

a(b(x)) -> b(a(a(x)))
b(c(x)) -> c(b(b(x)))
c(a(x)) -> a(c(c(x)))

Strategy:

innermost

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

TRS

     ↳Rev

     ↳Rev

     ↳DPs

       →DP Problem 1

         ↳UsableRules

           →DP Problem 2

             ↳MRR

...

               →DP Problem 5

                 ↳Negative Polynomial Order

Dependency Pairs:

A(b(x)) -> A(x)
A(b(x)) -> A(a(x))

Rules:

a(b(x)) -> b(a(a(x)))
b(c(x)) -> c(b(b(x)))
c(a(x)) -> a(c(c(x)))

Strategy:

innermost

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

A(b(x)) -> A(x)
A(b(x)) -> A(a(x))

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

a(b(x)) -> b(a(a(x)))
c(a(x)) -> a(c(c(x)))
b(c(x)) -> c(b(b(x)))

Used ordering:
Polynomial Order with Interpretation:

POL( A(x₁) ) = x₁

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

POL( a(x₁) ) = x₁

POL( c(x₁) ) = 0

This results in one new DP problem.

TRS

     ↳Rev

     ↳Rev

     ↳DPs

       →DP Problem 1

         ↳UsableRules

           →DP Problem 2

             ↳MRR

...

               →DP Problem 7

                 ↳Dependency Graph

Dependency Pair:

Rules:

a(b(x)) -> b(a(a(x)))
b(c(x)) -> c(b(b(x)))
c(a(x)) -> a(c(c(x)))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

TRS

     ↳Rev

     ↳Rev

     ↳DPs

       →DP Problem 1

         ↳UsableRules

           →DP Problem 2

             ↳MRR

...

               →DP Problem 6

                 ↳Negative Polynomial Order

Dependency Pairs:

C(a(x)) -> C(c(x))
C(a(x)) -> C(x)

Rules:

a(b(x)) -> b(a(a(x)))
b(c(x)) -> c(b(b(x)))
c(a(x)) -> a(c(c(x)))

Strategy:

innermost

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

C(a(x)) -> C(c(x))
C(a(x)) -> C(x)

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

a(b(x)) -> b(a(a(x)))
c(a(x)) -> a(c(c(x)))
b(c(x)) -> c(b(b(x)))

Used ordering:
Polynomial Order with Interpretation:

POL( C(x₁) ) = x₁

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

POL( c(x₁) ) = x₁

POL( b(x₁) ) = 0

This results in one new DP problem.

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

POL(c(x₁))	= x₁
POL(C(x₁))	= x₁
POL(B(x₁))	= x₁
POL(v(x₁))	= 1 + x₁
POL(b(x₁))	= x₁
POL(a(x₁))	= x₁
POL(w(x₁))	= 1 + x₁
POL(A(x₁))	= x₁
POL(u(x₁))	= 1 + x₁