---

Step * 3 1 1 1 1 of Lemma mFOL-bound-rename

.....assertion..... 
1. isall : 𝔹@i'
2. z : ℤ@i'
3. body : mFOL()@i'
4. ∀L:ℤ List
     (∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(body) ∈ AbstractFOFormula)
                      ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))})@i'
5. L : ℤ List@i'
6. (z ∈ L)
7. fmla' : mFOL()
8. mFOL-abstract(fmla') = mFOL-abstract(body) ∈ AbstractFOFormula
9. l_disjoint(ℤ;L;mFOL-boundvars(fmla'))
⊢ ∃z':ℤ. (¬(z' ∈ L @ mFOL-boundvars(fmla') @ mFOL-freevars(fmla')))
BY
{ (GenConclAtAddr [2;1;2] THEN All Thin) }

1
1. v : ℤ List@i
⊢ ∃z':ℤ. (¬(z' ∈ v))

---

Latex:


.....assertion..... 
1.  isall  :  \mBbbB{}@i'
2.  z  :  \mBbbZ{}@i'
3.  body  :  mFOL()@i'
4.  \mforall{}L:\mBbbZ{}  List
          (\mexists{}fmla':\{mFOL()|  ((mFOL-abstract(fmla')  =  mFOL-abstract(body))
                                            \mwedge{}  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla')))\})@i'
5.  L  :  \mBbbZ{}  List@i'
6.  (z  \mmember{}  L)
7.  fmla'  :  mFOL()
8.  mFOL-abstract(fmla')  =  mFOL-abstract(body)
9.  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla'))
\mvdash{}  \mexists{}z':\mBbbZ{}.  (\mneg{}(z'  \mmember{}  L  @  mFOL-boundvars(fmla')  @  mFOL-freevars(fmla')))


By

(GenConclAtAddr  [2;1;2]  THEN  All  Thin)

---

Home Index