YES
0 QTRS
↳1 DependencyPairsProof (⇔, 0 ms)
↳2 QDP
↳3 DependencyGraphProof (⇔, 0 ms)
↳4 AND
↳5 QDP
↳6 UsableRulesProof (⇔, 0 ms)
↳7 QDP
↳8 QDPSizeChangeProof (⇔, 0 ms)
↳9 YES
↳10 QDP
↳11 UsableRulesProof (⇔, 0 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
↳15 QDP
↳16 QDPOrderProof (⇔, 0 ms)
↳17 QDP
↳18 QDPOrderProof (⇔, 0 ms)
↳19 QDP
↳20 TransformationProof (⇔, 0 ms)
↳21 QDP
↳22 DependencyGraphProof (⇔, 0 ms)
↳23 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.
DIV(div(x, y), z) → DIV(x, times(y, z))
trivial
dummyConstant=1
div_1=1
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))
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)
trivial
s_1=1
dummyConstant=1
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)) → 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))