R
↳Dependency Pair Analysis
F(g(x), s(0), y) -> F(y, y, g(x))
G(s(x)) -> G(x)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳FwdInst
G(s(x)) -> G(x)
f(g(x), s(0), y) -> f(y, y, g(x))
g(s(x)) -> s(g(x))
g(0) -> 0
G(s(x)) -> G(x)
f(g(x), s(0), y) -> f(y, y, g(x))
g(s(x)) -> s(g(x))
g(0) -> 0
G(x1) -> G(x1)
s(x1) -> s(x1)
f(x1, x2, x3) -> f
g(x1) -> x1
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳Dependency Graph
→DP Problem 2
↳FwdInst
f(g(x), s(0), y) -> f(y, y, g(x))
g(s(x)) -> s(g(x))
g(0) -> 0
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Forward Instantiation Transformation
F(g(x), s(0), y) -> F(y, y, g(x))
f(g(x), s(0), y) -> f(y, y, g(x))
g(s(x)) -> s(g(x))
g(0) -> 0
one new Dependency Pair is created:
F(g(x), s(0), y) -> F(y, y, g(x))
F(g(x'), s(0), g(x'''')) -> F(g(x''''), g(x''''), g(x'))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳FwdInst
→DP Problem 4
↳Remaining Obligation(s)
F(g(x'), s(0), g(x'''')) -> F(g(x''''), g(x''''), g(x'))
f(g(x), s(0), y) -> f(y, y, g(x))
g(s(x)) -> s(g(x))
g(0) -> 0