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)

Innermost 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
         ↳Narrowing Transformation


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)


Strategy:

innermost




On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

F(f(x)) -> F(g(f(x), x))
three new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Narrowing Transformation


Dependency Pair:

F(f(x)) -> F(h(f(x), f(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)


Strategy:

innermost




On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

F(f(x)) -> F(h(f(x), f(x)))
five new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 3
                 ↳Narrowing Transformation


Dependency Pair:

F(f(x'')) -> F(g(f(x''), 0))


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)


Strategy:

innermost




On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

F(f(x'')) -> F(g(f(x''), 0))
three new Dependency Pairs are created:

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

The transformation is resulting in no new DP problems.


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