Term Rewriting System R:

   [x, y]
   f(g(x)) -> g(f(f(x)))
   f(h(x)) -> h(g(x))
   f'(s(x), y, y) -> f'(y, x, s(x))

Termination of R to be shown.


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

   f'(s(x), y, y) -> f'(y, x, s(x))

where the Polynomial interpretation:
POL(g(x_1)) = x_1
POL(s(x_1)) = 1 + x_1
POL(h(x_1)) = x_1
POL(f(x_1)) = x_1
POL(f'(x_1, x_2, x_3)) = 1 + 2*x_1 + x_2 + x_3
was used. 



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


This program has no overlaps, so it is sufficient to show innermost termination. 


R contains the following Dependency Pairs: 


   F(g(x)) -> F(f(x))
   F(g(x)) -> F(x)

Furthermore, R contains one SCC.


SCC1:

F(g(x)) -> F(x)
F(g(x)) -> F(f(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: 

   f(h(x)) -> h(g(x))
   f(g(x)) -> g(f(f(x)))


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(g(x_1)) = 1 + x_1
POL(h(x_1)) = 0
POL(F(x_1)) = 1 + x_1
POL(f(x_1)) = x_1

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 0.553 seconds.