R
↳Dependency Pair Analysis
H(X, Z) -> F(X, s(X), Z)
F(X, Y, g(X, Y)) -> H(0, g(X, Y))
G(X, s(Y)) -> G(X, Y)
R
↳DPs
→DP Problem 1
↳Polynomial Ordering
→DP Problem 2
↳Inst
G(X, s(Y)) -> G(X, Y)
h(X, Z) -> f(X, s(X), Z)
f(X, Y, g(X, Y)) -> h(0, g(X, Y))
g(0, Y) -> 0
g(X, s(Y)) -> g(X, Y)
G(X, s(Y)) -> G(X, Y)
POL(G(x1, x2)) = x2 POL(s(x1)) = 1 + x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 3
↳Dependency Graph
→DP Problem 2
↳Inst
h(X, Z) -> f(X, s(X), Z)
f(X, Y, g(X, Y)) -> h(0, g(X, Y))
g(0, Y) -> 0
g(X, s(Y)) -> g(X, Y)
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Instantiation Transformation
F(X, Y, g(X, Y)) -> H(0, g(X, Y))
H(X, Z) -> F(X, s(X), Z)
h(X, Z) -> f(X, s(X), Z)
f(X, Y, g(X, Y)) -> h(0, g(X, Y))
g(0, Y) -> 0
g(X, s(Y)) -> g(X, Y)
one new Dependency Pair is created:
H(X, Z) -> F(X, s(X), Z)
H(0, Z') -> F(0, s(0), Z')
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Inst
→DP Problem 4
↳Instantiation Transformation
H(0, Z') -> F(0, s(0), Z')
F(X, Y, g(X, Y)) -> H(0, g(X, Y))
h(X, Z) -> f(X, s(X), Z)
f(X, Y, g(X, Y)) -> h(0, g(X, Y))
g(0, Y) -> 0
g(X, s(Y)) -> g(X, Y)
one new Dependency Pair is created:
F(X, Y, g(X, Y)) -> H(0, g(X, Y))
F(0, s(0), g(0, s(0))) -> H(0, g(0, s(0)))
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Inst
→DP Problem 4
↳Inst
...
→DP Problem 5
↳Remaining Obligation(s)
F(0, s(0), g(0, s(0))) -> H(0, g(0, s(0)))
H(0, Z') -> F(0, s(0), Z')
h(X, Z) -> f(X, s(X), Z)
f(X, Y, g(X, Y)) -> h(0, g(X, Y))
g(0, Y) -> 0
g(X, s(Y)) -> g(X, Y)