Term Rewriting System R:

   [x, y, z]
   f(f(f(a, x), y), z) -> f(f(x, z), f(y, z))
   f(f(b, x), y) -> x
   f(c, y) -> y

Termination of R to be shown.


This program has no overlaps, so it is sufficient to show innermost termination. 


R contains the following Dependency Pairs: 


   F(f(f(a, x), y), z) -> F(f(x, z), f(y, z))
   F(f(f(a, x), y), z) -> F(x, z)
   F(f(f(a, x), y), z) -> F(y, z)

Furthermore, R contains one SCC.


SCC1:

F(f(f(a, x), y), z) -> F(y, z)
F(f(f(a, x), y), z) -> F(x, z)
F(f(f(a, x), y), z) -> F(f(x, z), f(y, z))

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


Non-Termination of R could be shown.

Duration: 0.686 seconds.