---

Step * of Lemma bag-member-filter-implies1

∀[T:Type]. ∀[x:T]. ∀[bs:bag(T)]. ∀[P:{x:T| x ↓∈ bs}  ⟶ 𝔹].  x ↓∈ [x∈bs|P[x]] supposing x ↓∈ bs ∧ (↑P[x])
BY
{ ((UnivCD THENA (Auto THEN InstLemma `bag-filter-wf2` [⌜T⌝;⌜bs⌝;⌜λ2x.P[x]⌝]⋅ THEN Auto))
   THEN InstLemma `bag-member-filter` [⌜{x:T| x ↓∈ bs} ⌝;⌜P⌝;⌜x⌝;⌜bs⌝]⋅
   THEN Auto
   THEN Try (Complete ((BLemma `bag-subtype` THEN Auto)))
   THEN D (-1)
   THEN Try (Complete ((RWO "bag-subtype2<" (-1)
                        THEN Auto
                        THEN InstLemma `bag-filter-wf2` [⌜T⌝;⌜bs⌝;⌜λ2x.P[x]⌝]⋅
                        THEN Auto)))
   THEN Try (Complete ((Auto THEN RWO "bag-subtype2<" 0 THEN Auto THEN BLemma `bag-subtype` THEN Auto)))) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[bs:bag(T)].  \mforall{}[P:\{x:T|  x  \mdownarrow{}\mmember{}  bs\}    {}\mrightarrow{}  \mBbbB{}].
    x  \mdownarrow{}\mmember{}  [x\mmember{}bs|P[x]]  supposing  x  \mdownarrow{}\mmember{}  bs  \mwedge{}  (\muparrow{}P[x])


By

---

Latex:
((UnivCD  THENA  (Auto  THEN  InstLemma  `bag-filter-wf2`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.P[x]\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  InstLemma  `bag-member-filter`  [\mkleeneopen{}\{x:T|  x  \mdownarrow{}\mmember{}  bs\}  \mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  ((BLemma  `bag-subtype`  THEN  Auto)))
  THEN  D  (-1)
  THEN  Try  (Complete  ((RWO  "bag-subtype2<"  (-1)
                                            THEN  Auto
                                            THEN  InstLemma  `bag-filter-wf2`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.P[x]\mkleeneclose{}]\mcdot{}
                                            THEN  Auto)))
  THEN  Try  (...))

---

Home Index