R
↳Dependency Pair Analysis
PLUS(s(x), y) -> PLUS(x, y)
TIMES(s(x), y) -> PLUS(y, times(x, y))
TIMES(s(x), y) -> TIMES(x, y)
DIV(x, y) -> QUOT(x, y, y)
DIV(div(x, y), z) -> DIV(x, times(y, z))
DIV(div(x, y), z) -> TIMES(y, z)
QUOT(s(x), s(y), z) -> QUOT(x, y, z)
QUOT(x, 0, s(z)) -> DIV(x, s(z))
R
↳DPs
→DP Problem 1
↳Polynomial Ordering
→DP Problem 2
↳Polo
→DP Problem 3
↳Remaining
PLUS(s(x), y) -> PLUS(x, y)
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
div(div(x, y), z) -> div(x, times(y, z))
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)))
PLUS(s(x), y) -> PLUS(x, y)
POL(PLUS(x1, x2)) = x1 POL(s(x1)) = 1 + x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 4
↳Dependency Graph
→DP Problem 2
↳Polo
→DP Problem 3
↳Remaining
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
div(div(x, y), z) -> div(x, times(y, z))
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)))
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polynomial Ordering
→DP Problem 3
↳Remaining
TIMES(s(x), y) -> TIMES(x, y)
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
div(div(x, y), z) -> div(x, times(y, z))
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)))
TIMES(s(x), y) -> TIMES(x, y)
POL(TIMES(x1, x2)) = x1 POL(s(x1)) = 1 + x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 5
↳Dependency Graph
→DP Problem 3
↳Remaining
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
div(div(x, y), z) -> div(x, times(y, z))
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)))
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Remaining Obligation(s)
DIV(div(x, y), z) -> DIV(x, times(y, z))
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)
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
div(div(x, y), z) -> div(x, times(y, z))
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)))