Term Rewriting System R:

   [x, y]
   f(g(x), x, y) -> f(y, y, g(y))
   g(g(x)) -> g(x)

Innermost Termination of R to be shown.


R contains the following Dependency Pairs: 


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

R contains no SCCs.




Innermost Termination of R successfully shown.


Duration: 0.345 seconds.