Term Rewriting System R:

   [y, x, z]
   f(0, y) -> y
   f(x, 0) -> x
   f(i(x), y) -> i(x)
   f(f(x, y), z) -> f(x, f(y, z))
   f(g(x, y), z) -> g(f(x, z), f(y, z))
   f(1, g(x, y)) -> x
   f(2, g(x, y)) -> y

Termination of R to be shown.


R contains the following Dependency Pairs: 


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

Furthermore, R contains one SCC.


SCC1:

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

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

No rules need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
POL(g(x_1, x_2)) = 1 + x_1 + x_2
POL(1) = 0
POL(i(x_1)) = 0
POL(F(x_1, x_2)) = 1 + x_1
POL(f(x_1, x_2)) = 1 + x_1 + x_2
POL(2) = 0
POL(0) = 0

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 0.566 seconds.