(vl-genblob-gencaselist-count x) → count
Theorem:
(defthm vl-genblob-gencaselist-count-greater-than-first (b* ((common-lisp::?count (vl-genblob-gencaselist-count x))) (implies (consp (vl-gencaselist-fix x)) (< (vl-genblob-genblock-count (cdar (vl-gencaselist-fix x))) count))) :rule-classes :linear)
Theorem:
(defthm vl-genblob-gencaselist-count-gte-rest (b* ((common-lisp::?count (vl-genblob-gencaselist-count x))) (<= (vl-genblob-gencaselist-count (cdr (vl-gencaselist-fix x))) count)) :rule-classes :linear)
Theorem:
(defthm vl-genblob-gencaselist-count-greater-than-rest (b* ((common-lisp::?count (vl-genblob-gencaselist-count x))) (implies (consp (vl-gencaselist-fix x)) (< (vl-genblob-gencaselist-count (cdr (vl-gencaselist-fix x))) count))) :rule-classes :linear)