Term Rewriting System R:

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

Termination of R to be shown.


R contains the following Dependency Pairs: 


   H(x, y) -> F(x, y, x)
   F(0, 1, x) -> H(x, x)

Furthermore, R contains one SCC.


SCC1:

F(0, 1, x) -> H(x, x)
H(x, y) -> F(x, y, x)

Found an infinite P-chain over R:
P = F(0, 1, x) -> H(x, x)
H(x, y) -> F(x, y, x)
R = [h(x, y) -> f(x, y, x), f(0, 1, x) -> h(x, x), g(x, y) -> y, g(x, y) -> 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.803 seconds.