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