Step
*
1
of Lemma
empty-bag-union
1. T : Type
2. bs : bag(bag(T))
3. bag-union(bs) = {} ∈ bag(T)
⊢ bs ~ bag-rep(#(bs);{})
BY
{ Assert ⌜∀bs:Top List List. ((concat(bs) = [] ∈ (Top List))
⇒ (bs ~ bag-rep(||bs||;[])))⌝⋅ }
1
.....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||;[])))
2
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);{})
Latex:
Latex:
1. T : Type
2. bs : bag(bag(T))
3. bag-union(bs) = \{\}
\mvdash{} bs \msim{} bag-rep(\#(bs);\{\})
By
Latex:
Assert \mkleeneopen{}\mforall{}bs:Top List List. ((concat(bs) = []) {}\mRightarrow{} (bs \msim{} bag-rep(||bs||;[])))\mkleeneclose{}\mcdot{}
Home
Index