---

Step * 3 2 of Lemma mFOL-bound-rename


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)
⊢ ∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(mFOquant(isall;z;body)) ∈ AbstractFOFormula)
                  ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))}
BY
{ ((InstHyp [⌈L⌉] (-3)⋅ THENA Auto) THEN ExRepD THEN With ⌈mFOquant(isall;z;fmla')⌉ (D 0)⋅ THEN Auto)⋅ }

1
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'))
⊢ mFOL-abstract(mFOquant(isall;z;fmla')) = mFOL-abstract(mFOquant(isall;z;body)) ∈ AbstractFOFormula

2
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'))
10. mFOL-abstract(mFOquant(isall;z;fmla')) = mFOL-abstract(mFOquant(isall;z;body)) ∈ AbstractFOFormula
⊢ l_disjoint(ℤ;L;mFOL-boundvars(mFOquant(isall;z;fmla')))

---

Latex:



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.  \mneg{}(z  \mmember{}  L)
\mvdash{}  \mexists{}fmla':\{mFOL()|  ((mFOL-abstract(fmla')  =  mFOL-abstract(mFOquant(isall;z;body)))
                                    \mwedge{}  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla')))\}


By

((InstHyp  [\mkleeneopen{}L\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)  THEN  ExRepD  THEN  With  \mkleeneopen{}mFOquant(isall;z;fmla')\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index