R
↳Dependency Pair Analysis
F(x, c(x), c(y)) -> F(y, y, f(y, x, y))
F(x, c(x), c(y)) -> F(y, x, y)
F(s(x), y, z) -> F(x, s(c(y)), c(z))
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳Remaining
F(s(x), y, z) -> F(x, s(c(y)), c(z))
f(x, c(x), c(y)) -> f(y, y, f(y, x, y))
f(s(x), y, z) -> f(x, s(c(y)), c(z))
f(c(x), x, y) -> c(y)
g(x, y) -> x
g(x, y) -> y
F(s(x), y, z) -> F(x, s(c(y)), c(z))
F > c
F > s
F(x1, x2, x3) -> F(x1, x2, x3)
s(x1) -> s(x1)
c(x1) -> c(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳Dependency Graph
→DP Problem 2
↳Remaining
f(x, c(x), c(y)) -> f(y, y, f(y, x, y))
f(s(x), y, z) -> f(x, s(c(y)), c(z))
f(c(x), x, y) -> c(y)
g(x, y) -> x
g(x, y) -> y
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Remaining Obligation(s)
F(x, c(x), c(y)) -> F(y, x, y)
F(x, c(x), c(y)) -> F(y, y, f(y, x, y))
f(x, c(x), c(y)) -> f(y, y, f(y, x, y))
f(s(x), y, z) -> f(x, s(c(y)), c(z))
f(c(x), x, y) -> c(y)
g(x, y) -> x
g(x, y) -> y