YES
0 QTRS
↳1 Overlay + Local Confluence (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 1 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
↳21 QDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 QDP
↳24 QReductionProof (⇔, 0 ms)
↳25 QDP
↳26 TransformationProof (⇔, 0 ms)
↳27 QDP
↳28 DependencyGraphProof (⇔, 0 ms)
↳29 QDP
↳30 UsableRulesProof (⇔, 0 ms)
↳31 QDP
↳32 QReductionProof (⇔, 0 ms)
↳33 QDP
↳34 QDPQMonotonicMRRProof (⇔, 15 ms)
↳35 QDP
↳36 DependencyGraphProof (⇔, 0 ms)
↳37 TRUE
minus(0, y) → 0
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
zero(s(x)) → false
zero(0) → true
p(s(x)) → x
div(x, y) → quot(x, y, 0)
quot(x, y, z) → if(zero(x), x, y, plus(z, s(0)))
if(true, x, y, z) → p(z)
if(false, x, s(y), z) → quot(minus(x, s(y)), s(y), z)
minus(0, y) → 0
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
zero(s(x)) → false
zero(0) → true
p(s(x)) → x
div(x, y) → quot(x, y, 0)
quot(x, y, z) → if(zero(x), x, y, plus(z, s(0)))
if(true, x, y, z) → p(z)
if(false, x, s(y), z) → quot(minus(x, s(y)), s(y), z)
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
zero(s(x0))
zero(0)
p(s(x0))
div(x0, x1)
quot(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, s(x1), x2)
MINUS(s(x), s(y)) → MINUS(x, y)
PLUS(s(x), y) → PLUS(x, s(y))
DIV(x, y) → QUOT(x, y, 0)
QUOT(x, y, z) → IF(zero(x), x, y, plus(z, s(0)))
QUOT(x, y, z) → ZERO(x)
QUOT(x, y, z) → PLUS(z, s(0))
IF(true, x, y, z) → P(z)
IF(false, x, s(y), z) → QUOT(minus(x, s(y)), s(y), z)
IF(false, x, s(y), z) → MINUS(x, s(y))
minus(0, y) → 0
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
zero(s(x)) → false
zero(0) → true
p(s(x)) → x
div(x, y) → quot(x, y, 0)
quot(x, y, z) → if(zero(x), x, y, plus(z, s(0)))
if(true, x, y, z) → p(z)
if(false, x, s(y), z) → quot(minus(x, s(y)), s(y), z)
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
zero(s(x0))
zero(0)
p(s(x0))
div(x0, x1)
quot(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, s(x1), x2)
PLUS(s(x), y) → PLUS(x, s(y))
minus(0, y) → 0
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
zero(s(x)) → false
zero(0) → true
p(s(x)) → x
div(x, y) → quot(x, y, 0)
quot(x, y, z) → if(zero(x), x, y, plus(z, s(0)))
if(true, x, y, z) → p(z)
if(false, x, s(y), z) → quot(minus(x, s(y)), s(y), z)
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
zero(s(x0))
zero(0)
p(s(x0))
div(x0, x1)
quot(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, s(x1), x2)
PLUS(s(x), y) → PLUS(x, s(y))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
zero(s(x0))
zero(0)
p(s(x0))
div(x0, x1)
quot(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, s(x1), x2)
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
zero(s(x0))
zero(0)
p(s(x0))
div(x0, x1)
quot(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, s(x1), x2)
PLUS(s(x), y) → PLUS(x, s(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(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
zero(s(x)) → false
zero(0) → true
p(s(x)) → x
div(x, y) → quot(x, y, 0)
quot(x, y, z) → if(zero(x), x, y, plus(z, s(0)))
if(true, x, y, z) → p(z)
if(false, x, s(y), z) → quot(minus(x, s(y)), s(y), z)
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
zero(s(x0))
zero(0)
p(s(x0))
div(x0, x1)
quot(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, s(x1), x2)
MINUS(s(x), s(y)) → MINUS(x, y)
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
zero(s(x0))
zero(0)
p(s(x0))
div(x0, x1)
quot(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, s(x1), x2)
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
zero(s(x0))
zero(0)
p(s(x0))
div(x0, x1)
quot(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, s(x1), x2)
MINUS(s(x), s(y)) → MINUS(x, y)
From the DPs we obtained the following set of size-change graphs:
IF(false, x, s(y), z) → QUOT(minus(x, s(y)), s(y), z)
QUOT(x, y, z) → IF(zero(x), x, y, plus(z, s(0)))
minus(0, y) → 0
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
zero(s(x)) → false
zero(0) → true
p(s(x)) → x
div(x, y) → quot(x, y, 0)
quot(x, y, z) → if(zero(x), x, y, plus(z, s(0)))
if(true, x, y, z) → p(z)
if(false, x, s(y), z) → quot(minus(x, s(y)), s(y), z)
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
zero(s(x0))
zero(0)
p(s(x0))
div(x0, x1)
quot(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, s(x1), x2)
IF(false, x, s(y), z) → QUOT(minus(x, s(y)), s(y), z)
QUOT(x, y, z) → IF(zero(x), x, y, plus(z, s(0)))
zero(s(x)) → false
zero(0) → true
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
zero(s(x0))
zero(0)
p(s(x0))
div(x0, x1)
quot(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, s(x1), x2)
p(s(x0))
div(x0, x1)
quot(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, s(x1), x2)
IF(false, x, s(y), z) → QUOT(minus(x, s(y)), s(y), z)
QUOT(x, y, z) → IF(zero(x), x, y, plus(z, s(0)))
zero(s(x)) → false
zero(0) → true
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
zero(s(x0))
zero(0)
QUOT(s(x0), y1, y2) → IF(false, s(x0), y1, plus(y2, s(0))) → QUOT(s(x0), y1, y2) → IF(false, s(x0), y1, plus(y2, s(0)))
QUOT(0, y1, y2) → IF(true, 0, y1, plus(y2, s(0))) → QUOT(0, y1, y2) → IF(true, 0, y1, plus(y2, s(0)))
IF(false, x, s(y), z) → QUOT(minus(x, s(y)), s(y), z)
QUOT(s(x0), y1, y2) → IF(false, s(x0), y1, plus(y2, s(0)))
QUOT(0, y1, y2) → IF(true, 0, y1, plus(y2, s(0)))
zero(s(x)) → false
zero(0) → true
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
zero(s(x0))
zero(0)
QUOT(s(x0), y1, y2) → IF(false, s(x0), y1, plus(y2, s(0)))
IF(false, x, s(y), z) → QUOT(minus(x, s(y)), s(y), z)
zero(s(x)) → false
zero(0) → true
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
zero(s(x0))
zero(0)
QUOT(s(x0), y1, y2) → IF(false, s(x0), y1, plus(y2, s(0)))
IF(false, x, s(y), z) → QUOT(minus(x, s(y)), s(y), z)
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
zero(s(x0))
zero(0)
zero(s(x0))
zero(0)
QUOT(s(x0), y1, y2) → IF(false, s(x0), y1, plus(y2, s(0)))
IF(false, x, s(y), z) → QUOT(minus(x, s(y)), s(y), z)
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
minus(s(x), s(y)) → minus(x, y)
POL(0) = 0
POL(IF(x1, x2, x3, x4)) = 2·x2 + x3
POL(QUOT(x1, x2, x3)) = 2·x1 + x2
POL(false) = 0
POL(minus(x1, x2)) = x1
POL(plus(x1, x2)) = 1 + x1 + x2
POL(s(x1)) = 1 + x1
QUOT(s(x0), y1, y2) → IF(false, s(x0), y1, plus(y2, s(0)))
IF(false, x, s(y), z) → QUOT(minus(x, s(y)), s(y), z)
minus(0, y) → 0
minus(x, 0) → x
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)