Term Rewriting System R:

   [x, y]
   f(a) -> g(h(a))
   h(g(x)) -> g(h(f(x)))
   k(x, h(x), a) -> h(x)
   k(f(x), y, x) -> f(x)

Termination of R to be shown.


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

   k(x, h(x), a) -> h(x)
   k(f(x), y, x) -> f(x)

where the Polynomial interpretation:
POL(g(x_1)) = x_1
POL(k(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3
POL(a) = 0
POL(h(x_1)) = x_1
POL(f(x_1)) = x_1
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: 


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

Furthermore, R contains one SCC.


SCC1:

H(g(x)) -> H(f(x))

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

   H(g(x)) -> H(f(x))
one new Dependency Pair
is created:


   H(g(a)) -> H(g(h(a)))

The transformation is resulting in one subcycle:


SCC1.Nar1:

H(g(a)) -> H(g(h(a)))

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

   H(g(a)) -> H(g(h(a)))
no new Dependency Pairs
are created.

none
The transformation is resulting in no subcycles.




Termination of R successfully shown.


Duration: 0.938 seconds.