---

Step * 3 1 1 2 1 3 1 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. mFOL-freevars(fmla') = mFOL-freevars(body) ∈ (ℤ List)
9. mFOL-abstract(fmla') = mFOL-abstract(body) ∈ AbstractFOFormula(mFOL-freevars(body))
10. l_disjoint(ℤ;L;mFOL-boundvars(fmla'))
11. z' : ℤ
12. ¬(z' ∈ L)
13. ¬(z' ∈ mFOL-boundvars(fmla'))
14. ¬(z' ∈ mFOL-freevars(fmla'))
15. mFOL-freevars(mFOquant(isall;z';mFOL-rename(fmla';z;z'))) = mFOL-freevars(mFOquant(isall;z;body)) ∈ (ℤ List)
16. mFOL-abstract(mFOquant(isall;z';mFOL-rename(fmla';z;z')))
= mFOL-abstract(mFOquant(isall;z;body))
∈ AbstractFOFormula(mFOL-freevars(mFOquant(isall;z;body)))
⊢ l_disjoint(ℤ;L;insert(z';mFOL-boundvars(fmla')))
BY
{ (RepeatFor 2 ((D 0 THEN Auto))
   THEN RWO "member-insert" (-1)
   THEN Auto
   THEN D -1
   THEN OnMaybeHyp 10 (\h. ((With ⌜x⌝ (D h)⋅ THENM D -1) THEN Complete (Auto))))⋅ }

---

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.  mFOL-freevars(fmla')  =  mFOL-freevars(body)
9.  mFOL-abstract(fmla')  =  mFOL-abstract(body)
10.  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla'))
11.  z'  :  \mBbbZ{}
12.  \mneg{}(z'  \mmember{}  L)
13.  \mneg{}(z'  \mmember{}  mFOL-boundvars(fmla'))
14.  \mneg{}(z'  \mmember{}  mFOL-freevars(fmla'))
15.  mFOL-freevars(mFOquant(isall;z';mFOL-rename(fmla';z;z')))
=  mFOL-freevars(mFOquant(isall;z;body))
16.  mFOL-abstract(mFOquant(isall;z';mFOL-rename(fmla';z;z')))
=  mFOL-abstract(mFOquant(isall;z;body))
\mvdash{}  l\_disjoint(\mBbbZ{};L;insert(z';mFOL-boundvars(fmla')))


By

---

Latex:
(RepeatFor  2  ((D  0  THEN  Auto))
  THEN  RWO  "member-insert"  (-1)
  THEN  Auto
  THEN  D  -1
  THEN  OnMaybeHyp  10  (\mbackslash{}h.  ((With  \mkleeneopen{}x\mkleeneclose{}  (D  h)\mcdot{}  THENM  D  -1)  THEN  Complete  (Auto))))\mcdot{}

---

Home Index