R
↳Dependency Pair Analysis
F(c(X, s(Y))) -> F(c(s(X), Y))
G(c(s(X), Y)) -> F(c(X, s(Y)))
R
↳DPs
→DP Problem 1
↳Instantiation Transformation
F(c(X, s(Y))) -> F(c(s(X), Y))
f(c(X, s(Y))) -> f(c(s(X), Y))
g(c(s(X), Y)) -> f(c(X, s(Y)))
one new Dependency Pair is created:
F(c(X, s(Y))) -> F(c(s(X), Y))
F(c(s(X''), s(Y''))) -> F(c(s(s(X'')), Y''))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳Remaining Obligation(s)
F(c(s(X''), s(Y''))) -> F(c(s(s(X'')), Y''))
f(c(X, s(Y))) -> f(c(s(X), Y))
g(c(s(X), Y)) -> f(c(X, s(Y)))