Term Rewriting System R:

   [x, y, z]
   f(g(x), h(x), y, x) -> f(y, y, y, x)
   f(x, y, z, 0) -> 2
   g(0) -> 2
   h(0) -> 2

Termination of R to be shown.


R contains the following Dependency Pairs: 


   F(g(x), h(x), y, x) -> F(y, y, y, x)

R contains no SCCs.




Termination of R successfully shown.


Duration: 0.409 seconds.