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

Termination of R to be shown.


Removing the following rules from R which fullfill a polynomial ordering: 

   c(w(x)) -> x
   w(c(x)) -> x

where the Polynomial interpretation:
POL(b(x_1)) = x_1
POL(v(x_1)) = x_1
POL(a(x_1)) = x_1
POL(w(x_1)) = 1 + x_1
POL(u(x_1)) = x_1
POL(c(x_1)) = x_1
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   a(u(x)) -> x
   u(a(x)) -> x

where the Polynomial interpretation:
POL(b(x_1)) = x_1
POL(v(x_1)) = x_1
POL(a(x_1)) = x_1
POL(u(x_1)) = 1 + x_1
POL(c(x_1)) = x_1
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   b(v(x)) -> x
   v(b(x)) -> x

where the Polynomial interpretation:
POL(b(x_1)) = x_1
POL(v(x_1)) = 1 + x_1
POL(a(x_1)) = x_1
POL(c(x_1)) = x_1
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


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.


SCC1:

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

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

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


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(b(x_1)) = x_1
POL(B(x_1)) = x_1
POL(a(x_1)) = 0
POL(A(x_1)) = 0
POL(c(x_1)) = 1 + x_1
POL(C(x_1)) = 0

 resulting in two subcycles.


SCC1.Polo1:

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

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

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


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(b(x_1)) = 1 + x_1
POL(a(x_1)) = x_1
POL(A(x_1)) = 1 + x_1
POL(c(x_1)) = 0

 resulting in no subcycles.


SCC1.Polo2:

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

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

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


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(b(x_1)) = 0
POL(a(x_1)) = 1 + x_1
POL(c(x_1)) = x_1
POL(C(x_1)) = 1 + x_1

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 1.8 seconds.