---

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


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

1
1. isall : 𝔹
2. z : ℤ
3. body : mFOL()
4. ∀L:ℤ List
     (∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(body) ∈ (ℤ List))
                    ∧ (mFOL-abstract(fmla') = mFOL-abstract(body) ∈ AbstractFOFormula(mFOL-freevars(body)))
                    ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))])
5. L : ℤ List
6. (z ∈ L)
7. fmla' : mFOL()
8. [%6] : (mFOL-freevars(fmla') = mFOL-freevars(body) ∈ (ℤ List))
∧ (mFOL-abstract(fmla') = mFOL-abstract(body) ∈ AbstractFOFormula(mFOL-freevars(body)))
∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla'))
9. z' : ℤ
10. ¬(z' ∈ L)
11. ¬(z' ∈ mFOL-boundvars(fmla'))
12. ¬(z' ∈ mFOL-freevars(fmla'))
⊢ ∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(mFOquant(isall;z;body)) ∈ (ℤ List))
                ∧ (mFOL-abstract(fmla')
                  = mFOL-abstract(mFOquant(isall;z;body))
                  ∈ AbstractFOFormula(mFOL-freevars(mFOquant(isall;z;body))))
                ∧ l_disjoint(ℤ;L;mFOL-boundvars(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{}  (mFOL-abstract(fmla')  =  mFOL-abstract(body))
                                        \mwedge{}  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla')))])
5.  L  :  \mBbbZ{}  List
6.  (z  \mmember{}  L)
7.  fmla'  :  mFOL()
8.  [\%6]  :  (mFOL-freevars(fmla')  =  mFOL-freevars(body))
\mwedge{}  (mFOL-abstract(fmla')  =  mFOL-abstract(body))
\mwedge{}  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla'))
9.  \mexists{}z':\mBbbZ{}.  ((\mneg{}(z'  \mmember{}  L))  \mwedge{}  (\mneg{}(z'  \mmember{}  mFOL-boundvars(fmla')))  \mwedge{}  (\mneg{}(z'  \mmember{}  mFOL-freevars(fmla'))))
\mvdash{}  \mexists{}fmla':mFOL()  [((mFOL-freevars(fmla')  =  mFOL-freevars(mFOquant(isall;z;body)))
                                \mwedge{}  (mFOL-abstract(fmla')  =  mFOL-abstract(mFOquant(isall;z;body)))
                                \mwedge{}  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla')))]


By

---

Latex:
ExRepD

---

Home Index