0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
↳5 QDP
↳6 UsableRulesProof (⇔)
↳7 QDP
↳8 QDPSizeChangeProof (⇔)
↳9 TRUE
↳10 QDP
↳11 UsableRulesProof (⇔)
↳12 QDP
↳13 QDPSizeChangeProof (⇔)
↳14 TRUE
↳15 QDP
↳16 QDPOrderProof (⇔)
↳17 QDP
↳18 Instantiation (⇔)
↳19 QDP
↳20 DependencyGraphProof (⇔)
↳21 TRUE
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)
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(div(x, y), z) → div(x, times(y, z))
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)
QUOT(s(x), s(y), z) → QUOT(x, y, z)
QUOT(x, 0, s(z)) → DIV(x, s(z))
DIV(div(x, y), z) → DIV(x, times(y, z))
DIV(div(x, y), z) → TIMES(y, z)
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)
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(div(x, y), z) → div(x, times(y, z))
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)
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(div(x, y), z) → div(x, times(y, z))
PLUS(s(x), y) → PLUS(x, y)
From the DPs we obtained the following set of size-change graphs:
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)
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(div(x, y), z) → div(x, times(y, z))
TIMES(s(x), y) → TIMES(x, y)
From the DPs we obtained the following set of size-change graphs:
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))
DIV(div(x, y), z) → DIV(x, times(y, z))
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)
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(div(x, y), z) → div(x, times(y, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
QUOT(s(x), s(y), z) → QUOT(x, y, z)
DIV(div(x, y), z) → DIV(x, times(y, z))
POL(0) = 0
POL(DIV(x1, x2)) = x1
POL(QUOT(x1, x2, x3)) = x1
POL(div(x1, x2)) = 1 + x1
POL(plus(x1, x2)) = 0
POL(s(x1)) = 1 + x1
POL(times(x1, x2)) = 0
DIV(x, y) → QUOT(x, y, y)
QUOT(x, 0, s(z)) → DIV(x, s(z))
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)
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(div(x, y), z) → div(x, times(y, z))
DIV(y_0, s(y_1)) → QUOT(y_0, s(y_1), s(y_1))
QUOT(x, 0, s(z)) → DIV(x, s(z))
DIV(y_0, s(y_1)) → QUOT(y_0, s(y_1), s(y_1))
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)
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(div(x, y), z) → div(x, times(y, z))