---

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


1. isall : 𝔹
2. var : ℤ
3. body : mFOL()
4. ∀old,new:ℤ.
     ∀x:ℤ
       ((x ∈ mFOL-freevars(mFOL-rename(body;old;new)))
       ⇐⇒ ((¬(x = old ∈ ℤ)) ∧ (x ∈ mFOL-freevars(body))) ∨ ((x = new ∈ ℤ) ∧ (old ∈ mFOL-freevars(body)))) 
     supposing ¬(new ∈ mFOL-boundvars(body))
5. old : ℤ
6. new : ℤ
7. ¬((new = var ∈ ℤ) ∨ (new ∈ mFOL-boundvars(body)))
8. x : ℤ
9. ∀x:ℤ
     ((x ∈ mFOL-freevars(mFOL-rename(body;old;new)))
     ⇐⇒ ((¬(x = old ∈ ℤ)) ∧ (x ∈ mFOL-freevars(body))) ∨ ((x = new ∈ ℤ) ∧ (old ∈ mFOL-freevars(body))))
10. var = old ∈ ℤ
⊢ (x ∈ filter(λx.(¬b(x =z var));mFOL-freevars(body)))
⇐⇒ ((¬(x = old ∈ ℤ)) ∧ (x ∈ filter(λx.(¬b(x =z var));mFOL-freevars(body))))
    ∨ ((x = new ∈ ℤ) ∧ (old ∈ filter(λx.(¬b(x =z var));mFOL-freevars(body))))
BY
{ ((RWW "member_filter 9" 0 THENA Auto)
   THEN Reduce 0
   THEN (RW assert_pushdownC 0 THEN Auto)
   THEN SplitOrHyps
   THEN Auto) }

---

Latex:

---

Latex:

1.  isall  :  \mBbbB{}
2.  var  :  \mBbbZ{}
3.  body  :  mFOL()
4.  \mforall{}old,new:\mBbbZ{}.
          \mforall{}x:\mBbbZ{}
              ((x  \mmember{}  mFOL-freevars(mFOL-rename(body;old;new)))
              \mLeftarrow{}{}\mRightarrow{}  ((\mneg{}(x  =  old))  \mwedge{}  (x  \mmember{}  mFOL-freevars(body)))  \mvee{}  ((x  =  new)  \mwedge{}  (old  \mmember{}  mFOL-freevars(body)))) 
          supposing  \mneg{}(new  \mmember{}  mFOL-boundvars(body))
5.  old  :  \mBbbZ{}
6.  new  :  \mBbbZ{}
7.  \mneg{}((new  =  var)  \mvee{}  (new  \mmember{}  mFOL-boundvars(body)))
8.  x  :  \mBbbZ{}
9.  \mforall{}x:\mBbbZ{}
          ((x  \mmember{}  mFOL-freevars(mFOL-rename(body;old;new)))
          \mLeftarrow{}{}\mRightarrow{}  ((\mneg{}(x  =  old))  \mwedge{}  (x  \mmember{}  mFOL-freevars(body)))  \mvee{}  ((x  =  new)  \mwedge{}  (old  \mmember{}  mFOL-freevars(body))))
10.  var  =  old
\mvdash{}  (x  \mmember{}  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  var));mFOL-freevars(body)))
\mLeftarrow{}{}\mRightarrow{}  ((\mneg{}(x  =  old))  \mwedge{}  (x  \mmember{}  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  var));mFOL-freevars(body))))
        \mvee{}  ((x  =  new)  \mwedge{}  (old  \mmember{}  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  var));mFOL-freevars(body))))


By

---

Latex:
((RWW  "member\_filter  9"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (RW  assert\_pushdownC  0  THEN  Auto)
  THEN  SplitOrHyps
  THEN  Auto)

---

Home Index