R
↳Dependency Pair Analysis
F(s(x), s(y)) -> F(x, y)
G(0, x) -> G(f(x, x), x)
G(0, x) -> F(x, x)
R
↳DPs
→DP Problem 1
↳Polynomial Ordering
→DP Problem 2
↳FwdInst
F(s(x), s(y)) -> F(x, y)
f(x, 0) -> s(0)
f(s(x), s(y)) -> s(f(x, y))
g(0, x) -> g(f(x, x), x)
F(s(x), s(y)) -> F(x, y)
f(x, 0) -> s(0)
f(s(x), s(y)) -> s(f(x, y))
g(0, x) -> g(f(x, x), x)
POL(0) = 0 POL(g(x1, x2)) = 0 POL(s(x1)) = 1 + x1 POL(f(x1, x2)) = 1 + x1 POL(F(x1, x2)) = x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 3
↳Dependency Graph
→DP Problem 2
↳FwdInst
f(x, 0) -> s(0)
f(s(x), s(y)) -> s(f(x, y))
g(0, x) -> g(f(x, x), x)
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Forward Instantiation Transformation
G(0, x) -> G(f(x, x), x)
f(x, 0) -> s(0)
f(s(x), s(y)) -> s(f(x, y))
g(0, x) -> g(f(x, x), x)
no new Dependency Pairs are created.
G(0, x) -> G(f(x, x), x)