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 AND
↳30 QDP
↳31 DependencyGraphProof (⇔)
↳32 TRUE
↳33 QDP
↳34 DependencyGraphProof (⇔)
↳35 TRUE
↳36 QDP
↳37 UsableRulesProof (⇔)
↳38 QDP
↳39 QReductionProof (⇔)
↳40 QDP
↳41 QDPSizeChangeProof (⇔)
↳42 TRUE
↳43 QDP
↳44 UsableRulesProof (⇔)
↳45 QDP
↳46 QReductionProof (⇔)
↳47 QDP
↳48 QDPSizeChangeProof (⇔)
↳49 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, ys, zs)
take(0, cons(x, xs), ys) → x
take(0, nil, cons(y, ys)) → y
take(s(c), cons(x, xs), ys) → take(c, xs, ys)
take(s(c), nil, cons(y, ys)) → take(c, nil, ys)
helpb(c, l, ys, zs) → cons(take(c, 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, ys, zs)
take(0, cons(x, xs), ys) → x
take(0, nil, cons(y, ys)) → y
take(s(c), cons(x, xs), ys) → take(c, xs, ys)
take(s(c), nil, cons(y, ys)) → take(c, nil, ys)
helpb(c, l, ys, zs) → cons(take(c, ys, zs), 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)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)
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, ys, zs)
TAKE(s(c), cons(x, xs), ys) → TAKE(c, xs, ys)
TAKE(s(c), nil, cons(y, ys)) → TAKE(c, nil, ys)
HELPB(c, l, ys, zs) → TAKE(c, ys, zs)
HELPB(c, l, 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, ys, zs)
take(0, cons(x, xs), ys) → x
take(0, nil, cons(y, ys)) → y
take(s(c), cons(x, xs), ys) → take(c, xs, ys)
take(s(c), nil, cons(y, ys)) → take(c, nil, ys)
helpb(c, l, ys, zs) → cons(take(c, ys, zs), 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)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)
TAKE(s(c), nil, cons(y, ys)) → TAKE(c, nil, ys)
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, ys, zs)
take(0, cons(x, xs), ys) → x
take(0, nil, cons(y, ys)) → y
take(s(c), cons(x, xs), ys) → take(c, xs, ys)
take(s(c), nil, cons(y, ys)) → take(c, nil, ys)
helpb(c, l, ys, zs) → cons(take(c, ys, zs), 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)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)
TAKE(s(c), nil, cons(y, ys)) → TAKE(c, nil, ys)
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)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)
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)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)
TAKE(s(c), nil, cons(y, ys)) → TAKE(c, nil, ys)
From the DPs we obtained the following set of size-change graphs:
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, ys, zs)
take(0, cons(x, xs), ys) → x
take(0, nil, cons(y, ys)) → y
take(s(c), cons(x, xs), ys) → take(c, xs, ys)
take(s(c), nil, cons(y, ys)) → take(c, nil, ys)
helpb(c, l, ys, zs) → cons(take(c, ys, zs), 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)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)
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)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)
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)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)
GE(s(x), s(y)) → GE(x, y)
From the DPs we obtained the following set of size-change graphs:
IF(false, c, l, ys, zs) → HELPB(c, l, ys, zs)
HELPB(c, l, 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, ys, zs)
take(0, cons(x, xs), ys) → x
take(0, nil, cons(y, ys)) → y
take(s(c), cons(x, xs), ys) → take(c, xs, ys)
take(s(c), nil, cons(y, ys)) → take(c, nil, ys)
helpb(c, l, ys, zs) → cons(take(c, ys, zs), 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)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)
IF(false, c, l, ys, zs) → HELPB(c, l, ys, zs)
HELPB(c, l, 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)
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)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)
app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)
IF(false, c, l, ys, zs) → HELPB(c, l, ys, zs)
HELPB(c, l, 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)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
HELPA(s(z0), z1, z2, z3) → IF(ge(s(z0), z1), s(z0), z1, z2, z3)
IF(false, c, l, ys, zs) → HELPB(c, l, ys, zs)
HELPB(c, l, ys, zs) → HELPA(s(c), l, ys, zs)
HELPA(s(z0), z1, z2, z3) → IF(ge(s(z0), z1), s(z0), z1, z2, z3)
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))
(1) (IF(ge(x8, x9), x8, x9, x10, x11)=IF(false, x12, x13, x14, x15) ⇒ IF(false, x12, x13, x14, x15)≥HELPB(x12, x13, x14, x15))
(2) (ge(x8, x9)=false ⇒ IF(false, x8, x9, x10, x11)≥HELPB(x8, x9, x10, x11))
(3) (false=false ⇒ IF(false, 0, s(x49), x10, x11)≥HELPB(0, s(x49), x10, x11))
(4) (ge(x51, x50)=false∧(∀x52,x53:ge(x51, x50)=false ⇒ IF(false, x51, x50, x52, x53)≥HELPB(x51, x50, x52, x53)) ⇒ IF(false, s(x51), s(x50), x10, x11)≥HELPB(s(x51), s(x50), x10, x11))
(5) (IF(false, 0, s(x49), x10, x11)≥HELPB(0, s(x49), x10, x11))
(6) (IF(false, x51, x50, x10, x11)≥HELPB(x51, x50, x10, x11) ⇒ IF(false, s(x51), s(x50), x10, x11)≥HELPB(s(x51), s(x50), x10, x11))
(7) (HELPB(x16, x17, x18, x19)=HELPB(x20, x21, x22, x23) ⇒ HELPB(x20, x21, x22, x23)≥HELPA(s(x20), x21, x22, x23))
(8) (HELPB(x16, x17, x18, x19)≥HELPA(s(x16), x17, x18, x19))
(9) (HELPA(s(x36), x37, x38, x39)=HELPA(x40, x41, x42, x43) ⇒ HELPA(x40, x41, x42, x43)≥IF(ge(x40, x41), x40, x41, x42, x43))
(10) (HELPA(s(x36), x37, x38, x39)≥IF(ge(s(x36), x37), s(x36), x37, x38, x39))
POL(0) = 0
POL(HELPA(x1, x2, x3, x4)) = 1 - x1 + x2 + x4
POL(HELPB(x1, x2, x3, x4)) = 1 - x1 + x2 + x4
POL(IF(x1, x2, x3, x4, x5)) = 1 - x1 - x2 + x3 + x5
POL(c) = -1
POL(false) = 0
POL(ge(x1, x2)) = 0
POL(s(x1)) = 1 + x1
POL(true) = 1
The following pairs are in Pbound:
HELPB(c, l, ys, zs) → HELPA(s(c), l, ys, zs)
The following rules are usable:
IF(false, c, l, ys, zs) → HELPB(c, l, ys, zs)
false → ge(0, s(x))
true → ge(x, 0)
ge(x, y) → ge(s(x), s(y))
IF(false, c, l, ys, zs) → HELPB(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)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
HELPB(c, l, 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)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
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, ys, zs)
take(0, cons(x, xs), ys) → x
take(0, nil, cons(y, ys)) → y
take(s(c), cons(x, xs), ys) → take(c, xs, ys)
take(s(c), nil, cons(y, ys)) → take(c, nil, ys)
helpb(c, l, ys, zs) → cons(take(c, ys, zs), 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)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)
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)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)
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)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)
LENGTH(cons(x, y)) → LENGTH(y)
From the DPs we obtained the following set of size-change graphs:
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, ys, zs)
take(0, cons(x, xs), ys) → x
take(0, nil, cons(y, ys)) → y
take(s(c), cons(x, xs), ys) → take(c, xs, ys)
take(s(c), nil, cons(y, ys)) → take(c, nil, ys)
helpb(c, l, ys, zs) → cons(take(c, ys, zs), 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)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)
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)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)
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)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)
PLUS(x, s(y)) → PLUS(x, y)
From the DPs we obtained the following set of size-change graphs: