---

Step * of Lemma bag-member-not-bag-null

∀[T:Type]. ∀[bs:bag(T)].  uiff(↓∃x:T. x ↓∈ bs;¬↑bag-null(bs))
BY
{ ((UnivCD THENA Auto)
   THEN D 0
   THEN Auto
   THEN (Unhide THENA Auto)
   THEN Try (Complete (((D 0 THENA Auto)
                        THEN SquashExRepD
                        THEN (RWO "assert-bag-null" (-1) THENA Auto)
                        THEN (RWO "-1" (-2) THENA Auto)
                        THEN BagMemberD (-2))))
   THEN (BagToList (-2) THENA Auto)
   THEN Unfold `bag-null` (-1)
   THEN (RWO "assert_of_null" (-1) THENA Auto)
   THEN (FLemma `member_exists` [-1] THENA Auto)
   THEN D (-1)
   THEN D 0
   THEN (InstConcl [⌜x⌝]⋅ THENA Auto)
   THEN Unfold `bag-member` 0
   THEN D 0
   THEN InstConcl [⌜bs⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[bs:bag(T)].    uiff(\mdownarrow{}\mexists{}x:T.  x  \mdownarrow{}\mmember{}  bs;\mneg{}\muparrow{}bag-null(bs))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  D  0
  THEN  Auto
  THEN  (Unhide  THENA  Auto)
  THEN  Try  (Complete  (((D  0  THENA  Auto)
                                            THEN  SquashExRepD
                                            THEN  (RWO  "assert-bag-null"  (-1)  THENA  Auto)
                                            THEN  (RWO  "-1"  (-2)  THENA  Auto)
                                            THEN  BagMemberD  (-2))))
  THEN  (BagToList  (-2)  THENA  Auto)
  THEN  Unfold  `bag-null`  (-1)
  THEN  (RWO  "assert\_of\_null"  (-1)  THENA  Auto)
  THEN  (FLemma  `member\_exists`  [-1]  THENA  Auto)
  THEN  D  (-1)
  THEN  D  0
  THEN  (InstConcl  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `bag-member`  0
  THEN  D  0
  THEN  InstConcl  [\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index