R
↳Dependency Pair Analysis
H(f(f(x))) -> H(f(g(f(x))))
H(f(f(x))) -> F(g(f(x)))
F(g(f(x))) -> F(f(x))
R
↳DPs
→DP Problem 1
↳Polynomial Ordering
→DP Problem 2
↳Nar
F(g(f(x))) -> F(f(x))
h(f(f(x))) -> h(f(g(f(x))))
f(g(f(x))) -> f(f(x))
F(g(f(x))) -> F(f(x))
f(g(f(x))) -> f(f(x))
POL(g(x1)) = 1 POL(f(x1)) = 0 POL(F(x1)) = x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 3
↳Dependency Graph
→DP Problem 2
↳Nar
h(f(f(x))) -> h(f(g(f(x))))
f(g(f(x))) -> f(f(x))
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Narrowing Transformation
H(f(f(x))) -> H(f(g(f(x))))
h(f(f(x))) -> h(f(g(f(x))))
f(g(f(x))) -> f(f(x))
two new Dependency Pairs are created:
H(f(f(x))) -> H(f(g(f(x))))
H(f(f(x''))) -> H(f(f(x'')))
H(f(f(g(f(x''))))) -> H(f(g(f(f(x'')))))
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Nar
→DP Problem 4
↳Remaining Obligation(s)
H(f(f(g(f(x''))))) -> H(f(g(f(f(x'')))))
H(f(f(x''))) -> H(f(f(x'')))
h(f(f(x))) -> h(f(g(f(x))))
f(g(f(x))) -> f(f(x))