Term Rewriting System R:

   [X]
   g(X) -> h(X)
   c -> d
   h(d) -> g(c)

Termination of R to be shown.


This program has no overlaps, so it is sufficient to show innermost termination. 


R contains the following Dependency Pairs: 


   G(X) -> H(X)
   H(d) -> G(c)
   H(d) -> C

Furthermore, R contains one SCC.


SCC1:

H(d) -> G(c)
G(X) -> H(X)

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

   H(d) -> G(c)
one new Dependency Pair
is created:


   H(d) -> G(d)

The transformation is resulting in one subcycle:


SCC1.Rewr1:

H(d) -> G(d)
G(X) -> H(X)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(G(x_1)) = x_1
POL(d) = 0
POL(H(x_1)) = x_1

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   c -> d


 This transformation is resulting in one new subcycle:


SCC1.Rewr1.MRR1:

G(X) -> H(X)
H(d) -> G(d)

Found an infinite P-chain over R:
P = G(X) -> H(X)
H(d) -> G(d)
R = []
s = G(d) evaluates to t = G(d)
Thus, s starts an infinite reduction.


Non-Termination of R could be shown.

Duration: 0.802 seconds.