YES
0 QTRS
↳1 Overlay + Local Confluence (⇔, 7 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 QDP
↳10 QReductionProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 QDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 QDP
↳17 QReductionProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y
minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y
minus(0, x0)
minus(s(x0), s(x1))
geq(x0, 0)
geq(0, s(x0))
geq(s(x0), s(x1))
div(0, s(x0))
div(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
MINUS(s(X), s(Y)) → MINUS(X, Y)
GEQ(s(X), s(Y)) → GEQ(X, Y)
DIV(s(X), s(Y)) → IF(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
DIV(s(X), s(Y)) → GEQ(X, Y)
DIV(s(X), s(Y)) → DIV(minus(X, Y), s(Y))
DIV(s(X), s(Y)) → MINUS(X, Y)
minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y
minus(0, x0)
minus(s(x0), s(x1))
geq(x0, 0)
geq(0, s(x0))
geq(s(x0), s(x1))
div(0, s(x0))
div(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
GEQ(s(X), s(Y)) → GEQ(X, Y)
minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y
minus(0, x0)
minus(s(x0), s(x1))
geq(x0, 0)
geq(0, s(x0))
geq(s(x0), s(x1))
div(0, s(x0))
div(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
GEQ(s(X), s(Y)) → GEQ(X, Y)
minus(0, x0)
minus(s(x0), s(x1))
geq(x0, 0)
geq(0, s(x0))
geq(s(x0), s(x1))
div(0, s(x0))
div(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
minus(0, x0)
minus(s(x0), s(x1))
geq(x0, 0)
geq(0, s(x0))
geq(s(x0), s(x1))
div(0, s(x0))
div(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
GEQ(s(X), s(Y)) → GEQ(X, Y)
From the DPs we obtained the following set of size-change graphs:
MINUS(s(X), s(Y)) → MINUS(X, Y)
minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y
minus(0, x0)
minus(s(x0), s(x1))
geq(x0, 0)
geq(0, s(x0))
geq(s(x0), s(x1))
div(0, s(x0))
div(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
MINUS(s(X), s(Y)) → MINUS(X, Y)
minus(0, x0)
minus(s(x0), s(x1))
geq(x0, 0)
geq(0, s(x0))
geq(s(x0), s(x1))
div(0, s(x0))
div(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
minus(0, x0)
minus(s(x0), s(x1))
geq(x0, 0)
geq(0, s(x0))
geq(s(x0), s(x1))
div(0, s(x0))
div(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
MINUS(s(X), s(Y)) → MINUS(X, Y)
From the DPs we obtained the following set of size-change graphs: