---

Step * 2 of Lemma bag-member-filter-implies2


1. [T] : Type
2. [x] : T
3. [bs] : bag(T)
4. [P] : {x:T| x ↓∈ bs}  ⟶ 𝔹
5. ∀b1:T List. ∀x1:{x:T| x ↓∈ b1}  ⟶ 𝔹. ∀x:T.  (x ↓∈ [x∈b1|x1[x]] ⇒ ((Ax ∈ x ↓∈ b1) ∧ (Ax ∈ ↑x1[x])))
⊢ x ↓∈ bs ∧ (↑P[x]) supposing x ↓∈ [x∈bs|P[x]]
BY
{ (Unhide THENA (Auto THEN TACTIC:InstLemma `bag-filter-wf2` [⌜T⌝;⌜bs⌝;⌜λ2x.P[x]⌝]⋅ THEN Auto)) }

1
1. T : Type
2. x : T
3. bs : bag(T)
4. P : {x:T| x ↓∈ bs}  ⟶ 𝔹
5. ∀b1:T List. ∀x1:{x:T| x ↓∈ b1}  ⟶ 𝔹. ∀x:T.  (x ↓∈ [x∈b1|x1[x]] ⇒ ((Ax ∈ x ↓∈ b1) ∧ (Ax ∈ ↑x1[x])))
⊢ x ↓∈ bs ∧ (↑P[x]) supposing x ↓∈ [x∈bs|P[x]]

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [x]  :  T
3.  [bs]  :  bag(T)
4.  [P]  :  \{x:T|  x  \mdownarrow{}\mmember{}  bs\}    {}\mrightarrow{}  \mBbbB{}
5.  \mforall{}b1:T  List.  \mforall{}x1:\{x:T|  x  \mdownarrow{}\mmember{}  b1\}    {}\mrightarrow{}  \mBbbB{}.  \mforall{}x:T.
          (x  \mdownarrow{}\mmember{}  [x\mmember{}b1|x1[x]]  {}\mRightarrow{}  ((Ax  \mmember{}  x  \mdownarrow{}\mmember{}  b1)  \mwedge{}  (Ax  \mmember{}  \muparrow{}x1[x])))
\mvdash{}  x  \mdownarrow{}\mmember{}  bs  \mwedge{}  (\muparrow{}P[x])  supposing  x  \mdownarrow{}\mmember{}  [x\mmember{}bs|P[x]]


By

---

Latex:
(Unhide  THENA  (Auto  THEN  TACTIC:InstLemma  `bag-filter-wf2`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.P[x]\mkleeneclose{}]\mcdot{}  THEN  Auto))

---

Home Index