---

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


1. knd : Atom
2. left : mFOL()
3. right : mFOL()
4. ∀old,new:ℤ.
     ∀x:ℤ
       ((x ∈ mFOL-freevars(mFOL-rename(left;old;new)))
       ⇐⇒ ((¬(x = old ∈ ℤ)) ∧ (x ∈ mFOL-freevars(left))) ∨ ((x = new ∈ ℤ) ∧ (old ∈ mFOL-freevars(left)))) 
     supposing ¬(new ∈ mFOL-boundvars(left))
5. ∀old,new:ℤ.
     ∀x:ℤ
       ((x ∈ mFOL-freevars(mFOL-rename(right;old;new)))
       ⇐⇒ ((¬(x = old ∈ ℤ)) ∧ (x ∈ mFOL-freevars(right))) ∨ ((x = new ∈ ℤ) ∧ (old ∈ mFOL-freevars(right)))) 
     supposing ¬(new ∈ mFOL-boundvars(right))
6. old : ℤ
7. new : ℤ
8. ¬(new ∈ mFOL-boundvars(left) ⋃ mFOL-boundvars(right))
9. x : ℤ
10. (¬(new ∈ mFOL-boundvars(left))) ∧ (¬(new ∈ mFOL-boundvars(right)))
⊢ (((¬(x = old ∈ ℤ)) ∧ (x ∈ mFOL-freevars(left))) ∨ ((x = new ∈ ℤ) ∧ (old ∈ mFOL-freevars(left))))
  ∨ ((¬(x = old ∈ ℤ)) ∧ (x ∈ mFOL-freevars(right)))
  ∨ ((x = new ∈ ℤ) ∧ (old ∈ mFOL-freevars(right)))
⇐⇒ ((¬(x = old ∈ ℤ)) ∧ ((x ∈ mFOL-freevars(left)) ∨ (x ∈ mFOL-freevars(right))))
    ∨ ((x = new ∈ ℤ) ∧ ((old ∈ mFOL-freevars(left)) ∨ (old ∈ mFOL-freevars(right))))
BY
{ (Auto THEN RepeatFor 2 ((SplitOrHyps THEN Auto))) }

---

Latex:

---

Latex:

1.  knd  :  Atom
2.  left  :  mFOL()
3.  right  :  mFOL()
4.  \mforall{}old,new:\mBbbZ{}.
          \mforall{}x:\mBbbZ{}
              ((x  \mmember{}  mFOL-freevars(mFOL-rename(left;old;new)))
              \mLeftarrow{}{}\mRightarrow{}  ((\mneg{}(x  =  old))  \mwedge{}  (x  \mmember{}  mFOL-freevars(left)))  \mvee{}  ((x  =  new)  \mwedge{}  (old  \mmember{}  mFOL-freevars(left)))) 
          supposing  \mneg{}(new  \mmember{}  mFOL-boundvars(left))
5.  \mforall{}old,new:\mBbbZ{}.
          \mforall{}x:\mBbbZ{}
              ((x  \mmember{}  mFOL-freevars(mFOL-rename(right;old;new)))
              \mLeftarrow{}{}\mRightarrow{}  ((\mneg{}(x  =  old))  \mwedge{}  (x  \mmember{}  mFOL-freevars(right)))
                      \mvee{}  ((x  =  new)  \mwedge{}  (old  \mmember{}  mFOL-freevars(right)))) 
          supposing  \mneg{}(new  \mmember{}  mFOL-boundvars(right))
6.  old  :  \mBbbZ{}
7.  new  :  \mBbbZ{}
8.  \mneg{}(new  \mmember{}  mFOL-boundvars(left)  \mcup{}  mFOL-boundvars(right))
9.  x  :  \mBbbZ{}
10.  (\mneg{}(new  \mmember{}  mFOL-boundvars(left)))  \mwedge{}  (\mneg{}(new  \mmember{}  mFOL-boundvars(right)))
\mvdash{}  (((\mneg{}(x  =  old))  \mwedge{}  (x  \mmember{}  mFOL-freevars(left)))  \mvee{}  ((x  =  new)  \mwedge{}  (old  \mmember{}  mFOL-freevars(left))))
    \mvee{}  ((\mneg{}(x  =  old))  \mwedge{}  (x  \mmember{}  mFOL-freevars(right)))
    \mvee{}  ((x  =  new)  \mwedge{}  (old  \mmember{}  mFOL-freevars(right)))
\mLeftarrow{}{}\mRightarrow{}  ((\mneg{}(x  =  old))  \mwedge{}  ((x  \mmember{}  mFOL-freevars(left))  \mvee{}  (x  \mmember{}  mFOL-freevars(right))))
        \mvee{}  ((x  =  new)  \mwedge{}  ((old  \mmember{}  mFOL-freevars(left))  \mvee{}  (old  \mmember{}  mFOL-freevars(right))))


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((SplitOrHyps  THEN  Auto)))

---

Home Index