---

Step * 3 of Lemma filter-mFOL-freevars-of-rename


1. z : ℤ
2. z' : ℤ
3. isall : 𝔹
4. var : ℤ
5. body : mFOL()
6. (¬(z' ∈ mFOL-boundvars(body)))
⇒ (¬(z' ∈ mFOL-freevars(body)))
⇒ (filter(λx.(¬b(x =z z'));mFOL-freevars(mFOL-rename(body;z;z')))
   = filter(λx.(¬b(x =z z));mFOL-freevars(body))
   ∈ (ℤ List))
7. ¬(z' ∈ mFOL-boundvars(mFOquant(isall;var;body)))
8. ¬(z' ∈ mFOL-freevars(mFOquant(isall;var;body)))
⊢ filter(λx.(¬b(x =z z'));filter(λx.(¬b(x =z var));
                                 mFOL-freevars(if (var =z z) then body else mFOL-rename(body;z;z') fi )))
= filter(λx.(¬b(x =z z));filter(λx.(¬b(x =z var));mFOL-freevars(body)))
∈ (ℤ List)
BY
{ (RepUR ``mFOL-freevars`` -1
   THEN Fold `mFOL-freevars` (-1)
   THEN RepUR ``mFOL-boundvars`` -2
   THEN Fold `mFOL-boundvars` (-2)) }

1
1. z : ℤ
2. z' : ℤ
3. isall : 𝔹
4. var : ℤ
5. body : mFOL()
6. (¬(z' ∈ mFOL-boundvars(body)))
⇒ (¬(z' ∈ mFOL-freevars(body)))
⇒ (filter(λx.(¬b(x =z z'));mFOL-freevars(mFOL-rename(body;z;z')))
   = filter(λx.(¬b(x =z z));mFOL-freevars(body))
   ∈ (ℤ List))
7. ¬(z' ∈ insert(var;mFOL-boundvars(body)))
8. ¬(z' ∈ filter(λx.(¬b(x =z var));mFOL-freevars(body)))
⊢ filter(λx.(¬b(x =z z'));filter(λx.(¬b(x =z var));
                                 mFOL-freevars(if (var =z z) then body else mFOL-rename(body;z;z') fi )))
= filter(λx.(¬b(x =z z));filter(λx.(¬b(x =z var));mFOL-freevars(body)))
∈ (ℤ List)

---

Latex:

---

Latex:

1.  z  :  \mBbbZ{}
2.  z'  :  \mBbbZ{}
3.  isall  :  \mBbbB{}
4.  var  :  \mBbbZ{}
5.  body  :  mFOL()
6.  (\mneg{}(z'  \mmember{}  mFOL-boundvars(body)))
{}\mRightarrow{}  (\mneg{}(z'  \mmember{}  mFOL-freevars(body)))
{}\mRightarrow{}  (filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z'));mFOL-freevars(mFOL-rename(body;z;z')))
      =  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z));mFOL-freevars(body)))
7.  \mneg{}(z'  \mmember{}  mFOL-boundvars(mFOquant(isall;var;body)))
8.  \mneg{}(z'  \mmember{}  mFOL-freevars(mFOquant(isall;var;body)))
\mvdash{}  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z'));filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  var));mFOL-freevars(if  (var  =\msubz{}  z)
                                                                                                      then  body
                                                                                                      else  mFOL-rename(body;z;z')
                                                                                                      fi  )))
=  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z));filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  var));mFOL-freevars(body)))


By

---

Latex:
(RepUR  ``mFOL-freevars``  -1
  THEN  Fold  `mFOL-freevars`  (-1)
  THEN  RepUR  ``mFOL-boundvars``  -2
  THEN  Fold  `mFOL-boundvars`  (-2))

---

Home Index