R
↳Dependency Pair Analysis
F(s(0), g(x)) -> F(x, g(x))
G(s(x)) -> G(x)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳Remaining
G(s(x)) -> G(x)
f(s(0), g(x)) -> f(x, g(x))
g(s(x)) -> g(x)
G(s(x)) -> G(x)
f(s(0), g(x)) -> f(x, g(x))
g(s(x)) -> g(x)
POL(g(x1)) = x1 POL(G(x1)) = x1 POL(s(x1)) = 1 + x1
G(x1) -> G(x1)
s(x1) -> s(x1)
f(x1, x2) -> x2
g(x1) -> g(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳Dependency Graph
→DP Problem 2
↳Remaining
f(s(0), g(x)) -> f(x, g(x))
g(s(x)) -> g(x)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Remaining Obligation(s)
F(s(0), g(x)) -> F(x, g(x))
f(s(0), g(x)) -> f(x, g(x))
g(s(x)) -> g(x)