---

Step * 1 1 of Lemma empty-bag-union

.....assertion..... 
1. T : Type
2. bs : bag(bag(T))
3. bag-union(bs) = {} ∈ bag(T)
⊢ ∀bs:Top List List. ((concat(bs) = [] ∈ (Top List)) ⇒ (bs ~ bag-rep(||bs||;[])))
BY
{ (All Thin THEN (Assert [] ∈ Top List BY Auto) THEN RepUR ``bag-rep concat empty-bag cons-bag`` 0) }

1
1. [] ∈ Top List
⊢ ∀bs:Top List List. ((reduce(λl,l'. (l @ l');[];bs) = [] ∈ (Top List)) ⇒ (bs ~ primrec(||bs||;[];λi,r. [[] / r])))

---

Latex:

---

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


By

---

Latex:
(All  Thin  THEN  (Assert  []  \mmember{}  Top  List  BY  Auto)  THEN  RepUR  ``bag-rep  concat  empty-bag  cons-bag``  0)

---

Home Index