---

Step * 2 of Lemma bag-member-map


1. T : Type
2. U : Type
3. x : U
4. f : T ⟶ U
5. bs : bag(T)
6. ↓∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U))
⊢ x ↓∈ bag-map(f;bs)
BY
{ (Auto
   THEN D (-1)
   THEN (Unhide THENA Auto)
   THEN ExRepD
   THEN Unfold `bag-member` 0
   THEN Unfold `bag-member` (-2)
   THEN SquashExRepD
   THEN D 0
   THEN (InstConcl [⌜map(f;L)⌝]⋅ THENA Auto)
   THEN D 0⋅
   THEN Try (Complete ((Try (Fold `bag-map` 0⋅) THEN HypSubst' (-3) 0 THEN Auto)))
   THEN (BLemma `member_map` THENA Auto)
   THEN InstConcl [⌜v⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  U  :  Type
3.  x  :  U
4.  f  :  T  {}\mrightarrow{}  U
5.  bs  :  bag(T)
6.  \mdownarrow{}\mexists{}v:T.  (v  \mdownarrow{}\mmember{}  bs  \mwedge{}  (x  =  (f  v)))
\mvdash{}  x  \mdownarrow{}\mmember{}  bag-map(f;bs)


By

---

Latex:
(Auto
  THEN  D  (-1)
  THEN  (Unhide  THENA  Auto)
  THEN  ExRepD
  THEN  Unfold  `bag-member`  0
  THEN  Unfold  `bag-member`  (-2)
  THEN  SquashExRepD
  THEN  D  0
  THEN  (InstConcl  [\mkleeneopen{}map(f;L)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  0\mcdot{}
  THEN  Try  (Complete  ((Try  (Fold  `bag-map`  0\mcdot{})  THEN  HypSubst'  (-3)  0  THEN  Auto)))
  THEN  (BLemma  `member\_map`  THENA  Auto)
  THEN  InstConcl  [\mkleeneopen{}v\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index