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 Rewriting (⇔)
↳29 QDP
↳30 UsableRulesProof (⇔)
↳31 QDP
↳32 QReductionProof (⇔)
↳33 QDP
↳34 Rewriting (⇔)
↳35 QDP
↳36 UsableRulesProof (⇔)
↳37 QDP
↳38 QReductionProof (⇔)
↳39 QDP
↳40 Instantiation (⇔)
↳41 QDP
↳42 NonInfProof (⇔)
↳43 AND
↳44 QDP
↳45 DependencyGraphProof (⇔)
↳46 TRUE
↳47 QDP
↳48 DependencyGraphProof (⇔)
↳49 TRUE
↳50 QDP
↳51 UsableRulesProof (⇔)
↳52 QDP
↳53 QReductionProof (⇔)
↳54 QDP
↳55 QDPSizeChangeProof (⇔)
↳56 TRUE
app(x, y) → helpa(0, plus(length(x), length(y)), x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpa(c, l, ys, zs) → if(ge(c, l), c, l, ys, zs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if(true, c, l, ys, zs) → nil
if(false, c, l, ys, zs) → helpb(c, l, greater(ys, zs), smaller(ys, zs))
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
helpb(c, l, cons(y, ys), zs) → cons(y, helpa(s(c), l, ys, zs))
app(x, y) → helpa(0, plus(length(x), length(y)), x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpa(c, l, ys, zs) → if(ge(c, l), c, l, ys, zs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if(true, c, l, ys, zs) → nil
if(false, c, l, ys, zs) → helpb(c, l, greater(ys, zs), smaller(ys, zs))
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
helpb(c, l, cons(y, ys), zs) → cons(y, helpa(s(c), l, ys, zs))
app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)
APP(x, y) → HELPA(0, plus(length(x), length(y)), x, y)
APP(x, y) → PLUS(length(x), length(y))
APP(x, y) → LENGTH(x)
APP(x, y) → LENGTH(y)
PLUS(x, s(y)) → PLUS(x, y)
LENGTH(cons(x, y)) → LENGTH(y)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)
HELPA(c, l, ys, zs) → GE(c, l)
GE(s(x), s(y)) → GE(x, y)
IF(false, c, l, ys, zs) → HELPB(c, l, greater(ys, zs), smaller(ys, zs))
IF(false, c, l, ys, zs) → GREATER(ys, zs)
IF(false, c, l, ys, zs) → SMALLER(ys, zs)
GREATER(ys, zs) → HELPC(ge(length(ys), length(zs)), ys, zs)
GREATER(ys, zs) → GE(length(ys), length(zs))
GREATER(ys, zs) → LENGTH(ys)
GREATER(ys, zs) → LENGTH(zs)
SMALLER(ys, zs) → HELPC(ge(length(ys), length(zs)), zs, ys)
SMALLER(ys, zs) → GE(length(ys), length(zs))
SMALLER(ys, zs) → LENGTH(ys)
SMALLER(ys, zs) → LENGTH(zs)
HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
app(x, y) → helpa(0, plus(length(x), length(y)), x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpa(c, l, ys, zs) → if(ge(c, l), c, l, ys, zs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if(true, c, l, ys, zs) → nil
if(false, c, l, ys, zs) → helpb(c, l, greater(ys, zs), smaller(ys, zs))
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
helpb(c, l, cons(y, ys), zs) → cons(y, helpa(s(c), l, ys, zs))
app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)
GE(s(x), s(y)) → GE(x, y)
app(x, y) → helpa(0, plus(length(x), length(y)), x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpa(c, l, ys, zs) → if(ge(c, l), c, l, ys, zs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if(true, c, l, ys, zs) → nil
if(false, c, l, ys, zs) → helpb(c, l, greater(ys, zs), smaller(ys, zs))
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
helpb(c, l, cons(y, ys), zs) → cons(y, helpa(s(c), l, ys, zs))
app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)
GE(s(x), s(y)) → GE(x, y)
app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)
app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)
GE(s(x), s(y)) → GE(x, y)
From the DPs we obtained the following set of size-change graphs:
LENGTH(cons(x, y)) → LENGTH(y)
app(x, y) → helpa(0, plus(length(x), length(y)), x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpa(c, l, ys, zs) → if(ge(c, l), c, l, ys, zs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if(true, c, l, ys, zs) → nil
if(false, c, l, ys, zs) → helpb(c, l, greater(ys, zs), smaller(ys, zs))
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
helpb(c, l, cons(y, ys), zs) → cons(y, helpa(s(c), l, ys, zs))
app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)
LENGTH(cons(x, y)) → LENGTH(y)
app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)
app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)
LENGTH(cons(x, y)) → LENGTH(y)
From the DPs we obtained the following set of size-change graphs:
IF(false, c, l, ys, zs) → HELPB(c, l, greater(ys, zs), smaller(ys, zs))
HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)
app(x, y) → helpa(0, plus(length(x), length(y)), x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpa(c, l, ys, zs) → if(ge(c, l), c, l, ys, zs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if(true, c, l, ys, zs) → nil
if(false, c, l, ys, zs) → helpb(c, l, greater(ys, zs), smaller(ys, zs))
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
helpb(c, l, cons(y, ys), zs) → cons(y, helpa(s(c), l, ys, zs))
app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)
IF(false, c, l, ys, zs) → HELPB(c, l, greater(ys, zs), smaller(ys, zs))
HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)
app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
helpa(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
helpb(x0, x1, cons(x2, x3), x4)
IF(false, c, l, ys, zs) → HELPB(c, l, greater(ys, zs), smaller(ys, zs))
HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
HELPA(s(z0), z1, z3, z4) → IF(ge(s(z0), z1), s(z0), z1, z3, z4)
IF(false, c, l, ys, zs) → HELPB(c, l, greater(ys, zs), smaller(ys, zs))
HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
HELPA(s(z0), z1, z3, z4) → IF(ge(s(z0), z1), s(z0), z1, z3, z4)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), smaller(ys, zs))
HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)
IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), smaller(ys, zs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)
IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), smaller(ys, zs))
length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
greater(x0, x1)
HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)
IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), smaller(ys, zs))
length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), helpc(ge(length(ys), length(zs)), zs, ys))
HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)
IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), helpc(ge(length(ys), length(zs)), zs, ys))
length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)
IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), helpc(ge(length(ys), length(zs)), zs, ys))
length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
smaller(x0, x1)
HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)
IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), helpc(ge(length(ys), length(zs)), zs, ys))
length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
helpc(true, x0, x1)
helpc(false, x0, x1)
HELPA(s(z0), z1, z3, z4) → IF(ge(s(z0), z1), s(z0), z1, z3, z4)
HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), helpc(ge(length(ys), length(zs)), zs, ys))
HELPA(s(z0), z1, z3, z4) → IF(ge(s(z0), z1), s(z0), z1, z3, z4)
length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
helpc(true, x0, x1)
helpc(false, x0, x1)
(1) (HELPB(x9, x10, helpc(ge(length(x11), length(x12)), x11, x12), helpc(ge(length(x11), length(x12)), x12, x11))=HELPB(x13, x14, cons(x15, x16), x17) ⇒ HELPB(x13, x14, cons(x15, x16), x17)≥HELPA(s(x13), x14, x16, x17))
(2) (ge(x53, x54)=x52∧helpc(x52, x11, x12)=cons(x15, x16)∧ge(x56, x57)=x55∧helpc(x55, x12, x11)=x17 ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))
(3) (x59=cons(x15, x16)∧ge(x53, x54)=true∧ge(x56, x57)=x55∧helpc(x55, x58, x59)=x17 ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))
(4) (x60=cons(x15, x16)∧ge(x53, x54)=false∧ge(x56, x57)=x55∧helpc(x55, x60, x61)=x17 ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))
(5) (ge(x53, x54)=true∧ge(x56, x57)=x55∧cons(x15, x16)=x62∧helpc(x55, x58, x62)=x17 ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))
(6) (ge(x53, x54)=false∧ge(x56, x57)=x55∧cons(x15, x16)=x77∧helpc(x55, x77, x61)=x17 ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))
(7) (true=true∧ge(x56, x57)=x55∧cons(x15, x16)=x62∧helpc(x55, x58, x62)=x17 ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))
(8) (ge(x66, x65)=true∧ge(x56, x57)=x55∧cons(x15, x16)=x62∧helpc(x55, x58, x62)=x17∧(∀x67,x68,x69,x70,x71,x72,x73,x74,x75,x76:ge(x66, x65)=true∧ge(x67, x68)=x69∧cons(x70, x71)=x72∧helpc(x69, x73, x72)=x74 ⇒ HELPB(x75, x76, cons(x70, x71), x74)≥HELPA(s(x75), x76, x71, x74)) ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))
(9) (HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))
(10) (HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17) ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))
(11) (false=false∧ge(x56, x57)=x55∧cons(x15, x16)=x77∧helpc(x55, x77, x61)=x17 ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))
(12) (ge(x81, x80)=false∧ge(x56, x57)=x55∧cons(x15, x16)=x77∧helpc(x55, x77, x61)=x17∧(∀x82,x83,x84,x85,x86,x87,x88,x89,x90,x91:ge(x81, x80)=false∧ge(x82, x83)=x84∧cons(x85, x86)=x87∧helpc(x84, x87, x88)=x89 ⇒ HELPB(x90, x91, cons(x85, x86), x89)≥HELPA(s(x90), x91, x86, x89)) ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))
(13) (HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17) ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))
(14) (HELPA(s(x18), x19, x21, x22)=HELPA(x23, x24, x25, x26) ⇒ HELPA(x23, x24, x25, x26)≥IF(ge(x23, x24), x23, x24, x25, x26))
(15) (HELPA(s(x18), x19, x21, x22)≥IF(ge(s(x18), x19), s(x18), x19, x21, x22))
(16) (IF(ge(x40, x41), x40, x41, x42, x43)=IF(false, x44, x45, x46, x47) ⇒ IF(false, x44, x45, x46, x47)≥HELPB(x44, x45, helpc(ge(length(x46), length(x47)), x46, x47), helpc(ge(length(x46), length(x47)), x47, x46)))
(17) (ge(x40, x41)=false ⇒ IF(false, x40, x41, x42, x43)≥HELPB(x40, x41, helpc(ge(length(x42), length(x43)), x42, x43), helpc(ge(length(x42), length(x43)), x43, x42)))
(18) (false=false ⇒ IF(false, 0, s(x93), x42, x43)≥HELPB(0, s(x93), helpc(ge(length(x42), length(x43)), x42, x43), helpc(ge(length(x42), length(x43)), x43, x42)))
(19) (ge(x95, x94)=false∧(∀x96,x97:ge(x95, x94)=false ⇒ IF(false, x95, x94, x96, x97)≥HELPB(x95, x94, helpc(ge(length(x96), length(x97)), x96, x97), helpc(ge(length(x96), length(x97)), x97, x96))) ⇒ IF(false, s(x95), s(x94), x42, x43)≥HELPB(s(x95), s(x94), helpc(ge(length(x42), length(x43)), x42, x43), helpc(ge(length(x42), length(x43)), x43, x42)))
(20) (IF(false, 0, s(x93), x42, x43)≥HELPB(0, s(x93), helpc(ge(length(x42), length(x43)), x42, x43), helpc(ge(length(x42), length(x43)), x43, x42)))
(21) (IF(false, x95, x94, x42, x43)≥HELPB(x95, x94, helpc(ge(length(x42), length(x43)), x42, x43), helpc(ge(length(x42), length(x43)), x43, x42)) ⇒ IF(false, s(x95), s(x94), x42, x43)≥HELPB(s(x95), s(x94), helpc(ge(length(x42), length(x43)), x42, x43), helpc(ge(length(x42), length(x43)), x43, x42)))
POL(0) = 0
POL(HELPA(x1, x2, x3, x4)) = 1 - x1 + x2
POL(HELPB(x1, x2, x3, x4)) = 1 - x1 + x2 - x3
POL(IF(x1, x2, x3, x4, x5)) = 1 - x1 - x2 + x3
POL(c) = -1
POL(cons(x1, x2)) = 0
POL(false) = 0
POL(ge(x1, x2)) = 0
POL(helpc(x1, x2, x3)) = 0
POL(length(x1)) = 0
POL(nil) = 0
POL(s(x1)) = 1 + x1
POL(true) = 0
The following pairs are in Pbound:
HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
The following rules are usable:
IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), helpc(ge(length(ys), length(zs)), zs, ys))
zs → helpc(false, ys, zs)
ys → helpc(true, ys, zs)
ge(x, y) → ge(s(x), s(y))
false → ge(0, s(x))
true → ge(x, 0)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)
IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), helpc(ge(length(ys), length(zs)), zs, ys))
length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
helpc(true, x0, x1)
helpc(false, x0, x1)
HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)
length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
helpc(true, x0, x1)
helpc(false, x0, x1)
PLUS(x, s(y)) → PLUS(x, y)
app(x, y) → helpa(0, plus(length(x), length(y)), x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpa(c, l, ys, zs) → if(ge(c, l), c, l, ys, zs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if(true, c, l, ys, zs) → nil
if(false, c, l, ys, zs) → helpb(c, l, greater(ys, zs), smaller(ys, zs))
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
helpb(c, l, cons(y, ys), zs) → cons(y, helpa(s(c), l, ys, zs))
app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)
PLUS(x, s(y)) → PLUS(x, y)
app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)
app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)
PLUS(x, s(y)) → PLUS(x, y)
From the DPs we obtained the following set of size-change graphs: