---

Step * 2 1 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)))
⊢ valueall-type(ℤ)
BY
{ Auto }

---

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{}  valueall-type(\mBbbZ{})


By

---

Latex:
Auto

---

Home Index