---

Step * of Lemma bag-size-one

∀[T:Type]. ∀[bs:bag(T)].  bs ~ {only(bs)} supposing #(bs) = 1 ∈ ℤ
BY
{ (Auto
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜bs = L ∈ (Top List)⌝⋅ THENA Auto)
   THEN D -2
   THEN RepUR ``bag-size bag-only single-bag`` 0
   THEN Try (Complete (Auto))
   THEN D -2
   THEN Reduce 0
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[bs:bag(T)].    bs  \msim{}  \{only(bs)\}  supposing  \#(bs)  =  1


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}bs  =  L\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  RepUR  ``bag-size  bag-only  single-bag``  0
  THEN  Try  (Complete  (Auto))
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto')

---

Home Index