---

Step * of Lemma bag-size-bag-member

∀[T:Type]. ∀[bs:bag(T)].  (0 < #(bs) ⇐⇒ ↓∃b:T. b ↓∈ bs)
BY
{ (Auto
   THEN (BagToList (-2) THENA Auto)
   THEN Try ((Unfold `bag-size` (-1)
              THEN Unfold `bag-member` 0⋅
              THEN (Assert ⌜∃b:T. (b ∈ bs)⌝⋅
                    THENA ((InstConcl [⌜bs[0]⌝]⋅ THENA Auto) THEN BLemma `select_member` THEN Auto)
                    )
              THEN D (-1)
              THEN D 0
              THEN (InstConcl [⌜b⌝]⋅ THENA Auto)
              THEN D 0
              THEN InstConcl [⌜bs⌝]⋅
              THEN Auto))) }

1
1. T : Type
2. bs : T List
3. ∃b:T. b ↓∈ bs
⊢ 0 < #(bs)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[bs:bag(T)].    (0  <  \#(bs)  \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}\mexists{}b:T.  b  \mdownarrow{}\mmember{}  bs)


By

---

Latex:
(Auto
  THEN  (BagToList  (-2)  THENA  Auto)
  THEN  Try  ((Unfold  `bag-size`  (-1)
                        THEN  Unfold  `bag-member`  0\mcdot{}
                        THEN  (Assert  \mkleeneopen{}\mexists{}b:T.  (b  \mmember{}  bs)\mkleeneclose{}\mcdot{}
                                    THENA  ((InstConcl  [\mkleeneopen{}bs[0]\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  BLemma  `select\_member`  THEN  Auto)
                                    )
                        THEN  D  (-1)
                        THEN  D  0
                        THEN  (InstConcl  [\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
                        THEN  D  0
                        THEN  InstConcl  [\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}
                        THEN  Auto)))

---

Home Index