---

Step * 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'));
         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)
BY
{ (RWO "val-union-l-union" 0 THENA 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)))
⊢ valueall-type(ℤ)

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'));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'));
                  val-union(IntDeq;mFOL-freevars(mFOL-rename(left;z;z'));mFOL-freevars(...)))
=  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z));val-union(IntDeq;mFOL-freevars(left);mFOL-freevars(right)))


By

---

Latex:
(RWO  "val-union-l-union"  0  THENA  Auto)

---

Home Index