Term Rewriting System R:

   [X, Y]
   f(0, 1, X) -> h(X, X)
   h(0, X) -> f(0, X, X)
   g(X, Y) -> X
   g(X, Y) -> Y

Termination of R to be shown.


R contains the following Dependency Pairs: 


   F(0, 1, X) -> H(X, X)
   H(0, X) -> F(0, X, X)

Furthermore, R contains one SCC.


SCC1:

H(0, X) -> F(0, X, X)
F(0, 1, X) -> H(X, X)

Found an infinite P-chain over R:
P = H(0, X) -> F(0, X, X)
F(0, 1, X) -> H(X, X)
R = [f(0, 1, X) -> h(X, X), h(0, X) -> f(0, X, X), g(X, Y) -> Y, g(X, Y) -> X]
s = H(0, g(0, 1)) evaluates to t = H(0, g(0, 1))
Thus, s starts an infinite reduction.


Non-Termination of R could be shown.

Duration: 0.945 seconds.