---

Step * of Lemma 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
{ Auto }

1
1. s : mFOL-sequent()@i
2. v : ℤ@i
3. (v ∈ mFOL-sequent-freevars(s))@i
⊢ (v ∈ mFOL-freevars(snd(s))) ∨ (∃h∈fst(s). (v ∈ mFOL-freevars(h)))

2
1. s : mFOL-sequent()@i
2. v : ℤ@i
3. (v ∈ mFOL-freevars(snd(s))) ∨ (∃h∈fst(s). (v ∈ mFOL-freevars(h)))@i
⊢ (v ∈ mFOL-sequent-freevars(s))

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index