Step
*
1
of Lemma
bag-member-union
1. T : Type
2. x : T
3. bbs : bag(T) List
⊢ uiff(x ↓∈ bag-union(bbs);↓∃b:bag(T). (x ↓∈ b ∧ b ↓∈ bbs))
BY
{ (ListInd (-1) THEN Reduce 0) }
1
1. T : Type
2. x : T
⊢ uiff(x ↓∈ bag-union([]);↓∃b:bag(T). (x ↓∈ b ∧ b ↓∈ []))
2
1. T : Type
2. x : T
3. u : bag(T)
4. v : bag(T) List
5. uiff(x ↓∈ bag-union(v);↓∃b:bag(T). (x ↓∈ b ∧ b ↓∈ v))
⊢ uiff(x ↓∈ bag-union([u / v]);↓∃b:bag(T). (x ↓∈ b ∧ b ↓∈ [u / v]))
Latex:
Latex:
1. T : Type
2. x : T
3. bbs : bag(T) List
\mvdash{} uiff(x \mdownarrow{}\mmember{} bag-union(bbs);\mdownarrow{}\mexists{}b:bag(T). (x \mdownarrow{}\mmember{} b \mwedge{} b \mdownarrow{}\mmember{} bbs))
By
Latex:
(ListInd (-1) THEN Reduce 0)
Home
Index