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 Rewriting (⇔)
↳27 QDP
↳28 Instantiation (⇔)
↳29 QDP
↳30 NonInfProof (⇔)
↳31 QDP
↳32 DependencyGraphProof (⇔)
↳33 TRUE
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
quot(x, s(y)) → help(x, s(y), 0)
help(x, s(y), c) → if(lt(c, x), x, s(y), c)
if(true, x, s(y), c) → s(help(x, s(y), plus(c, s(y))))
if(false, x, s(y), c) → 0
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
quot(x, s(y)) → help(x, s(y), 0)
help(x, s(y), c) → if(lt(c, x), x, s(y), c)
if(true, x, s(y), c) → s(help(x, s(y), plus(c, s(y))))
if(false, x, s(y), c) → 0
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
plus(x0, 0)
plus(x0, s(x1))
quot(x0, s(x1))
help(x0, s(x1), x2)
if(true, x0, s(x1), x2)
if(false, x0, s(x1), x2)
LT(s(x), s(y)) → LT(x, y)
PLUS(x, s(y)) → PLUS(x, y)
QUOT(x, s(y)) → HELP(x, s(y), 0)
HELP(x, s(y), c) → IF(lt(c, x), x, s(y), c)
HELP(x, s(y), c) → LT(c, x)
IF(true, x, s(y), c) → HELP(x, s(y), plus(c, s(y)))
IF(true, x, s(y), c) → PLUS(c, s(y))
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
quot(x, s(y)) → help(x, s(y), 0)
help(x, s(y), c) → if(lt(c, x), x, s(y), c)
if(true, x, s(y), c) → s(help(x, s(y), plus(c, s(y))))
if(false, x, s(y), c) → 0
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
plus(x0, 0)
plus(x0, s(x1))
quot(x0, s(x1))
help(x0, s(x1), x2)
if(true, x0, s(x1), x2)
if(false, x0, s(x1), x2)
PLUS(x, s(y)) → PLUS(x, y)
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
quot(x, s(y)) → help(x, s(y), 0)
help(x, s(y), c) → if(lt(c, x), x, s(y), c)
if(true, x, s(y), c) → s(help(x, s(y), plus(c, s(y))))
if(false, x, s(y), c) → 0
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
plus(x0, 0)
plus(x0, s(x1))
quot(x0, s(x1))
help(x0, s(x1), x2)
if(true, x0, s(x1), x2)
if(false, x0, s(x1), x2)
PLUS(x, s(y)) → PLUS(x, y)
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
plus(x0, 0)
plus(x0, s(x1))
quot(x0, s(x1))
help(x0, s(x1), x2)
if(true, x0, s(x1), x2)
if(false, x0, s(x1), x2)
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
plus(x0, 0)
plus(x0, s(x1))
quot(x0, s(x1))
help(x0, s(x1), x2)
if(true, x0, s(x1), x2)
if(false, x0, s(x1), x2)
PLUS(x, s(y)) → PLUS(x, y)
From the DPs we obtained the following set of size-change graphs:
LT(s(x), s(y)) → LT(x, y)
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
quot(x, s(y)) → help(x, s(y), 0)
help(x, s(y), c) → if(lt(c, x), x, s(y), c)
if(true, x, s(y), c) → s(help(x, s(y), plus(c, s(y))))
if(false, x, s(y), c) → 0
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
plus(x0, 0)
plus(x0, s(x1))
quot(x0, s(x1))
help(x0, s(x1), x2)
if(true, x0, s(x1), x2)
if(false, x0, s(x1), x2)
LT(s(x), s(y)) → LT(x, y)
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
plus(x0, 0)
plus(x0, s(x1))
quot(x0, s(x1))
help(x0, s(x1), x2)
if(true, x0, s(x1), x2)
if(false, x0, s(x1), x2)
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
plus(x0, 0)
plus(x0, s(x1))
quot(x0, s(x1))
help(x0, s(x1), x2)
if(true, x0, s(x1), x2)
if(false, x0, s(x1), x2)
LT(s(x), s(y)) → LT(x, y)
From the DPs we obtained the following set of size-change graphs:
HELP(x, s(y), c) → IF(lt(c, x), x, s(y), c)
IF(true, x, s(y), c) → HELP(x, s(y), plus(c, s(y)))
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
quot(x, s(y)) → help(x, s(y), 0)
help(x, s(y), c) → if(lt(c, x), x, s(y), c)
if(true, x, s(y), c) → s(help(x, s(y), plus(c, s(y))))
if(false, x, s(y), c) → 0
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
plus(x0, 0)
plus(x0, s(x1))
quot(x0, s(x1))
help(x0, s(x1), x2)
if(true, x0, s(x1), x2)
if(false, x0, s(x1), x2)
HELP(x, s(y), c) → IF(lt(c, x), x, s(y), c)
IF(true, x, s(y), c) → HELP(x, s(y), plus(c, s(y)))
plus(x, s(y)) → s(plus(x, y))
plus(x, 0) → x
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
plus(x0, 0)
plus(x0, s(x1))
quot(x0, s(x1))
help(x0, s(x1), x2)
if(true, x0, s(x1), x2)
if(false, x0, s(x1), x2)
quot(x0, s(x1))
help(x0, s(x1), x2)
if(true, x0, s(x1), x2)
if(false, x0, s(x1), x2)
HELP(x, s(y), c) → IF(lt(c, x), x, s(y), c)
IF(true, x, s(y), c) → HELP(x, s(y), plus(c, s(y)))
plus(x, s(y)) → s(plus(x, y))
plus(x, 0) → x
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
plus(x0, 0)
plus(x0, s(x1))
IF(true, x, s(y), c) → HELP(x, s(y), s(plus(c, y)))
HELP(x, s(y), c) → IF(lt(c, x), x, s(y), c)
IF(true, x, s(y), c) → HELP(x, s(y), s(plus(c, y)))
plus(x, s(y)) → s(plus(x, y))
plus(x, 0) → x
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
plus(x0, 0)
plus(x0, s(x1))
HELP(z0, s(z1), s(y_0)) → IF(lt(s(y_0), z0), z0, s(z1), s(y_0))
IF(true, x, s(y), c) → HELP(x, s(y), s(plus(c, y)))
HELP(z0, s(z1), s(y_0)) → IF(lt(s(y_0), z0), z0, s(z1), s(y_0))
plus(x, s(y)) → s(plus(x, y))
plus(x, 0) → x
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
plus(x0, 0)
plus(x0, s(x1))
(1) (HELP(x3, s(x4), s(plus(x5, x4)))=HELP(x6, s(x7), x8) ⇒ HELP(x6, s(x7), x8)≥IF(lt(x8, x6), x6, s(x7), x8))
(2) (HELP(x3, s(x4), x8)≥IF(lt(x8, x3), x3, s(x4), x8))
(3) (IF(lt(x11, x9), x9, s(x10), x11)=IF(true, x12, s(x13), x14) ⇒ IF(true, x12, s(x13), x14)≥HELP(x12, s(x13), s(plus(x14, x13))))
(4) (lt(x11, x9)=true ⇒ IF(true, x9, s(x10), x11)≥HELP(x9, s(x10), s(plus(x11, x10))))
(5) (true=true ⇒ IF(true, s(x19), s(x10), 0)≥HELP(s(x19), s(x10), s(plus(0, x10))))
(6) (lt(x21, x20)=true∧(∀x22:lt(x21, x20)=true ⇒ IF(true, x20, s(x22), x21)≥HELP(x20, s(x22), s(plus(x21, x22)))) ⇒ IF(true, s(x20), s(x10), s(x21))≥HELP(s(x20), s(x10), s(plus(s(x21), x10))))
(7) (IF(true, s(x19), s(x10), 0)≥HELP(s(x19), s(x10), s(plus(0, x10))))
(8) (IF(true, x20, s(x10), x21)≥HELP(x20, s(x10), s(plus(x21, x10))) ⇒ IF(true, s(x20), s(x10), s(x21))≥HELP(s(x20), s(x10), s(plus(s(x21), x10))))
POL(0) = 0
POL(HELP(x1, x2, x3)) = -1 + x1 + x2 - x3
POL(IF(x1, x2, x3, x4)) = 1 - x1 + x2 - x4
POL(c) = -1
POL(false) = 1
POL(lt(x1, x2)) = 1
POL(plus(x1, x2)) = x1 + x2
POL(s(x1)) = 1 + x1
POL(true) = 1
The following pairs are in Pbound:
IF(true, x, s(y), c) → HELP(x, s(y), s(plus(c, y)))
The following rules are usable:
IF(true, x, s(y), c) → HELP(x, s(y), s(plus(c, y)))
true → lt(0, s(y))
lt(x, y) → lt(s(x), s(y))
x → plus(x, 0)
false → lt(x, 0)
s(plus(x, y)) → plus(x, s(y))
HELP(x, s(y), c) → IF(lt(c, x), x, s(y), c)
plus(x, s(y)) → s(plus(x, y))
plus(x, 0) → x
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
plus(x0, 0)
plus(x0, s(x1))