---

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

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

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

---

Latex:

---

Latex:
.....assertion..... 
1.  [T]  :  Type
2.  [x]  :  T
3.  [bs]  :  bag(T)
4.  [P]  :  \{x:T|  x  \mdownarrow{}\mmember{}  bs\}    {}\mrightarrow{}  \mBbbB{}
\mvdash{}  \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])))


By

---

Latex:
TACTIC:(RepeatFor  3  (Thin  (-1))
                THEN  RepeatFor  4  ((D  0
                                                      THENA  (Auto
                                                                    THEN  (TACTIC:InstLemma  `bag-filter-wf2`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.x1[x]\mkleeneclose{}]\mcdot{}
                                                                                THEN  Auto
                                                                                )\mcdot{}
                                                                    )
                                                      ))
                )

---

Home Index