Term Rewriting System R:
[x, y]
f(f(x)) -> f(g(f(x), x))
f(f(x)) -> f(h(f(x), f(x)))
g(x, y) -> y
h(x, x) -> g(x, 0)

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

F(f(x)) -> F(g(f(x), x))
F(f(x)) -> G(f(x), x)
F(f(x)) -> F(h(f(x), f(x)))
F(f(x)) -> H(f(x), f(x))
H(x, x) -> G(x, 0)

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Negative Polynomial Order


Dependency Pairs:

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


Rules:


f(f(x)) -> f(g(f(x), x))
f(f(x)) -> f(h(f(x), f(x)))
g(x, y) -> y
h(x, x) -> g(x, 0)





The following Dependency Pairs can be strictly oriented using the given order.

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


Moreover, the following usable rules (regarding the implicit AFS) are oriented.

h(x, x) -> g(x, 0)
g(x, y) -> y
f(f(x)) -> f(g(f(x), x))
f(f(x)) -> f(h(f(x), f(x)))


Used ordering:
Polynomial Order with Interpretation:

POL( F(x1) ) = x1

POL( f(x1) ) = x1 + 1

POL( h(x1, x2) ) = 0

POL( g(x1, x2) ) = x2

POL( 0 ) = 0


This results in one new DP problem. 


   R
     ↳DPs
       →DP Problem 1
         ↳Neg POLO
           →DP Problem 2
             ↳Dependency Graph


Dependency Pair:


Rules:


f(f(x)) -> f(g(f(x), x))
f(f(x)) -> f(h(f(x), f(x)))
g(x, y) -> y
h(x, x) -> g(x, 0)





Using the Dependency Graph resulted in no new DP problems.

Termination of R successfully shown.
Duration:
0:00 minutes