---

Step * 1 1 1 2 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. ∃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
BY
{ (SquashExRepD
   THEN (Assert ⌜sv-bag-only([v∈bs|dec2bool(g x (f v))]) = v ∈ T⌝⋅ THENM Auto)
   THEN InstLemma `sv-bag-only-filter` [⌜T⌝;⌜bs⌝;⌜λ2v.dec2bool(g x (f v))⌝;⌜v⌝]⋅
   THEN Auto
   THEN (Try ((RWO "dec2bool_decidable" 0 THEN Auto))
         THEN Try ((RWO "dec2bool_decidable" (-1) THEN Auto THEN All (Unfold `inject`) THEN BackThruSomeHyp THEN Auto))
         )⋅)⋅ }

---

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


By

---

Latex:
(SquashExRepD
  THEN  (Assert  \mkleeneopen{}sv-bag-only([v\mmember{}bs|dec2bool(g  x  (f  v))])  =  v\mkleeneclose{}\mcdot{}  THENM  Auto)
  THEN  InstLemma  `sv-bag-only-filter`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}v.dec2bool(g  x  (f  v))\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (Try  ((RWO  "dec2bool\_decidable"  0  THEN  Auto))
              THEN  Try  ((RWO  "dec2bool\_decidable"  (-1)
                                    THEN  Auto
                                    THEN  All  (Unfold  `inject`)
                                    THEN  BackThruSomeHyp
                                    THEN  Auto))
              )\mcdot{})\mcdot{}

---

Home Index