Term Rewriting System R:

   [x, y, z]
   :(:(x, y), z) -> :(x, :(y, z))
   :(+(x, y), z) -> +(:(x, z), :(y, z))
   :(z, +(x, f(y))) -> :(g(z, y), +(x, a))

Termination of R to be shown.


R contains the following Dependency Pairs: 


   :'(z, +(x, f(y))) -> :'(g(z, y), +(x, a))
   :'(:(x, y), z) -> :'(x, :(y, z))
   :'(:(x, y), z) -> :'(y, z)
   :'(+(x, y), z) -> :'(x, z)
   :'(+(x, y), z) -> :'(y, z)

Furthermore, R contains one SCC.


SCC1:

:'(+(x, y), z) -> :'(y, z)
:'(+(x, y), z) -> :'(x, z)
:'(:(x, y), z) -> :'(y, z)
:'(:(x, y), z) -> :'(x, :(y, 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)) = 0
POL(:(x_1, x_2)) = 1 + x_1 + x_2
POL(a) = 0
POL(:'(x_1, x_2)) = x_1
POL(+(x_1, x_2)) = 1 + x_1 + x_2
POL(f(x_1)) = 0

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 0.545 seconds.