---

Step * 2 1 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))
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)))
BY
{ ((D 0 THENA Auto) THEN D -1 THEN Auto) }

---

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))))
5.  v1@0  :  \mBbbZ{}  List
6.  (\mneg{}(v  \mmember{}  reduce(\mlambda{}h,vs.  mFOL-freevars(h)  \mcup{}  vs;v1@0;v1)))
{}\mRightarrow{}  ((\mneg{}(v  \mmember{}  v1@0))  \mwedge{}  (\mforall{}h\mmember{}v1.\mneg{}(v  \mmember{}  mFOL-freevars(h))))
7.  (\mneg{}(v  \mmember{}  reduce(\mlambda{}h,vs.  mFOL-freevars(h)  \mcup{}  vs;v1@0;v1)))  \mLeftarrow{}{}  (\mneg{}(v  \mmember{}  v1@0))
\mwedge{}  (\mforall{}h\mmember{}v1.\mneg{}(v  \mmember{}  mFOL-freevars(h)))
8.  \mneg{}(v  \mmember{}  v1@0)
9.  \mneg{}(v  \mmember{}  mFOL-freevars(u))
10.  (\mforall{}h\mmember{}v1.\mneg{}(v  \mmember{}  mFOL-freevars(h)))
\mvdash{}  \mneg{}((v  \mmember{}  mFOL-freevars(u))  \mvee{}  (v  \mmember{}  reduce(\mlambda{}h,vs.  mFOL-freevars(h)  \mcup{}  vs;v1@0;v1)))


By

---

Latex:
((D  0  THENA  Auto)  THEN  D  -1  THEN  Auto)

---

Home Index