---

Step * 2 of Lemma not-member-mFOL-sequent-freevars


1. v : ℤ
2. u : mFOL()
3. v1 : mFOL() List
4. ∀v1@0:ℤ List. (¬(v ∈ reduce(λh,vs. mFOL-freevars(h) ⋃ vs;v1@0;v1)) ⇐⇒ (¬(v ∈ v1@0)) ∧ (∀h∈v1.¬(v ∈ mFOL-freevars(h))\000C))
⊢ ∀v1@0:ℤ List
    (¬((v ∈ mFOL-freevars(u)) ∨ (v ∈ reduce(λh,vs. mFOL-freevars(h) ⋃ vs;v1@0;v1)))
    ⇐⇒ (¬(v ∈ v1@0)) ∧ (¬(v ∈ mFOL-freevars(u))) ∧ (∀h∈v1.¬(v ∈ mFOL-freevars(h))))
BY
{ (ParallelLast THEN Auto) }

1
1. v : ℤ
2. u : mFOL()
3. v1 : mFOL() List
4. ∀v1@0:ℤ List. (¬(v ∈ reduce(λh,vs. mFOL-freevars(h) ⋃ vs;v1@0;v1)) ⇐⇒ (¬(v ∈ v1@0)) ∧ (∀h∈v1.¬(v ∈ mFOL-freevars(h))\000C))
5. v1@0 : ℤ List
6. (¬(v ∈ reduce(λh,vs. mFOL-freevars(h) ⋃ vs;v1@0;v1))) ⇒ ((¬(v ∈ v1@0)) ∧ (∀h∈v1.¬(v ∈ mFOL-freevars(h))))
7. (¬(v ∈ reduce(λh,vs. mFOL-freevars(h) ⋃ vs;v1@0;v1))) ⇐ (¬(v ∈ v1@0)) ∧ (∀h∈v1.¬(v ∈ mFOL-freevars(h)))
8. ¬(v ∈ v1@0)
9. ¬(v ∈ mFOL-freevars(u))
10. (∀h∈v1.¬(v ∈ mFOL-freevars(h)))
⊢ ¬((v ∈ mFOL-freevars(u)) ∨ (v ∈ reduce(λh,vs. mFOL-freevars(h) ⋃ vs;v1@0;v1)))

---

Latex:

---

Latex:

1.  v  :  \mBbbZ{}
2.  u  :  mFOL()
3.  v1  :  mFOL()  List
4.  \mforall{}v1@0:\mBbbZ{}  List
          (\mneg{}(v  \mmember{}  reduce(\mlambda{}h,vs.  mFOL-freevars(h)  \mcup{}  vs;v1@0;v1))
          \mLeftarrow{}{}\mRightarrow{}  (\mneg{}(v  \mmember{}  v1@0))  \mwedge{}  (\mforall{}h\mmember{}v1.\mneg{}(v  \mmember{}  mFOL-freevars(h))))
\mvdash{}  \mforall{}v1@0:\mBbbZ{}  List
        (\mneg{}((v  \mmember{}  mFOL-freevars(u))  \mvee{}  (v  \mmember{}  reduce(\mlambda{}h,vs.  mFOL-freevars(h)  \mcup{}  vs;v1@0;v1)))
        \mLeftarrow{}{}\mRightarrow{}  (\mneg{}(v  \mmember{}  v1@0))  \mwedge{}  (\mneg{}(v  \mmember{}  mFOL-freevars(u)))  \mwedge{}  (\mforall{}h\mmember{}v1.\mneg{}(v  \mmember{}  mFOL-freevars(h))))


By

---

Latex:
(ParallelLast  THEN  Auto)

---

Home Index