---

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


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'));mFOL-freevars(mFOL-rename(left;z;z')) ⋃ mFOL-freevars(mFOL-rename(right;z;z')))
= filter(λx.(¬b(x =z z));mFOL-freevars(left) ⋃ mFOL-freevars(right))
∈ (ℤ List)
BY
{ (Assert (¬(z' ∈ mFOL-boundvars(left))) ∧ (¬(z' ∈ mFOL-boundvars(right))) BY
         (D 0
          THEN ParallelOp -2
          THEN RepUR ``mFOL-boundvars`` 0
          THEN Fold `mFOL-boundvars` 0
          THEN RWO "member-union" 0
          THEN Auto)) }

1
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)))
10. (¬(z' ∈ mFOL-boundvars(left))) ∧ (¬(z' ∈ mFOL-boundvars(right)))
⊢ filter(λx.(¬b(x =z z'));mFOL-freevars(mFOL-rename(left;z;z')) ⋃ mFOL-freevars(mFOL-rename(right;z;z')))
= filter(λx.(¬b(x =z z));mFOL-freevars(left) ⋃ mFOL-freevars(right))
∈ (ℤ List)

---

Latex:

---

Latex:

1.  z  :  \mBbbZ{}
2.  z'  :  \mBbbZ{}
3.  knd  :  Atom
4.  left  :  mFOL()
5.  right  :  mFOL()
6.  (\mneg{}(z'  \mmember{}  mFOL-boundvars(left)))
{}\mRightarrow{}  (\mneg{}(z'  \mmember{}  mFOL-freevars(left)))
{}\mRightarrow{}  (filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z'));mFOL-freevars(mFOL-rename(left;z;z')))
      =  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z));mFOL-freevars(left)))
7.  (\mneg{}(z'  \mmember{}  mFOL-boundvars(right)))
{}\mRightarrow{}  (\mneg{}(z'  \mmember{}  mFOL-freevars(right)))
{}\mRightarrow{}  (filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z'));mFOL-freevars(mFOL-rename(right;z;z')))
      =  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z));mFOL-freevars(right)))
8.  \mneg{}(z'  \mmember{}  mFOL-boundvars(mFOconnect(knd;left;right)))
9.  \mneg{}(z'  \mmember{}  mFOL-freevars(mFOconnect(knd;left;right)))
\mvdash{}  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z'));mFOL-freevars(mFOL-rename(left;z;z'))  \mcup{}
                                                      mFOL-freevars(mFOL-rename(right;z;z')))
=  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z));mFOL-freevars(left)  \mcup{}  mFOL-freevars(right))


By

---

Latex:
(Assert  (\mneg{}(z'  \mmember{}  mFOL-boundvars(left)))  \mwedge{}  (\mneg{}(z'  \mmember{}  mFOL-boundvars(right)))  BY
              (D  0
                THEN  ParallelOp  -2
                THEN  RepUR  ``mFOL-boundvars``  0
                THEN  Fold  `mFOL-boundvars`  0
                THEN  RWO  "member-union"  0
                THEN  Auto))

---

Home Index