Term Rewriting System R:

   [x]
   f(f(x)) -> f(c(f(x)))
   f(f(x)) -> f(d(f(x)))
   g(c(x)) -> x
   g(d(x)) -> x
   g(c(0)) -> g(d(1))
   g(c(1)) -> g(d(0))

Termination of R to be shown.


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

   g(c(x)) -> x
   g(d(x)) -> x

where the Polynomial interpretation:
POL(g(x_1)) = 1 + x_1
POL(1) = 0
POL(d(x_1)) = x_1
POL(f(x_1)) = x_1
POL(c(x_1)) = x_1
POL(0) = 0
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: 


   G(c(1)) -> G(d(0))
   G(c(0)) -> G(d(1))
   F(f(x)) -> F(c(f(x)))
   F(f(x)) -> F(d(f(x)))

R contains no SCCs.




Termination of R successfully shown.


Duration: 0.494 seconds.