Term Rewriting System R:

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

Innermost Termination of R to be shown.


R contains the following Dependency Pairs: 


   H(x, y) -> F(x, y, x)
   F(0, 1, x) -> H(x, x)

Furthermore, R contains one SCC.


SCC1:

F(0, 1, x) -> H(x, x)
H(x, y) -> F(x, y, x)

On this Scc, a Instantiation SCC transformation can be performed.
 
As a result of transforming the rule 

   H(x, y) -> F(x, y, x)
one new Dependency Pair
is created:


   H(y', y') -> F(y', y', y')

The transformation is resulting in no subcycles.




Innermost Termination of R successfully shown.


Duration: 0.391 seconds.