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. 



   TRS
     ↳Reversing
     ↳Rev
     ↳RRRPolo




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
     ↳RRRPolo




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
     ↳Removing Redundant Rules



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

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

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

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


   TRS
     ↳Rev
     ↳Rev
     ↳RRRPolo
       →TRS4
         ↳Removing Redundant Rules



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

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

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

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


   TRS
     ↳Rev
     ↳Rev
     ↳RRRPolo
       →TRS4
         ↳RRRPolo
           →TRS5
             ↳Removing Redundant Rules



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

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

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

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


   TRS
     ↳Rev
     ↳Rev
     ↳RRRPolo
       →TRS4
         ↳RRRPolo
           →TRS5
             ↳RRRPolo
             ...
               →TRS6
                 ↳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
     ↳RRRPolo
       →TRS4
         ↳RRRPolo
           →TRS5
             ↳RRRPolo
             ...
               →DP Problem 1
                 ↳Negative Polynomial Order


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





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.

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


Used ordering:
Polynomial Order with Interpretation:

POL( B(x1) ) = x1

POL( c(x1) ) = x1 + 1

POL( A(x1) ) = 0

POL( a(x1) ) = 0

POL( C(x1) ) = 0

POL( b(x1) ) = x1


This results in one new DP problem. 


   TRS
     ↳Rev
     ↳Rev
     ↳RRRPolo
       →TRS4
         ↳RRRPolo
           →TRS5
             ↳RRRPolo
             ...
               →DP Problem 2
                 ↳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)))





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


   TRS
     ↳Rev
     ↳Rev
     ↳RRRPolo
       →TRS4
         ↳RRRPolo
           →TRS5
             ↳RRRPolo
             ...
               →DP Problem 3
                 ↳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)))





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


Used ordering:
Polynomial Order with Interpretation:

POL( A(x1) ) = x1

POL( b(x1) ) = x1 + 1

POL( a(x1) ) = x1

POL( c(x1) ) = 0


This results in one new DP problem. 


   TRS
     ↳Rev
     ↳Rev
     ↳RRRPolo
       →TRS4
         ↳RRRPolo
           →TRS5
             ↳RRRPolo
             ...
               →DP Problem 5
                 ↳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)))





Using the Dependency Graph resulted in no new DP problems.


   TRS
     ↳Rev
     ↳Rev
     ↳RRRPolo
       →TRS4
         ↳RRRPolo
           →TRS5
             ↳RRRPolo
             ...
               →DP Problem 4
                 ↳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)))





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.

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


Used ordering:
Polynomial Order with Interpretation:

POL( C(x1) ) = x1

POL( a(x1) ) = x1 + 1

POL( c(x1) ) = x1

POL( b(x1) ) = 0


This results in one new DP problem.

Termination of R successfully shown.
Duration:
0:02 minutes