---

Step * 1 of Lemma bag-null-bag-union


1. T : Type
2. u : bag(T)
3. v : bag(T) List
4. (∀bs:bag(T). (bs ↓∈ v ⇒ (↑bag-null(bs)))) ⇒ (↑bag-null(bag-union(v)))
5. ∀bs:bag(T). (bs ↓∈ u.v ⇒ (↑bag-null(bs)))
6. u = {} ∈ bag(T)
⊢ ↑bag-null(bag-union(v))
BY
{ (((BHyp (-3) THENA Auto) THEN (UnivCD THENA Auto))
   THEN BHyp (-4)
   THEN Auto
   THEN BagMemberD 0
   THEN D 0
   THEN Auto
   THEN OrRight
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  bag(T)
3.  v  :  bag(T)  List
4.  (\mforall{}bs:bag(T).  (bs  \mdownarrow{}\mmember{}  v  {}\mRightarrow{}  (\muparrow{}bag-null(bs))))  {}\mRightarrow{}  (\muparrow{}bag-null(bag-union(v)))
5.  \mforall{}bs:bag(T).  (bs  \mdownarrow{}\mmember{}  u.v  {}\mRightarrow{}  (\muparrow{}bag-null(bs)))
6.  u  =  \{\}
\mvdash{}  \muparrow{}bag-null(bag-union(v))


By

---

Latex:
(((BHyp  (-3)  THENA  Auto)  THEN  (UnivCD  THENA  Auto))
  THEN  BHyp  (-4)
  THEN  Auto
  THEN  BagMemberD  0
  THEN  D  0
  THEN  Auto
  THEN  OrRight
  THEN  Auto)\mcdot{}

---

Home Index