Term Rewriting System R:

   [X]
   f(g(X)) -> g(f(f(X)))
   f(h(X)) -> h(g(X))

Termination of R to be shown.



Rule(s) before reversing: 

   f(g(X)) -> g(f(f(X)))
   f(h(X)) -> h(g(X))


Rule(s) after reversing: 

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


Termination could be shown with a Match Bound of 1.
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
75, 76, 77, 78, 79, 80, 81, 82

Node 75 is start node and node 76 is final node.

Those nodes are connect through the following edges:

* 76 to 76 labelled #(0)
* 75 to 77 labelled f(0)
* 77 to 78 labelled f(0)
* 78 to 76 labelled g(0)
* 75 to 79 labelled g(0)
* 79 to 76 labelled h(0)
* 78 to 80 labelled f(1)
* 80 to 81 labelled f(1)
* 81 to 76 labelled g(1)
* 79 to 82 labelled g(1)
* 82 to 76 labelled h(1)
* 82 to 82 labelled g(1)
* 81 to 80 labelled f(1)




Termination of R successfully shown.


Duration: 0.483 seconds.