R
↳Dependency Pair Analysis
DIV(x, y) -> QUOT(x, y, y)
QUOT(s(x), s(y), z) -> QUOT(x, y, z)
QUOT(x, 0, s(z)) -> DIV(x, s(z))
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
QUOT(x, 0, s(z)) -> DIV(x, s(z))
QUOT(s(x), s(y), z) -> QUOT(x, y, z)
DIV(x, y) -> QUOT(x, y, y)
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
QUOT(s(x), s(y), z) -> QUOT(x, y, z)
POL(s(x1)) = 1 + x1
QUOT(x1, x2, x3) -> x1
s(x1) -> s(x1)
DIV(x1, x2) -> x1
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
QUOT(x, 0, s(z)) -> DIV(x, s(z))
DIV(x, y) -> QUOT(x, y, y)
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
DIV(x, y) -> QUOT(x, y, y)
POL(QUOT(x1, x2)) = x1 + x2 POL(0) = 1 POL(DIV(x1, x2)) = 1 + x1 + x2 POL(s) = 0
DIV(x1, x2) -> DIV(x1, x2)
QUOT(x1, x2, x3) -> QUOT(x1, x2)
s(x1) -> s
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
...
→DP Problem 3
↳Dependency Graph
QUOT(x, 0, s(z)) -> DIV(x, s(z))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))