---

Step * 1 2 of Lemma empty-bag-union


1. T : Type
2. bs : bag(bag(T))
3. bag-union(bs) = {} ∈ bag(T)
4. ∀bs:Top List List. ((concat(bs) = [] ∈ (Top List)) ⇒ (bs ~ bag-rep(||bs||;[])))
⊢ bs ~ bag-rep(#(bs);{})
BY
{ (Unfolds ``bag-size empty-bag`` 0 THEN With ⌜bs⌝ (D (-1))⋅) }

1
.....wf..... 
1. T : Type
2. bs : bag(bag(T))
3. bag-union(bs) = {} ∈ bag(T)
⊢ bs ∈ Top List List

2
1. T : Type
2. bs : bag(bag(T))
3. bag-union(bs) = {} ∈ bag(T)
4. (concat(bs) = [] ∈ (Top List)) ⇒ (bs ~ bag-rep(||bs||;[]))
⊢ bs ~ bag-rep(||bs||;[])

---

Latex:

---

Latex:

1.  T  :  Type
2.  bs  :  bag(bag(T))
3.  bag-union(bs)  =  \{\}
4.  \mforall{}bs:Top  List  List.  ((concat(bs)  =  [])  {}\mRightarrow{}  (bs  \msim{}  bag-rep(||bs||;[])))
\mvdash{}  bs  \msim{}  bag-rep(\#(bs);\{\})


By

---

Latex:
(Unfolds  ``bag-size  empty-bag``  0  THEN  With  \mkleeneopen{}bs\mkleeneclose{}  (D  (-1))\mcdot{})

---

Home Index