---

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

No Annotations
∀z,z':ℤ. ∀fmla':mFOL().
  ((¬(z' ∈ mFOL-boundvars(fmla')))
  ⇒ (¬(z' ∈ mFOL-freevars(fmla')))
  ⇒ (filter(λx.(¬b(x =z z'));mFOL-freevars(mFOL-rename(fmla';z;z')))
     = filter(λx.(¬b(x =z z));mFOL-freevars(fmla'))
     ∈ (ℤ List)))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (BLemma `mFOL-induction` THEN Auto)
   THEN RepUR ``mFOL-rename mFOL-freevars`` 0
   THEN Try (Folds ``mFOL-rename mFOL-freevars`` 0)) }

1
1. z : ℤ
2. z' : ℤ
3. name : Atom
4. vars : ℤ List
5. ¬(z' ∈ mFOL-boundvars(name(vars)))
6. ¬(z' ∈ mFOL-freevars(name(vars)))
⊢ filter(λx.(¬b(x =z z'));remove-repeats(IntDeq;map(λv.if (v =z z) then z' else v fi ;vars)))
= filter(λx.(¬b(x =z z));remove-repeats(IntDeq;vars))
∈ (ℤ List)

2
1. z : ℤ
2. z' : ℤ
3. knd : Atom
4. left : mFOL()
5. right : mFOL()
6. (¬(z' ∈ mFOL-boundvars(left)))
⇒ (¬(z' ∈ mFOL-freevars(left)))
⇒ (filter(λx.(¬b(x =z z'));mFOL-freevars(mFOL-rename(left;z;z')))
   = filter(λx.(¬b(x =z z));mFOL-freevars(left))
   ∈ (ℤ List))
7. (¬(z' ∈ mFOL-boundvars(right)))
⇒ (¬(z' ∈ mFOL-freevars(right)))
⇒ (filter(λx.(¬b(x =z z'));mFOL-freevars(mFOL-rename(right;z;z')))
   = filter(λx.(¬b(x =z z));mFOL-freevars(right))
   ∈ (ℤ List))
8. ¬(z' ∈ mFOL-boundvars(mFOconnect(knd;left;right)))
9. ¬(z' ∈ mFOL-freevars(mFOconnect(knd;left;right)))
⊢ filter(λx.(¬b(x =z z'));
         val-union(IntDeq;mFOL-freevars(mFOL-rename(left;z;z'));mFOL-freevars(mFOL-rename(right;z;z'))))
= filter(λx.(¬b(x =z z));val-union(IntDeq;mFOL-freevars(left);mFOL-freevars(right)))
∈ (ℤ List)

3
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)

---

Latex:

---

Latex:
No  Annotations
\mforall{}z,z':\mBbbZ{}.  \mforall{}fmla':mFOL().
    ((\mneg{}(z'  \mmember{}  mFOL-boundvars(fmla')))
    {}\mRightarrow{}  (\mneg{}(z'  \mmember{}  mFOL-freevars(fmla')))
    {}\mRightarrow{}  (filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z'));mFOL-freevars(mFOL-rename(fmla';z;z')))
          =  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z));mFOL-freevars(fmla'))))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (BLemma  `mFOL-induction`  THEN  Auto)
  THEN  RepUR  ``mFOL-rename  mFOL-freevars``  0
  THEN  Try  (Folds  ``mFOL-rename  mFOL-freevars``  0))

---

Home Index