---

Step * 1 of Lemma bag-member-combine


1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. b : B
5. n : ℕ
6. ∀n:ℕn. ∀bs:bag(A).  ((#(bs) ≤ n) ⇒ uiff(b ↓∈ ⋃x∈bs.f[x];↓∃x:A. (x ↓∈ bs ∧ b ↓∈ f[x])))
7. bs : bag(A)
8. bs = {} ∈ bag(A)
⊢ (#(bs) ≤ n) ⇒ uiff(b ↓∈ ⋃x∈bs.f[x];↓∃x:A. (x ↓∈ bs ∧ b ↓∈ f[x]))
BY
{ ((HypSubst' (-1) 0 THENA Auto)
   THEN RepUR ``bag-combine empty-bag bag-map bag-union bag-size`` 0
   THEN Fold `empty-bag` 0⋅
   THEN RWO "bag-member-empty-iff" 0
   THEN Auto
   THEN ExRepD
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  bag(B)
4.  b  :  B
5.  n  :  \mBbbN{}
6.  \mforall{}n:\mBbbN{}n.  \mforall{}bs:bag(A).    ((\#(bs)  \mleq{}  n)  {}\mRightarrow{}  uiff(b  \mdownarrow{}\mmember{}  \mcup{}x\mmember{}bs.f[x];\mdownarrow{}\mexists{}x:A.  (x  \mdownarrow{}\mmember{}  bs  \mwedge{}  b  \mdownarrow{}\mmember{}  f[x])))
7.  bs  :  bag(A)
8.  bs  =  \{\}
\mvdash{}  (\#(bs)  \mleq{}  n)  {}\mRightarrow{}  uiff(b  \mdownarrow{}\mmember{}  \mcup{}x\mmember{}bs.f[x];\mdownarrow{}\mexists{}x:A.  (x  \mdownarrow{}\mmember{}  bs  \mwedge{}  b  \mdownarrow{}\mmember{}  f[x]))


By

---

Latex:
((HypSubst'  (-1)  0  THENA  Auto)
  THEN  RepUR  ``bag-combine  empty-bag  bag-map  bag-union  bag-size``  0
  THEN  Fold  `empty-bag`  0\mcdot{}
  THEN  RWO  "bag-member-empty-iff"  0
  THEN  Auto
  THEN  ExRepD
  THEN  Auto)\mcdot{}

---

Home Index