Term Rewriting System R:

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

Termination of R to be shown.


R contains the following Dependency Pairs: 


   F(s(x)) -> F(g(x, x))
   F(s(x)) -> G(x, x)

Furthermore, R contains one SCC.


SCC1:

F(s(x)) -> F(g(x, x))

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


Non-Termination of R could be shown.

Duration: 0.522 seconds.