---

Step * of Lemma bag-size-zero

∀[C:Type]. ∀[bs:bag(C)].  bs ~ {} supposing #(bs) ≤ 0
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (GenConcl ⌜bs = L ∈ (Top List)⌝⋅ THENA Auto)
   THEN Unfold `bag-size` 0
   THEN D (-2)
   THEN RepUR ``empty-bag`` 0
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[C:Type].  \mforall{}[bs:bag(C)].    bs  \msim{}  \{\}  supposing  \#(bs)  \mleq{}  0


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (GenConcl  \mkleeneopen{}bs  =  L\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Unfold  `bag-size`  0
  THEN  D  (-2)
  THEN  RepUR  ``empty-bag``  0
  THEN  Auto')

---

Home Index