Term Rewriting System R:

   [X, Y]
   f(0, 1, X) -> f(g(X, X), 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) -> F(g(X, X), X, X)
   F(0, 1, X) -> G(X, X)

Furthermore, R contains one SCC.


SCC1:

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

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


Non-Termination of R could be shown.

Duration: 0.792 seconds.