---

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

∀s:mFOL-sequent(). ∀v:ℤ.
  (¬(v ∈ mFOL-sequent-freevars(s)) ⇐⇒ (¬(v ∈ mFOL-freevars(snd(s)))) ∧ (∀h∈fst(s).¬(v ∈ mFOL-freevars(h))))
BY
{ ((UnivCD THENA Auto)
   THEN D 1
   THEN RepUR ``mFOL-sequent-freevars`` 0
   THEN (GenConclTerm ⌜mFOL-freevars(s2)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN MoveToConcl (-1)
   THEN Thin (-2)
   THEN ListInd 1
   THEN Reduce 0
   THEN (RWO "l_all_nil_iff l_all_cons" 0 THENA Auto)
   THEN (RWW "member-union" 0 THENA Auto)) }

1
1. v : ℤ
⊢ ∀v1:ℤ List. (¬(v ∈ v1) ⇐⇒ (¬(v ∈ v1)) ∧ True)

2
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))))

---

Latex:

---

Latex:
\mforall{}s:mFOL-sequent().  \mforall{}v:\mBbbZ{}.
    (\mneg{}(v  \mmember{}  mFOL-sequent-freevars(s))
    \mLeftarrow{}{}\mRightarrow{}  (\mneg{}(v  \mmember{}  mFOL-freevars(snd(s))))  \mwedge{}  (\mforall{}h\mmember{}fst(s).\mneg{}(v  \mmember{}  mFOL-freevars(h))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  D  1
  THEN  RepUR  ``mFOL-sequent-freevars``  0
  THEN  (GenConclTerm  \mkleeneopen{}mFOL-freevars(s2)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  MoveToConcl  (-1)
  THEN  Thin  (-2)
  THEN  ListInd  1
  THEN  Reduce  0
  THEN  (RWO  "l\_all\_nil\_iff  l\_all\_cons"  0  THENA  Auto)
  THEN  (RWW  "member-union"  0  THENA  Auto))

---

Home Index