---

Step * 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)
⊢ ∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U))
BY
{ TACTIC:(Assert 0 < #([v∈bs|dec2bool(g x (f v))]) BY
                (TrySquashExRepD (-2)
                 THEN Using [`x',⌜v⌝] (BLemma `bag-member-size`)⋅
                 THEN Try (((InstLemma `bag-filter-wf2` [⌜T⌝;⌜bs⌝;⌜λ2v.dec2bool(g x (f v))⌝]⋅ THENA Auto)
                            THEN DoSubsume
                            THEN Complete (Auto)))
                 THEN BLemma `bag-member-filter2`
                 THEN Auto
                 THEN TACTIC:RWO "dec2bool_decidable" 0
                 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)
11. 0 < #([v∈bs|dec2bool(g x (f v))])
⊢ ∃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.  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)
\mvdash{}  \mexists{}v:T.  (v  \mdownarrow{}\mmember{}  bs  \mwedge{}  (x  =  (f  v)))


By

---

Latex:
TACTIC:(Assert  0  <  \#([v\mmember{}bs|dec2bool(g  x  (f  v))])  BY
                            (TrySquashExRepD  (-2)
                              THEN  Using  [`x',\mkleeneopen{}v\mkleeneclose{}]  (BLemma  `bag-member-size`)\mcdot{}
                              THEN  Try  (((InstLemma  `bag-filter-wf2`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}v.dec2bool(g  x  (f  v))\mkleeneclose{}]\mcdot{}
                                                      THENA  Auto
                                                      )
                                                    THEN  DoSubsume
                                                    THEN  Complete  (Auto)))
                              THEN  BLemma  `bag-member-filter2`
                              THEN  Auto
                              THEN  TACTIC:RWO  "dec2bool\_decidable"  0
                              THEN  Auto))

---

Home Index