---

Step * of Lemma bag-from-member-function

∀[T:Type]
  ∀bs:bag(T). ∀P,Q:T ⟶ ℙ.
    ((∀i:T. Dec(Q[i]))
    ⇒ (∀i:T. (i ↓∈ bs ⇒ Q[i] ⇒ P[i]))
    ⇒ (∃b:bag(T). ((∀i:T. (i ↓∈ bs ⇒ Q[i] ⇒ i ↓∈ b)) ∧ (∀i:T. (i ↓∈ b ⇒ P[i])))))
BY
{ (Auto
   THEN RenameVar `g' (-2)
   THEN InstConcl [⌜[i∈bs|dec2bool(g i)]⌝]⋅
   THEN Auto
   THEN Try ((BagMemberD (-1) THEN RepD THEN RWO "dec2bool_decidable" (-1) THEN Auto))
   THEN Try ((BagMemberD 0 THEN Auto THEN RWO "dec2bool_decidable" 0 THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}bs:bag(T).  \mforall{}P,Q:T  {}\mrightarrow{}  \mBbbP{}.
        ((\mforall{}i:T.  Dec(Q[i]))
        {}\mRightarrow{}  (\mforall{}i:T.  (i  \mdownarrow{}\mmember{}  bs  {}\mRightarrow{}  Q[i]  {}\mRightarrow{}  P[i]))
        {}\mRightarrow{}  (\mexists{}b:bag(T).  ((\mforall{}i:T.  (i  \mdownarrow{}\mmember{}  bs  {}\mRightarrow{}  Q[i]  {}\mRightarrow{}  i  \mdownarrow{}\mmember{}  b))  \mwedge{}  (\mforall{}i:T.  (i  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  P[i])))))


By

---

Latex:
(Auto
  THEN  RenameVar  `g'  (-2)
  THEN  InstConcl  [\mkleeneopen{}[i\mmember{}bs|dec2bool(g  i)]\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((BagMemberD  (-1)  THEN  RepD  THEN  RWO  "dec2bool\_decidable"  (-1)  THEN  Auto))
  THEN  Try  ((BagMemberD  0  THEN  Auto  THEN  RWO  "dec2bool\_decidable"  0  THEN  Auto)))

---

Home Index