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
↳Forward Instantiation Transformation
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)))
one new Dependency Pair is created:
F(c(s(X''), s(Y''))) -> F(c(s(s(X'')), Y''))
F(c(s(X''''), s(s(Y'''')))) -> F(c(s(s(X'''')), s(Y'''')))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳FwdInst
...
→DP Problem 3
↳Remaining Obligation(s)
F(c(s(X''''), s(s(Y'''')))) -> F(c(s(s(X'''')), s(Y'''')))
f(c(X, s(Y))) -> f(c(s(X), Y))
g(c(s(X), Y)) -> f(c(X, s(Y)))