Term Rewriting System R:

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

Termination of R to be shown.


R contains the following Dependency Pairs: 


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

Furthermore, R contains one SCC.


SCC1:

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

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


Non-Termination of R could be shown.

Duration: 0.437 seconds.