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 QDPSizeChangeProof (⇔)
↳27 TRUE
↳28 QDP
↳29 UsableRulesProof (⇔)
↳30 QDP
↳31 QReductionProof (⇔)
↳32 QDP
↳33 Instantiation (⇔)
↳34 QDP
↳35 NonInfProof (⇔)
↳36 QDP
↳37 DependencyGraphProof (⇔)
↳38 TRUE
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
rev(x) → if(x, eq(0, length(x)), nil, 0, length(x))
if(x, true, z, c, l) → z
if(x, false, z, c, l) → help(s(c), l, x, z)
help(c, l, cons(x, y), z) → if(append(y, cons(x, nil)), ge(c, l), cons(x, z), c, l)
append(nil, y) → y
append(cons(x, y), z) → cons(x, append(y, z))
length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
rev(x) → if(x, eq(0, length(x)), nil, 0, length(x))
if(x, true, z, c, l) → z
if(x, false, z, c, l) → help(s(c), l, x, z)
help(c, l, cons(x, y), z) → if(append(y, cons(x, nil)), ge(c, l), cons(x, z), c, l)
append(nil, y) → y
append(cons(x, y), z) → cons(x, append(y, z))
length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
rev(x0)
if(x0, true, x1, x2, x3)
if(x0, false, x1, x2, x3)
help(x0, x1, cons(x2, x3), x4)
append(nil, x0)
append(cons(x0, x1), x2)
length(nil)
length(cons(x0, x1))
GE(s(x), s(y)) → GE(x, y)
REV(x) → IF(x, eq(0, length(x)), nil, 0, length(x))
REV(x) → LENGTH(x)
IF(x, false, z, c, l) → HELP(s(c), l, x, z)
HELP(c, l, cons(x, y), z) → IF(append(y, cons(x, nil)), ge(c, l), cons(x, z), c, l)
HELP(c, l, cons(x, y), z) → APPEND(y, cons(x, nil))
HELP(c, l, cons(x, y), z) → GE(c, l)
APPEND(cons(x, y), z) → APPEND(y, z)
LENGTH(cons(x, y)) → LENGTH(y)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
rev(x) → if(x, eq(0, length(x)), nil, 0, length(x))
if(x, true, z, c, l) → z
if(x, false, z, c, l) → help(s(c), l, x, z)
help(c, l, cons(x, y), z) → if(append(y, cons(x, nil)), ge(c, l), cons(x, z), c, l)
append(nil, y) → y
append(cons(x, y), z) → cons(x, append(y, z))
length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
rev(x0)
if(x0, true, x1, x2, x3)
if(x0, false, x1, x2, x3)
help(x0, x1, cons(x2, x3), x4)
append(nil, x0)
append(cons(x0, x1), x2)
length(nil)
length(cons(x0, x1))
LENGTH(cons(x, y)) → LENGTH(y)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
rev(x) → if(x, eq(0, length(x)), nil, 0, length(x))
if(x, true, z, c, l) → z
if(x, false, z, c, l) → help(s(c), l, x, z)
help(c, l, cons(x, y), z) → if(append(y, cons(x, nil)), ge(c, l), cons(x, z), c, l)
append(nil, y) → y
append(cons(x, y), z) → cons(x, append(y, z))
length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
rev(x0)
if(x0, true, x1, x2, x3)
if(x0, false, x1, x2, x3)
help(x0, x1, cons(x2, x3), x4)
append(nil, x0)
append(cons(x0, x1), x2)
length(nil)
length(cons(x0, x1))
LENGTH(cons(x, y)) → LENGTH(y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
rev(x0)
if(x0, true, x1, x2, x3)
if(x0, false, x1, x2, x3)
help(x0, x1, cons(x2, x3), x4)
append(nil, x0)
append(cons(x0, x1), x2)
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
rev(x0)
if(x0, true, x1, x2, x3)
if(x0, false, x1, x2, x3)
help(x0, x1, cons(x2, x3), x4)
append(nil, x0)
append(cons(x0, x1), x2)
length(nil)
length(cons(x0, x1))
LENGTH(cons(x, y)) → LENGTH(y)
From the DPs we obtained the following set of size-change graphs:
APPEND(cons(x, y), z) → APPEND(y, z)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
rev(x) → if(x, eq(0, length(x)), nil, 0, length(x))
if(x, true, z, c, l) → z
if(x, false, z, c, l) → help(s(c), l, x, z)
help(c, l, cons(x, y), z) → if(append(y, cons(x, nil)), ge(c, l), cons(x, z), c, l)
append(nil, y) → y
append(cons(x, y), z) → cons(x, append(y, z))
length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
rev(x0)
if(x0, true, x1, x2, x3)
if(x0, false, x1, x2, x3)
help(x0, x1, cons(x2, x3), x4)
append(nil, x0)
append(cons(x0, x1), x2)
length(nil)
length(cons(x0, x1))
APPEND(cons(x, y), z) → APPEND(y, z)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
rev(x0)
if(x0, true, x1, x2, x3)
if(x0, false, x1, x2, x3)
help(x0, x1, cons(x2, x3), x4)
append(nil, x0)
append(cons(x0, x1), x2)
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
rev(x0)
if(x0, true, x1, x2, x3)
if(x0, false, x1, x2, x3)
help(x0, x1, cons(x2, x3), x4)
append(nil, x0)
append(cons(x0, x1), x2)
length(nil)
length(cons(x0, x1))
APPEND(cons(x, y), z) → APPEND(y, z)
From the DPs we obtained the following set of size-change graphs:
GE(s(x), s(y)) → GE(x, y)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
rev(x) → if(x, eq(0, length(x)), nil, 0, length(x))
if(x, true, z, c, l) → z
if(x, false, z, c, l) → help(s(c), l, x, z)
help(c, l, cons(x, y), z) → if(append(y, cons(x, nil)), ge(c, l), cons(x, z), c, l)
append(nil, y) → y
append(cons(x, y), z) → cons(x, append(y, z))
length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
rev(x0)
if(x0, true, x1, x2, x3)
if(x0, false, x1, x2, x3)
help(x0, x1, cons(x2, x3), x4)
append(nil, x0)
append(cons(x0, x1), x2)
length(nil)
length(cons(x0, x1))
GE(s(x), s(y)) → GE(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
rev(x0)
if(x0, true, x1, x2, x3)
if(x0, false, x1, x2, x3)
help(x0, x1, cons(x2, x3), x4)
append(nil, x0)
append(cons(x0, x1), x2)
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
rev(x0)
if(x0, true, x1, x2, x3)
if(x0, false, x1, x2, x3)
help(x0, x1, cons(x2, x3), x4)
append(nil, x0)
append(cons(x0, x1), x2)
length(nil)
length(cons(x0, x1))
GE(s(x), s(y)) → GE(x, y)
From the DPs we obtained the following set of size-change graphs:
HELP(c, l, cons(x, y), z) → IF(append(y, cons(x, nil)), ge(c, l), cons(x, z), c, l)
IF(x, false, z, c, l) → HELP(s(c), l, x, z)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
rev(x) → if(x, eq(0, length(x)), nil, 0, length(x))
if(x, true, z, c, l) → z
if(x, false, z, c, l) → help(s(c), l, x, z)
help(c, l, cons(x, y), z) → if(append(y, cons(x, nil)), ge(c, l), cons(x, z), c, l)
append(nil, y) → y
append(cons(x, y), z) → cons(x, append(y, z))
length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
rev(x0)
if(x0, true, x1, x2, x3)
if(x0, false, x1, x2, x3)
help(x0, x1, cons(x2, x3), x4)
append(nil, x0)
append(cons(x0, x1), x2)
length(nil)
length(cons(x0, x1))
HELP(c, l, cons(x, y), z) → IF(append(y, cons(x, nil)), ge(c, l), cons(x, z), c, l)
IF(x, false, z, c, l) → HELP(s(c), l, x, z)
append(nil, y) → y
append(cons(x, y), z) → cons(x, append(y, z))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
rev(x0)
if(x0, true, x1, x2, x3)
if(x0, false, x1, x2, x3)
help(x0, x1, cons(x2, x3), x4)
append(nil, x0)
append(cons(x0, x1), x2)
length(nil)
length(cons(x0, x1))
rev(x0)
if(x0, true, x1, x2, x3)
if(x0, false, x1, x2, x3)
help(x0, x1, cons(x2, x3), x4)
length(nil)
length(cons(x0, x1))
HELP(c, l, cons(x, y), z) → IF(append(y, cons(x, nil)), ge(c, l), cons(x, z), c, l)
IF(x, false, z, c, l) → HELP(s(c), l, x, z)
append(nil, y) → y
append(cons(x, y), z) → cons(x, append(y, z))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, x0)
append(cons(x0, x1), x2)
HELP(s(z2), z3, cons(x2, x3), z1) → IF(append(x3, cons(x2, nil)), ge(s(z2), z3), cons(x2, z1), s(z2), z3)
IF(x, false, z, c, l) → HELP(s(c), l, x, z)
HELP(s(z2), z3, cons(x2, x3), z1) → IF(append(x3, cons(x2, nil)), ge(s(z2), z3), cons(x2, z1), s(z2), z3)
append(nil, y) → y
append(cons(x, y), z) → cons(x, append(y, z))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, x0)
append(cons(x0, x1), x2)
(1) (HELP(s(x7), x8, x5, x6)=HELP(x9, x10, cons(x11, x12), x13) ⇒ HELP(x9, x10, cons(x11, x12), x13)≥IF(append(x12, cons(x11, nil)), ge(x9, x10), cons(x11, x13), x9, x10))
(2) (HELP(s(x7), x8, cons(x11, x12), x6)≥IF(append(x12, cons(x11, nil)), ge(s(x7), x8), cons(x11, x6), s(x7), x8))
(3) (IF(append(x17, cons(x16, nil)), ge(x14, x15), cons(x16, x18), x14, x15)=IF(x19, false, x20, x21, x22) ⇒ IF(x19, false, x20, x21, x22)≥HELP(s(x21), x22, x19, x20))
(4) (cons(x16, nil)=x27∧append(x17, x27)=x19∧ge(x14, x15)=false ⇒ IF(x19, false, cons(x16, x18), x14, x15)≥HELP(s(x14), x15, x19, cons(x16, x18)))
(5) (false=false∧cons(x16, nil)=x27∧append(x17, x27)=x19 ⇒ IF(x19, false, cons(x16, x18), 0, s(x29))≥HELP(s(0), s(x29), x19, cons(x16, x18)))
(6) (ge(x31, x30)=false∧cons(x16, nil)=x27∧append(x17, x27)=x19∧(∀x32,x33,x34,x35,x36:ge(x31, x30)=false∧cons(x32, nil)=x33∧append(x34, x33)=x35 ⇒ IF(x35, false, cons(x32, x36), x31, x30)≥HELP(s(x31), x30, x35, cons(x32, x36))) ⇒ IF(x19, false, cons(x16, x18), s(x31), s(x30))≥HELP(s(s(x31)), s(x30), x19, cons(x16, x18)))
(7) (IF(x19, false, cons(x16, x18), 0, s(x29))≥HELP(s(0), s(x29), x19, cons(x16, x18)))
(8) (IF(x19, false, cons(x16, x18), x31, x30)≥HELP(s(x31), x30, x19, cons(x16, x18)) ⇒ IF(x19, false, cons(x16, x18), s(x31), s(x30))≥HELP(s(s(x31)), s(x30), x19, cons(x16, x18)))
POL(0) = 1
POL(HELP(x1, x2, x3, x4)) = -1 - x1 + x2 - x3 + x4
POL(IF(x1, x2, x3, x4, x5)) = -1 - x2 - x3 - x4 + x5
POL(append(x1, x2)) = 0
POL(c) = -2
POL(cons(x1, x2)) = 0
POL(false) = 0
POL(ge(x1, x2)) = 0
POL(nil) = 0
POL(s(x1)) = 1 + x1
POL(true) = 0
The following pairs are in Pbound:
IF(x, false, z, c, l) → HELP(s(c), l, x, z)
The following rules are usable:
IF(x, false, z, c, l) → HELP(s(c), l, x, z)
ge(x, y) → ge(s(x), s(y))
false → ge(0, s(y))
true → ge(x, 0)
HELP(c, l, cons(x, y), z) → IF(append(y, cons(x, nil)), ge(c, l), cons(x, z), c, l)
append(nil, y) → y
append(cons(x, y), z) → cons(x, append(y, z))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, x0)
append(cons(x0, x1), x2)