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
↳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(s(X'''')), s(Y''''))) -> F(c(s(s(s(X''''))), Y''''))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳Inst
...
→DP Problem 3
↳Instantiation Transformation
F(c(s(s(X'''')), s(Y''''))) -> F(c(s(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(s(X'''')), s(Y''''))) -> F(c(s(s(s(X''''))), Y''''))
F(c(s(s(s(X''''''))), s(Y''''''))) -> F(c(s(s(s(s(X'''''')))), Y''''''))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳Inst
...
→DP Problem 4
↳Instantiation Transformation
F(c(s(s(s(X''''''))), s(Y''''''))) -> F(c(s(s(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(s(s(X''''''))), s(Y''''''))) -> F(c(s(s(s(s(X'''''')))), Y''''''))
F(c(s(s(s(s(X'''''''')))), s(Y''''''''))) -> F(c(s(s(s(s(s(X''''''''))))), Y''''''''))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳Inst
...
→DP Problem 5
↳Instantiation Transformation
F(c(s(s(s(s(X'''''''')))), s(Y''''''''))) -> F(c(s(s(s(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(s(s(s(X'''''''')))), s(Y''''''''))) -> F(c(s(s(s(s(s(X''''''''))))), Y''''''''))
F(c(s(s(s(s(s(X''''''''''))))), s(Y''''''''''))) -> F(c(s(s(s(s(s(s(X'''''''''')))))), Y''''''''''))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳Inst
...
→DP Problem 6
↳Remaining Obligation(s)
F(c(s(s(s(s(s(X''''''''''))))), s(Y''''''''''))) -> F(c(s(s(s(s(s(s(X'''''''''')))))), Y''''''''''))
f(c(X, s(Y))) -> f(c(s(X), Y))
g(c(s(X), Y)) -> f(c(X, s(Y)))