R
↳Dependency Pair Analysis
A -> G(c)
F(g(X), b) -> F(a, X)
F(g(X), b) -> A
R
↳DPs
→DP Problem 1
↳Narrowing Transformation
F(g(X), b) -> F(a, X)
a -> g(c)
g(a) -> b
f(g(X), b) -> f(a, X)
one new Dependency Pair is created:
F(g(X), b) -> F(a, X)
F(g(X), b) -> F(g(c), X)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Argument Filtering and Ordering
F(g(X), b) -> F(g(c), X)
a -> g(c)
g(a) -> b
f(g(X), b) -> f(a, X)
F(g(X), b) -> F(g(c), X)
g(a) -> b
a -> g(c)
f(g(X), b) -> f(a, X)
POL(c) = 0 POL(g(x1)) = x1 POL(b) = 1 POL(a) = 1 POL(F(x1, x2)) = 1 + x1 + x2 POL(f(x1, x2)) = x1 + x2
F(x1, x2) -> F(x1, x2)
g(x1) -> g(x1)
a -> a
f(x1, x2) -> f(x1, x2)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳AFS
...
→DP Problem 3
↳Dependency Graph
a -> g(c)
g(a) -> b
f(g(X), b) -> f(a, X)