---

Step * 1 of Lemma bag-member-map3-deq


1. [T] : Type
2. [U] : Type
3. x : U
4. bs : bag(T)
5. f : {v:T| v ↓∈ bs}  ⟶ U
6. Inj({v:T| v ↓∈ bs} ;U;f)
7. ∀x,y:U.  Dec(x = y ∈ U)
8. uiff(x ↓∈ bag-map(f;bs);↓∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U)))
9. ↓∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U))
⊢ ∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U))
BY
{ (TACTIC:RenameVar `g' (-3)
   THEN (Assert single-valued-bag([v∈bs|dec2bool(g x (f v))];T) BY
               (BLemma `single-valued-bag-filter`
                THEN Auto
                THEN ∀h:hyp. (RWO "dec2bool_decidable" h⋅ THENA Auto) 
                THEN All (Unfold `inject`)
                THEN BackThruSomeHyp
                THEN Auto))
   ) }

1
1. [T] : Type
2. [U] : Type
3. x : U
4. bs : bag(T)
5. f : {v:T| v ↓∈ bs}  ⟶ U
6. Inj({v:T| v ↓∈ bs} ;U;f)
7. g : ∀x,y:U.  Dec(x = y ∈ U)
8. uiff(x ↓∈ bag-map(f;bs);↓∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U)))
9. ↓∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U))
10. single-valued-bag([v∈bs|dec2bool(g x (f v))];T)
⊢ ∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [U]  :  Type
3.  x  :  U
4.  bs  :  bag(T)
5.  f  :  \{v:T|  v  \mdownarrow{}\mmember{}  bs\}    {}\mrightarrow{}  U
6.  Inj(\{v:T|  v  \mdownarrow{}\mmember{}  bs\}  ;U;f)
7.  \mforall{}x,y:U.    Dec(x  =  y)
8.  uiff(x  \mdownarrow{}\mmember{}  bag-map(f;bs);\mdownarrow{}\mexists{}v:T.  (v  \mdownarrow{}\mmember{}  bs  \mwedge{}  (x  =  (f  v))))
9.  \mdownarrow{}\mexists{}v:T.  (v  \mdownarrow{}\mmember{}  bs  \mwedge{}  (x  =  (f  v)))
\mvdash{}  \mexists{}v:T.  (v  \mdownarrow{}\mmember{}  bs  \mwedge{}  (x  =  (f  v)))


By

---

Latex:
(TACTIC:RenameVar  `g'  (-3)
  THEN  (Assert  single-valued-bag([v\mmember{}bs|dec2bool(g  x  (f  v))];T)  BY
                          (BLemma  `single-valued-bag-filter`
                            THEN  Auto
                            THEN  \mforall{}h:hyp.  (RWO  "dec2bool\_decidable"  h\mcdot{}  THENA  Auto) 
                            THEN  All  (Unfold  `inject`)
                            THEN  BackThruSomeHyp
                            THEN  Auto))
  )

---

Home Index