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