0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 TRUE
↳14 QDP
↳15 UsableRulesProof (⇔)
↳16 QDP
↳17 QReductionProof (⇔)
↳18 QDP
↳19 QDPSizeChangeProof (⇔)
↳20 TRUE
↳21 QDP
↳22 UsableRulesProof (⇔)
↳23 QDP
↳24 QReductionProof (⇔)
↳25 QDP
↳26 Narrowing (⇔)
↳27 QDP
↳28 DependencyGraphProof (⇔)
↳29 QDP
↳30 Rewriting (⇔)
↳31 QDP
↳32 Narrowing (⇔)
↳33 QDP
↳34 DependencyGraphProof (⇔)
↳35 QDP
↳36 Instantiation (⇔)
↳37 QDP
↳38 Rewriting (⇔)
↳39 QDP
↳40 ForwardInstantiation (⇔)
↳41 QDP
↳42 Narrowing (⇔)
↳43 QDP
↳44 Instantiation (⇔)
↳45 QDP
↳46 Instantiation (⇔)
↳47 QDP
↳48 DependencyGraphProof (⇔)
↳49 AND
↳50 QDP
↳51 ForwardInstantiation (⇔)
↳52 QDP
↳53 Rewriting (⇔)
↳54 QDP
↳55 QDPOrderProof (⇔)
↳56 QDP
↳57 DependencyGraphProof (⇔)
↳58 TRUE
↳59 QDP
↳60 UsableRulesProof (⇔)
↳61 QDP
↳62 QReductionProof (⇔)
↳63 QDP
↳64 Rewriting (⇔)
↳65 QDP
↳66 UsableRulesProof (⇔)
↳67 QDP
↳68 QReductionProof (⇔)
↳69 QDP
↳70 ForwardInstantiation (⇔)
↳71 QDP
↳72 ForwardInstantiation (⇔)
↳73 QDP
↳74 QDPSizeChangeProof (⇔)
↳75 TRUE
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
div(x, y) → ify(ge(y, s(0)), x, y)
ify(false, x, y) → divByZeroError
ify(true, x, y) → if(ge(x, y), x, y)
if(false, x, y) → 0
if(true, x, y) → s(div(minus(x, y), y))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
div(x, y) → ify(ge(y, s(0)), x, y)
ify(false, x, y) → divByZeroError
ify(true, x, y) → if(ge(x, y), x, y)
if(false, x, y) → 0
if(true, x, y) → s(div(minus(x, y), y))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
GE(s(x), s(y)) → GE(x, y)
MINUS(s(x), s(y)) → MINUS(x, y)
DIV(x, y) → IFY(ge(y, s(0)), x, y)
DIV(x, y) → GE(y, s(0))
IFY(true, x, y) → IF(ge(x, y), x, y)
IFY(true, x, y) → GE(x, y)
IF(true, x, y) → DIV(minus(x, y), y)
IF(true, x, y) → MINUS(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
div(x, y) → ify(ge(y, s(0)), x, y)
ify(false, x, y) → divByZeroError
ify(true, x, y) → if(ge(x, y), x, y)
if(false, x, y) → 0
if(true, x, y) → s(div(minus(x, y), y))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
MINUS(s(x), s(y)) → MINUS(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
div(x, y) → ify(ge(y, s(0)), x, y)
ify(false, x, y) → divByZeroError
ify(true, x, y) → if(ge(x, y), x, y)
if(false, x, y) → 0
if(true, x, y) → s(div(minus(x, y), y))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
MINUS(s(x), s(y)) → MINUS(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
MINUS(s(x), s(y)) → MINUS(x, y)
From the DPs we obtained the following set of size-change graphs:
GE(s(x), s(y)) → GE(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
div(x, y) → ify(ge(y, s(0)), x, y)
ify(false, x, y) → divByZeroError
ify(true, x, y) → if(ge(x, y), x, y)
if(false, x, y) → 0
if(true, x, y) → s(div(minus(x, y), y))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
GE(s(x), s(y)) → GE(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
GE(s(x), s(y)) → GE(x, y)
From the DPs we obtained the following set of size-change graphs:
DIV(x, y) → IFY(ge(y, s(0)), x, y)
IFY(true, x, y) → IF(ge(x, y), x, y)
IF(true, x, y) → DIV(minus(x, y), y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
div(x, y) → ify(ge(y, s(0)), x, y)
ify(false, x, y) → divByZeroError
ify(true, x, y) → if(ge(x, y), x, y)
if(false, x, y) → 0
if(true, x, y) → s(div(minus(x, y), y))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
DIV(x, y) → IFY(ge(y, s(0)), x, y)
IFY(true, x, y) → IF(ge(x, y), x, y)
IF(true, x, y) → DIV(minus(x, y), y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
DIV(x, y) → IFY(ge(y, s(0)), x, y)
IFY(true, x, y) → IF(ge(x, y), x, y)
IF(true, x, y) → DIV(minus(x, y), y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
DIV(y0, 0) → IFY(false, y0, 0)
DIV(y0, s(x0)) → IFY(ge(x0, 0), y0, s(x0))
IFY(true, x, y) → IF(ge(x, y), x, y)
IF(true, x, y) → DIV(minus(x, y), y)
DIV(y0, 0) → IFY(false, y0, 0)
DIV(y0, s(x0)) → IFY(ge(x0, 0), y0, s(x0))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
IF(true, x, y) → DIV(minus(x, y), y)
DIV(y0, s(x0)) → IFY(ge(x0, 0), y0, s(x0))
IFY(true, x, y) → IF(ge(x, y), x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
DIV(y0, s(x0)) → IFY(true, y0, s(x0))
IF(true, x, y) → DIV(minus(x, y), y)
IFY(true, x, y) → IF(ge(x, y), x, y)
DIV(y0, s(x0)) → IFY(true, y0, s(x0))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
IFY(true, x0, 0) → IF(true, x0, 0)
IFY(true, 0, s(x0)) → IF(false, 0, s(x0))
IFY(true, s(x0), s(x1)) → IF(ge(x0, x1), s(x0), s(x1))
IF(true, x, y) → DIV(minus(x, y), y)
DIV(y0, s(x0)) → IFY(true, y0, s(x0))
IFY(true, x0, 0) → IF(true, x0, 0)
IFY(true, 0, s(x0)) → IF(false, 0, s(x0))
IFY(true, s(x0), s(x1)) → IF(ge(x0, x1), s(x0), s(x1))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
DIV(y0, s(x0)) → IFY(true, y0, s(x0))
IFY(true, s(x0), s(x1)) → IF(ge(x0, x1), s(x0), s(x1))
IF(true, x, y) → DIV(minus(x, y), y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
IF(true, s(z0), s(z1)) → DIV(minus(s(z0), s(z1)), s(z1))
DIV(y0, s(x0)) → IFY(true, y0, s(x0))
IFY(true, s(x0), s(x1)) → IF(ge(x0, x1), s(x0), s(x1))
IF(true, s(z0), s(z1)) → DIV(minus(s(z0), s(z1)), s(z1))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
IF(true, s(z0), s(z1)) → DIV(minus(z0, z1), s(z1))
DIV(y0, s(x0)) → IFY(true, y0, s(x0))
IFY(true, s(x0), s(x1)) → IF(ge(x0, x1), s(x0), s(x1))
IF(true, s(z0), s(z1)) → DIV(minus(z0, z1), s(z1))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
DIV(s(y_0), s(x1)) → IFY(true, s(y_0), s(x1))
IFY(true, s(x0), s(x1)) → IF(ge(x0, x1), s(x0), s(x1))
IF(true, s(z0), s(z1)) → DIV(minus(z0, z1), s(z1))
DIV(s(y_0), s(x1)) → IFY(true, s(y_0), s(x1))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
IF(true, s(x0), s(0)) → DIV(x0, s(0))
IF(true, s(s(x0)), s(s(x1))) → DIV(minus(x0, x1), s(s(x1)))
IFY(true, s(x0), s(x1)) → IF(ge(x0, x1), s(x0), s(x1))
DIV(s(y_0), s(x1)) → IFY(true, s(y_0), s(x1))
IF(true, s(x0), s(0)) → DIV(x0, s(0))
IF(true, s(s(x0)), s(s(x1))) → DIV(minus(x0, x1), s(s(x1)))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
DIV(s(x0), s(0)) → IFY(true, s(x0), s(0))
DIV(s(x0), s(s(z1))) → IFY(true, s(x0), s(s(z1)))
IFY(true, s(x0), s(x1)) → IF(ge(x0, x1), s(x0), s(x1))
IF(true, s(x0), s(0)) → DIV(x0, s(0))
IF(true, s(s(x0)), s(s(x1))) → DIV(minus(x0, x1), s(s(x1)))
DIV(s(x0), s(0)) → IFY(true, s(x0), s(0))
DIV(s(x0), s(s(z1))) → IFY(true, s(x0), s(s(z1)))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
IFY(true, s(z0), s(0)) → IF(ge(z0, 0), s(z0), s(0))
IFY(true, s(z0), s(s(z1))) → IF(ge(z0, s(z1)), s(z0), s(s(z1)))
IF(true, s(x0), s(0)) → DIV(x0, s(0))
IF(true, s(s(x0)), s(s(x1))) → DIV(minus(x0, x1), s(s(x1)))
DIV(s(x0), s(0)) → IFY(true, s(x0), s(0))
DIV(s(x0), s(s(z1))) → IFY(true, s(x0), s(s(z1)))
IFY(true, s(z0), s(0)) → IF(ge(z0, 0), s(z0), s(0))
IFY(true, s(z0), s(s(z1))) → IF(ge(z0, s(z1)), s(z0), s(s(z1)))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
DIV(s(x0), s(s(z1))) → IFY(true, s(x0), s(s(z1)))
IFY(true, s(z0), s(s(z1))) → IF(ge(z0, s(z1)), s(z0), s(s(z1)))
IF(true, s(s(x0)), s(s(x1))) → DIV(minus(x0, x1), s(s(x1)))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
IFY(true, s(s(y_1)), s(s(x1))) → IF(ge(s(y_1), s(x1)), s(s(y_1)), s(s(x1)))
DIV(s(x0), s(s(z1))) → IFY(true, s(x0), s(s(z1)))
IF(true, s(s(x0)), s(s(x1))) → DIV(minus(x0, x1), s(s(x1)))
IFY(true, s(s(y_1)), s(s(x1))) → IF(ge(s(y_1), s(x1)), s(s(y_1)), s(s(x1)))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
IFY(true, s(s(y_1)), s(s(x1))) → IF(ge(y_1, x1), s(s(y_1)), s(s(x1)))
DIV(s(x0), s(s(z1))) → IFY(true, s(x0), s(s(z1)))
IF(true, s(s(x0)), s(s(x1))) → DIV(minus(x0, x1), s(s(x1)))
IFY(true, s(s(y_1)), s(s(x1))) → IF(ge(y_1, x1), s(s(y_1)), s(s(x1)))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF(true, s(s(x0)), s(s(x1))) → DIV(minus(x0, x1), s(s(x1)))
POL(0) = 0
POL(DIV(x1, x2)) = x1
POL(IF(x1, x2, x3)) = x2
POL(IFY(x1, x2, x3)) = x2
POL(false) = 0
POL(ge(x1, x2)) = 0
POL(minus(x1, x2)) = x1
POL(s(x1)) = 1 + x1
POL(true) = 0
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
DIV(s(x0), s(s(z1))) → IFY(true, s(x0), s(s(z1)))
IFY(true, s(s(y_1)), s(s(x1))) → IF(ge(y_1, x1), s(s(y_1)), s(s(x1)))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
DIV(s(x0), s(0)) → IFY(true, s(x0), s(0))
IFY(true, s(z0), s(0)) → IF(ge(z0, 0), s(z0), s(0))
IF(true, s(x0), s(0)) → DIV(x0, s(0))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
DIV(s(x0), s(0)) → IFY(true, s(x0), s(0))
IFY(true, s(z0), s(0)) → IF(ge(z0, 0), s(z0), s(0))
IF(true, s(x0), s(0)) → DIV(x0, s(0))
ge(x, 0) → true
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
DIV(s(x0), s(0)) → IFY(true, s(x0), s(0))
IFY(true, s(z0), s(0)) → IF(ge(z0, 0), s(z0), s(0))
IF(true, s(x0), s(0)) → DIV(x0, s(0))
ge(x, 0) → true
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
IFY(true, s(z0), s(0)) → IF(true, s(z0), s(0))
DIV(s(x0), s(0)) → IFY(true, s(x0), s(0))
IF(true, s(x0), s(0)) → DIV(x0, s(0))
IFY(true, s(z0), s(0)) → IF(true, s(z0), s(0))
ge(x, 0) → true
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
DIV(s(x0), s(0)) → IFY(true, s(x0), s(0))
IF(true, s(x0), s(0)) → DIV(x0, s(0))
IFY(true, s(z0), s(0)) → IF(true, s(z0), s(0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
DIV(s(x0), s(0)) → IFY(true, s(x0), s(0))
IF(true, s(x0), s(0)) → DIV(x0, s(0))
IFY(true, s(z0), s(0)) → IF(true, s(z0), s(0))
IF(true, s(s(y_0)), s(0)) → DIV(s(y_0), s(0))
DIV(s(x0), s(0)) → IFY(true, s(x0), s(0))
IFY(true, s(z0), s(0)) → IF(true, s(z0), s(0))
IF(true, s(s(y_0)), s(0)) → DIV(s(y_0), s(0))
IFY(true, s(s(y_0)), s(0)) → IF(true, s(s(y_0)), s(0))
DIV(s(x0), s(0)) → IFY(true, s(x0), s(0))
IF(true, s(s(y_0)), s(0)) → DIV(s(y_0), s(0))
IFY(true, s(s(y_0)), s(0)) → IF(true, s(s(y_0)), s(0))
From the DPs we obtained the following set of size-change graphs: