---

Step * 3 2 of Lemma FOL-bound-rename


1. isall : 𝔹
2. z : ℤ
3. body : mFOL()
4. ∀L:ℤ List
     (∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(body) ∈ (ℤ List))
                    ∧ (FOL-abstract(fmla') = FOL-abstract(body) ∈ AbstractFOFormula+(mFOL-freevars(body)))
                    ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))])
5. L : ℤ List
6. ¬(z ∈ L)
⊢ ∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(mFOquant(isall;z;body)) ∈ (ℤ List))
                ∧ (FOL-abstract(fmla')
                  = FOL-abstract(mFOquant(isall;z;body))
                  ∈ AbstractFOFormula+(mFOL-freevars(mFOquant(isall;z;body))))
                ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))]
BY
{ ((InstHyp [⌜L⌝] (-3)⋅ THENA Auto) THEN D -1 THEN With ⌜mFOquant(isall;z;fmla')⌝ (D 0)⋅ THEN Auto)⋅ }

1
1. isall : 𝔹
2. z : ℤ
3. body : mFOL()
4. ∀L:ℤ List
     (∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(body) ∈ (ℤ List))
                    ∧ (FOL-abstract(fmla') = FOL-abstract(body) ∈ AbstractFOFormula+(mFOL-freevars(body)))
                    ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))])
5. L : ℤ List
6. ¬(z ∈ L)
7. fmla' : mFOL()
8. mFOL-freevars(fmla') = mFOL-freevars(body) ∈ (ℤ List)
9. FOL-abstract(fmla') = FOL-abstract(body) ∈ AbstractFOFormula+(mFOL-freevars(body))
10. l_disjoint(ℤ;L;mFOL-boundvars(fmla'))
⊢ mFOL-freevars(mFOquant(isall;z;fmla')) = mFOL-freevars(mFOquant(isall;z;body)) ∈ (ℤ List)

2
1. isall : 𝔹
2. z : ℤ
3. body : mFOL()
4. ∀L:ℤ List
     (∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(body) ∈ (ℤ List))
                    ∧ (FOL-abstract(fmla') = FOL-abstract(body) ∈ AbstractFOFormula+(mFOL-freevars(body)))
                    ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))])
5. L : ℤ List
6. ¬(z ∈ L)
7. fmla' : mFOL()
8. mFOL-freevars(fmla') = mFOL-freevars(body) ∈ (ℤ List)
9. FOL-abstract(fmla') = FOL-abstract(body) ∈ AbstractFOFormula+(mFOL-freevars(body))
10. l_disjoint(ℤ;L;mFOL-boundvars(fmla'))
11. mFOL-freevars(mFOquant(isall;z;fmla')) = mFOL-freevars(mFOquant(isall;z;body)) ∈ (ℤ List)
⊢ FOL-abstract(mFOquant(isall;z;fmla'))
= FOL-abstract(mFOquant(isall;z;body))
∈ AbstractFOFormula+(mFOL-freevars(mFOquant(isall;z;body)))

3
1. isall : 𝔹
2. z : ℤ
3. body : mFOL()
4. ∀L:ℤ List
     (∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(body) ∈ (ℤ List))
                    ∧ (FOL-abstract(fmla') = FOL-abstract(body) ∈ AbstractFOFormula+(mFOL-freevars(body)))
                    ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))])
5. L : ℤ List
6. ¬(z ∈ L)
7. fmla' : mFOL()
8. mFOL-freevars(fmla') = mFOL-freevars(body) ∈ (ℤ List)
9. FOL-abstract(fmla') = FOL-abstract(body) ∈ AbstractFOFormula+(mFOL-freevars(body))
10. l_disjoint(ℤ;L;mFOL-boundvars(fmla'))
11. mFOL-freevars(mFOquant(isall;z;fmla')) = mFOL-freevars(mFOquant(isall;z;body)) ∈ (ℤ List)
12. FOL-abstract(mFOquant(isall;z;fmla'))
= FOL-abstract(mFOquant(isall;z;body))
∈ AbstractFOFormula+(mFOL-freevars(mFOquant(isall;z;body)))
⊢ l_disjoint(ℤ;L;mFOL-boundvars(mFOquant(isall;z;fmla')))

---

Latex:

---

Latex:

1.  isall  :  \mBbbB{}
2.  z  :  \mBbbZ{}
3.  body  :  mFOL()
4.  \mforall{}L:\mBbbZ{}  List
          (\mexists{}fmla':mFOL()  [((mFOL-freevars(fmla')  =  mFOL-freevars(body))
                                        \mwedge{}  (FOL-abstract(fmla')  =  FOL-abstract(body))
                                        \mwedge{}  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla')))])
5.  L  :  \mBbbZ{}  List
6.  \mneg{}(z  \mmember{}  L)
\mvdash{}  \mexists{}fmla':mFOL()  [((mFOL-freevars(fmla')  =  mFOL-freevars(mFOquant(isall;z;body)))
                                \mwedge{}  (FOL-abstract(fmla')  =  FOL-abstract(mFOquant(isall;z;body)))
                                \mwedge{}  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla')))]


By

---

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

---

Home Index