---

Step * 1 1 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. 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)
11. 0 < #([v∈bs|dec2bool(g x (f v))])
⊢ ∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U))
BY
{ ((InstLemma `bag-filter-wf2` [⌜T⌝;⌜bs⌝;⌜λ2v.dec2bool(g x (f v))⌝]⋅ THEN Auto)
   THEN InstConcl [⌜sv-bag-only([v∈bs|dec2bool(g x (f v))])⌝]⋅
   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. ↓∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U))
9. single-valued-bag([v∈bs|dec2bool(g x (f v))];T)
10. 0 < #([v∈bs|dec2bool(g x (f v))])
11. [x@0∈bs|dec2bool(g x (f x@0))] ∈ bag({x@0:{b:T| b ↓∈ bs} | ↑dec2bool(g x (f x@0))} )
12. x ↓∈ bag-map(f;bs)
13. ↓∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U))
⊢ sv-bag-only([v∈bs|dec2bool(g x (f v))]) ↓∈ bs

2
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. ∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U))
9. single-valued-bag([v∈bs|dec2bool(g x (f v))];T)
10. 0 < #([v∈bs|dec2bool(g x (f v))])
11. [x@0∈bs|dec2bool(g x (f x@0))] ∈ bag({x@0:{b:T| b ↓∈ bs} | ↑dec2bool(g x (f x@0))} )
12. x ↓∈ bag-map(f;bs)
13. ∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U))
14. sv-bag-only([v∈bs|dec2bool(g x (f v))]) ↓∈ bs
⊢ x = (f sv-bag-only([v∈bs|dec2bool(g 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.  g  :  \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)))
10.  single-valued-bag([v\mmember{}bs|dec2bool(g  x  (f  v))];T)
11.  0  <  \#([v\mmember{}bs|dec2bool(g  x  (f  v))])
\mvdash{}  \mexists{}v:T.  (v  \mdownarrow{}\mmember{}  bs  \mwedge{}  (x  =  (f  v)))


By

---

Latex:
((InstLemma  `bag-filter-wf2`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}v.dec2bool(g  x  (f  v))\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  InstConcl  [\mkleeneopen{}sv-bag-only([v\mmember{}bs|dec2bool(g  x  (f  v))])\mkleeneclose{}]\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index