---

Step * 3 1 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' ∈ 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)
BY
{ ((RWO "member-insert" (-2) THENA Auto)
   THEN (RWO "member_filter" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN MoveToConcl (-1)
   THEN (BoolCase ⌜(z' =z var)⌝⋅ THENA Auto)
   THEN (D 0 THENA Auto)) }

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' = var ∈ ℤ) ∨ (z' ∈ mFOL-boundvars(body)))
8. z' = var ∈ ℤ
9. ¬((z' ∈ mFOL-freevars(body)) ∧ False)
⊢ 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)

2
1. z : ℤ
2. z' : ℤ
3. isall : 𝔹
4. var : ℤ
5. z' ≠ var
6. body : mFOL()
7. (¬(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))
8. ¬((z' = var ∈ ℤ) ∨ (z' ∈ mFOL-boundvars(body)))
9. ¬((z' ∈ mFOL-freevars(body)) ∧ True)
⊢ 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{}  insert(var;mFOL-boundvars(body)))
8.  \mneg{}(z'  \mmember{}  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  var));mFOL-freevars(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:
((RWO  "member-insert"  (-2)  THENA  Auto)
  THEN  (RWO  "member\_filter"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  MoveToConcl  (-1)
  THEN  (BoolCase  \mkleeneopen{}(z'  =\msubz{}  var)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (D  0  THENA  Auto))

---

Home Index