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 RisEmptyProof (⇔)
↳56 TRUE
↳57 RisEmptyProof (⇔)
↳58 TRUE
↳59 RisEmptyProof (⇔)
↳60 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
le'2 > true
le'2 > false
len1 > s1
len1 > 0
le2 > true
le2 > false
take2 > 0
sum2 > s1
equalbool2 > true
not1 > true
not1 > false
isafalse1 > true
isafalse1 > false
equalsort[a23]2 > true
equalsort[a23]2 > false
equalsort[a24]2 > true
equalsort[a24]2 > false
equalsort[a24]2 > and2
equalsort[a50]2 > true
trivial
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