Term Rewriting System R:

   [x, y]
   f(a) -> b
   f(c) -> d
   f(g(x, y)) -> g(f(x), f(y))
   f(h(x, y)) -> g(h(y, f(x)), h(x, f(y)))
   g(x, x) -> h(e, x)

Termination of R to be shown.


R contains the following Dependency Pairs: 


   F(h(x, y)) -> G(h(y, f(x)), h(x, f(y)))
   F(h(x, y)) -> F(x)
   F(h(x, y)) -> F(y)
   F(g(x, y)) -> G(f(x), f(y))
   F(g(x, y)) -> F(x)
   F(g(x, y)) -> F(y)

Furthermore, R contains one SCC.


SCC1:

F(g(x, y)) -> F(y)
F(g(x, y)) -> F(x)
F(h(x, y)) -> F(y)
F(h(x, y)) -> F(x)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(g(x_1, x_2)) = 1 + x_1 + x_2
POL(F(x_1)) = 1 + x_1
POL(h(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   F(g(x, y)) -> F(y)
   F(g(x, y)) -> F(x)
   F(h(x, y)) -> F(y)
   F(h(x, y)) -> F(x)



 This transformation is resulting in no new subcycles.




Termination of R successfully shown.


Duration: 0.532 seconds.