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 QDPSizeChangeProof (⇔)
↳34 TRUE
↳35 QDP
↳36 UsableRulesProof (⇔)
↳37 QDP
↳38 QReductionProof (⇔)
↳39 QDP
↳40 QDPSizeChangeProof (⇔)
↳41 TRUE
↳42 QDP
↳43 UsableRulesProof (⇔)
↳44 QDP
↳45 QReductionProof (⇔)
↳46 QDP
↳47 Induction-Processor (⇐)
↳48 AND
↳49 QDP
↳50 PisEmptyProof (⇔)
↳51 TRUE
↳52 QTRS
↳53 QTRSRRRProof (⇔)
↳54 QTRS
↳55 QTRSRRRProof (⇔)
↳56 QTRS
↳57 QTRSRRRProof (⇔)
↳58 QTRS
↳59 QTRSRRRProof (⇔)
↳60 QTRS
↳61 QTRSRRRProof (⇔)
↳62 QTRS
↳63 RisEmptyProof (⇔)
↳64 TRUE
↳65 RisEmptyProof (⇔)
↳66 TRUE
↳67 RisEmptyProof (⇔)
↳68 TRUE
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
addList(x, y) → if(le(0, min(len(x), len(y))), 0, x, y, nil)
if(false, c, x, y, z) → z
if(true, c, xs, ys, z) → if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
addList(x, y) → if(le(0, min(len(x), len(y))), 0, x, y, nil)
if(false, c, x, y, z) → z
if(true, c, xs, ys, z) → if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
MIN(s(x), s(y)) → MIN(x, y)
LEN(cons(x, xs)) → LEN(xs)
SUM(x, s(y)) → SUM(x, y)
LE(s(x), s(y)) → LE(x, y)
TAKE(s(x), cons(y, ys)) → TAKE(x, ys)
ADDLIST(x, y) → IF(le(0, min(len(x), len(y))), 0, x, y, nil)
ADDLIST(x, y) → LE(0, min(len(x), len(y)))
ADDLIST(x, y) → MIN(len(x), len(y))
ADDLIST(x, y) → LEN(x)
ADDLIST(x, y) → LEN(y)
IF(true, c, xs, ys, z) → IF(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
IF(true, c, xs, ys, z) → LE(s(c), min(len(xs), len(ys)))
IF(true, c, xs, ys, z) → MIN(len(xs), len(ys))
IF(true, c, xs, ys, z) → LEN(xs)
IF(true, c, xs, ys, z) → LEN(ys)
IF(true, c, xs, ys, z) → SUM(take(c, xs), take(c, ys))
IF(true, c, xs, ys, z) → TAKE(c, xs)
IF(true, c, xs, ys, z) → TAKE(c, ys)
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
addList(x, y) → if(le(0, min(len(x), len(y))), 0, x, y, nil)
if(false, c, x, y, z) → z
if(true, c, xs, ys, z) → if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
TAKE(s(x), cons(y, ys)) → TAKE(x, ys)
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
addList(x, y) → if(le(0, min(len(x), len(y))), 0, x, y, nil)
if(false, c, x, y, z) → z
if(true, c, xs, ys, z) → if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
TAKE(s(x), cons(y, ys)) → TAKE(x, ys)
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
TAKE(s(x), cons(y, ys)) → TAKE(x, ys)
From the DPs we obtained the following set of size-change graphs:
LE(s(x), s(y)) → LE(x, y)
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
addList(x, y) → if(le(0, min(len(x), len(y))), 0, x, y, nil)
if(false, c, x, y, z) → z
if(true, c, xs, ys, z) → if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
LE(s(x), s(y)) → LE(x, y)
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
LE(s(x), s(y)) → LE(x, y)
From the DPs we obtained the following set of size-change graphs:
SUM(x, s(y)) → SUM(x, y)
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
addList(x, y) → if(le(0, min(len(x), len(y))), 0, x, y, nil)
if(false, c, x, y, z) → z
if(true, c, xs, ys, z) → if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
SUM(x, s(y)) → SUM(x, y)
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
SUM(x, s(y)) → SUM(x, y)
From the DPs we obtained the following set of size-change graphs:
LEN(cons(x, xs)) → LEN(xs)
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
addList(x, y) → if(le(0, min(len(x), len(y))), 0, x, y, nil)
if(false, c, x, y, z) → z
if(true, c, xs, ys, z) → if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
LEN(cons(x, xs)) → LEN(xs)
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
LEN(cons(x, xs)) → LEN(xs)
From the DPs we obtained the following set of size-change graphs:
MIN(s(x), s(y)) → MIN(x, y)
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
addList(x, y) → if(le(0, min(len(x), len(y))), 0, x, y, nil)
if(false, c, x, y, z) → z
if(true, c, xs, ys, z) → if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
MIN(s(x), s(y)) → MIN(x, y)
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
MIN(s(x), s(y)) → MIN(x, y)
From the DPs we obtained the following set of size-change graphs:
IF(true, c, xs, ys, z) → IF(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
addList(x, y) → if(le(0, min(len(x), len(y))), 0, x, y, nil)
if(false, c, x, y, z) → z
if(true, c, xs, ys, z) → if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
IF(true, c, xs, ys, z) → IF(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
IF(true, c, xs, ys, z) → IF(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
POL(0) = 0
POL(IF(x1, x2, x3, x4, x5)) = x1 + x2
POL(cons(x1, x2)) = x1 + x2
POL(false) = 0
POL(le(x1, x2)) = 1
POL(len(x1)) = 0
POL(min(x1, x2)) = 0
POL(nil) = 0
POL(s(x1)) = 0
POL(sum(x1, x2)) = 1 + x1
POL(take(x1, x2)) = x2
POL(true) = 1
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
le'(s(x46), 0) → true
le'(s(x56), s(y36)) → le'(x56, y36)
le'(0, x105) → false
len(nil) → 0
len(cons(x7, xs')) → s(len(xs'))
min(0, y10) → 0
min(s(x26), 0) → 0
min(s(x36), s(y23)) → min(x36, y23)
le(s(x46), 0) → false
le(s(x56), s(y36)) → le(x56, y36)
take(0, cons(y43, ys12)) → y43
take(s(x75), cons(y50, ys15)) → take(x75, ys15)
sum(x85, 0) → x85
sum(x95, s(y63)) → s(sum(x95, y63))
le(0, x105) → true
take(0, nil) → 0
take(s(x2), nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a23](0, 0) → true
equal_sort[a23](0, s(x0)) → false
equal_sort[a23](s(x0), 0) → false
equal_sort[a23](s(x0), s(x1)) → equal_sort[a23](x0, x1)
equal_sort[a24](nil, nil) → true
equal_sort[a24](nil, cons(x0, x1)) → false
equal_sort[a24](cons(x0, x1), nil) → false
equal_sort[a24](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a24](x0, x2), equal_sort[a24](x1, x3))
equal_sort[a50](witness_sort[a50], witness_sort[a50]) → true
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 1
POL(and(x1, x2)) = 1 + x1 + x2
POL(cons(x1, x2)) = 2 + x1 + x2
POL(equal_bool(x1, x2)) = x1 + x2
POL(equal_sort[a23](x1, x2)) = 2 + x1 + x2
POL(equal_sort[a24](x1, x2)) = 1 + x1 + x2
POL(equal_sort[a50](x1, x2)) = 1 + x1 + x2
POL(false) = 3
POL(isa_false(x1)) = 4 + x1
POL(isa_true(x1)) = x1
POL(le(x1, x2)) = 3 + x1 + x2
POL(le'(x1, x2)) = 3 + x1 + x2
POL(len(x1)) = 2 + x1
POL(min(x1, x2)) = 1 + x1 + x2
POL(nil) = 0
POL(not(x1)) = 4 + x1
POL(or(x1, x2)) = 1 + x1 + x2
POL(s(x1)) = x1
POL(sum(x1, x2)) = x1 + x2
POL(take(x1, x2)) = 2 + x1 + x2
POL(true) = 0
POL(witness_sort[a50]) = 0
le'(s(x46), 0) → true
le'(0, x105) → false
len(nil) → 0
len(cons(x7, xs')) → s(len(xs'))
min(0, y10) → 0
min(s(x26), 0) → 0
le(s(x46), 0) → false
take(0, cons(y43, ys12)) → y43
take(s(x75), cons(y50, ys15)) → take(x75, ys15)
sum(x85, 0) → x85
le(0, x105) → true
take(0, nil) → 0
take(s(x2), nil) → 0
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a23](0, 0) → true
equal_sort[a24](nil, nil) → true
equal_sort[a24](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a24](x0, x2), equal_sort[a24](x1, x3))
equal_sort[a50](witness_sort[a50], witness_sort[a50]) → true
le'(s(x56), s(y36)) → le'(x56, y36)
min(s(x36), s(y23)) → min(x36, y23)
le(s(x56), s(y36)) → le(x56, y36)
sum(x95, s(y63)) → s(sum(x95, y63))
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
isa_true(true) → true
isa_true(false) → false
equal_sort[a23](0, s(x0)) → false
equal_sort[a23](s(x0), 0) → false
equal_sort[a23](s(x0), s(x1)) → equal_sort[a23](x0, x1)
equal_sort[a24](nil, cons(x0, x1)) → false
equal_sort[a24](cons(x0, x1), nil) → false
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(cons(x1, x2)) = x1 + x2
POL(equal_bool(x1, x2)) = 1 + x1 + x2
POL(equal_sort[a23](x1, x2)) = x1 + x2
POL(equal_sort[a24](x1, x2)) = x1 + x2
POL(false) = 0
POL(isa_true(x1)) = x1
POL(le(x1, x2)) = x1 + x2
POL(le'(x1, x2)) = x1 + x2
POL(min(x1, x2)) = x1 + x2
POL(nil) = 0
POL(s(x1)) = x1
POL(sum(x1, x2)) = x1 + x2
POL(true) = 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
le'(s(x56), s(y36)) → le'(x56, y36)
min(s(x36), s(y23)) → min(x36, y23)
le(s(x56), s(y36)) → le(x56, y36)
sum(x95, s(y63)) → s(sum(x95, y63))
isa_true(true) → true
isa_true(false) → false
equal_sort[a23](0, s(x0)) → false
equal_sort[a23](s(x0), 0) → false
equal_sort[a23](s(x0), s(x1)) → equal_sort[a23](x0, x1)
equal_sort[a24](nil, cons(x0, x1)) → false
equal_sort[a24](cons(x0, x1), nil) → false
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(cons(x1, x2)) = x1 + x2
POL(equal_sort[a23](x1, x2)) = x1 + x2
POL(equal_sort[a24](x1, x2)) = x1 + x2
POL(false) = 0
POL(isa_true(x1)) = 1 + x1
POL(le(x1, x2)) = x1 + x2
POL(le'(x1, x2)) = x1 + x2
POL(min(x1, x2)) = x1 + x2
POL(nil) = 0
POL(s(x1)) = x1
POL(sum(x1, x2)) = x1 + x2
POL(true) = 0
isa_true(true) → true
isa_true(false) → false
le'(s(x56), s(y36)) → le'(x56, y36)
min(s(x36), s(y23)) → min(x36, y23)
le(s(x56), s(y36)) → le(x56, y36)
sum(x95, s(y63)) → s(sum(x95, y63))
equal_sort[a23](0, s(x0)) → false
equal_sort[a23](s(x0), 0) → false
equal_sort[a23](s(x0), s(x1)) → equal_sort[a23](x0, x1)
equal_sort[a24](nil, cons(x0, x1)) → false
equal_sort[a24](cons(x0, x1), nil) → false
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 2
POL(cons(x1, x2)) = x1 + x2
POL(equal_sort[a23](x1, x2)) = x1 + 2·x2
POL(equal_sort[a24](x1, x2)) = 2·x1 + 2·x2
POL(false) = 0
POL(le(x1, x2)) = 2·x1 + x2
POL(le'(x1, x2)) = 2·x1 + x2
POL(min(x1, x2)) = x1 + x2
POL(nil) = 0
POL(s(x1)) = 2 + x1
POL(sum(x1, x2)) = 2·x1 + 2·x2
le'(s(x56), s(y36)) → le'(x56, y36)
min(s(x36), s(y23)) → min(x36, y23)
le(s(x56), s(y36)) → le(x56, y36)
sum(x95, s(y63)) → s(sum(x95, y63))
equal_sort[a23](0, s(x0)) → false
equal_sort[a23](s(x0), 0) → false
equal_sort[a23](s(x0), s(x1)) → equal_sort[a23](x0, x1)
equal_sort[a24](nil, cons(x0, x1)) → false
equal_sort[a24](cons(x0, x1), nil) → false
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(cons(x1, x2)) = x1 + x2
POL(equal_sort[a24](x1, x2)) = 1 + x1 + x2
POL(false) = 0
POL(nil) = 0
equal_sort[a24](nil, cons(x0, x1)) → false
equal_sort[a24](cons(x0, x1), nil) → false