Term Rewriting System R:
[x, y]
f(a) -> g(h(a))
h(g(x)) -> g(h(f(x)))
k(x, h(x), a) -> h(x)
k(f(x), y, x) -> f(x)
Innermost Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
F(a) -> H(a)
H(g(x)) -> H(f(x))
H(g(x)) -> F(x)
Furthermore, R contains one SCC.
R
↳DPs
→DP Problem 1
↳Narrowing Transformation
Dependency Pair:
H(g(x)) -> H(f(x))
Rules:
f(a) -> g(h(a))
h(g(x)) -> g(h(f(x)))
k(x, h(x), a) -> h(x)
k(f(x), y, x) -> f(x)
Strategy:
innermost
On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule
H(g(x)) -> H(f(x))
one new Dependency Pair
is created:
H(g(a)) -> H(g(h(a)))
The transformation is resulting in one new DP problem:
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Narrowing Transformation
Dependency Pair:
H(g(a)) -> H(g(h(a)))
Rules:
f(a) -> g(h(a))
h(g(x)) -> g(h(f(x)))
k(x, h(x), a) -> h(x)
k(f(x), y, x) -> f(x)
Strategy:
innermost
On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule
H(g(a)) -> H(g(h(a)))
no new Dependency Pairs
are created.
The transformation is resulting in no new DP problems.
Innermost Termination of R successfully shown.
Duration:
0:00 minutes