Term Rewriting System R:

   [x, y]
   f(g(x), x, y) -> f(y, y, g(y))
   g(g(x)) -> g(x)

Termination of R to be shown.


R contains the following Dependency Pairs: 


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

Furthermore, R contains one SCC.


SCC1:

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

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


Non-Termination of R could be shown.

Duration: 0.465 seconds.