R
↳Dependency Pair Analysis
F(x, g(y)) -> F(h(x), i(x, y))
F(x, g(y)) -> I(x, y)
I(x, j(y, z)) -> J(g(y), i(x, z))
I(x, j(y, z)) -> I(x, z)
I(h(x), j(j(y, z), 0)) -> J(i(h(x), j(y, z)), i(x, j(y, z)))
I(h(x), j(j(y, z), 0)) -> I(h(x), j(y, z))
I(h(x), j(j(y, z), 0)) -> I(x, j(y, z))
J(g(x), g(y)) -> J(x, y)
R
↳DPs
→DP Problem 1
↳Polynomial Ordering
→DP Problem 2
↳Polo
→DP Problem 3
↳Remaining
J(g(x), g(y)) -> J(x, y)
f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))
innermost
J(g(x), g(y)) -> J(x, y)
POL(g(x1)) = 1 + x1 POL(J(x1, x2)) = x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 4
↳Dependency Graph
→DP Problem 2
↳Polo
→DP Problem 3
↳Remaining
f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))
innermost
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polynomial Ordering
→DP Problem 3
↳Remaining
I(h(x), j(j(y, z), 0)) -> I(x, j(y, z))
I(h(x), j(j(y, z), 0)) -> I(h(x), j(y, z))
I(x, j(y, z)) -> I(x, z)
f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))
innermost
I(h(x), j(j(y, z), 0)) -> I(x, j(y, z))
POL(I(x1, x2)) = x1 POL(0) = 0 POL(g(x1)) = 0 POL(h(x1)) = 1 + x1 POL(j(x1, x2)) = 0
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 5
↳Polynomial Ordering
→DP Problem 3
↳Remaining
I(h(x), j(j(y, z), 0)) -> I(h(x), j(y, z))
I(x, j(y, z)) -> I(x, z)
f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))
innermost
I(h(x), j(j(y, z), 0)) -> I(h(x), j(y, z))
j(g(x), g(y)) -> g(j(x, y))
POL(I(x1, x2)) = 1 + x1 + x2 POL(0) = 1 POL(g(x1)) = 0 POL(h(x1)) = 0 POL(j(x1, x2)) = x1 + x2
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 5
↳Polo
...
→DP Problem 6
↳Polynomial Ordering
→DP Problem 3
↳Remaining
I(x, j(y, z)) -> I(x, z)
f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))
innermost
I(x, j(y, z)) -> I(x, z)
POL(I(x1, x2)) = x2 POL(j(x1, x2)) = 1 + x2
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 5
↳Polo
...
→DP Problem 7
↳Dependency Graph
→DP Problem 3
↳Remaining
f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))
innermost
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Remaining Obligation(s)
F(x, g(y)) -> F(h(x), i(x, y))
f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))
innermost