---

Step * 3 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))))
⊢ (x ∈ filter(λx.(¬b(x =z var));mFOL-freevars(if (var =z old) then body else mFOL-rename(body;old;new) fi )))
⇐⇒ ((¬(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
{ AutoBoolCase ⌜(var =z old)⌝⋅ }

1
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))))

2
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. var ≠ old
7. new : ℤ
8. ¬((new = var ∈ ℤ) ∨ (new ∈ mFOL-boundvars(body)))
9. x : ℤ
10. ∀x:ℤ
      ((x ∈ mFOL-freevars(mFOL-rename(body;old;new)))
      ⇐⇒ ((¬(x = old ∈ ℤ)) ∧ (x ∈ mFOL-freevars(body))) ∨ ((x = new ∈ ℤ) ∧ (old ∈ mFOL-freevars(body))))
⊢ (x ∈ filter(λx.(¬b(x =z var));mFOL-freevars(mFOL-rename(body;old;new))))
⇐⇒ ((¬(x = old ∈ ℤ)) ∧ (x ∈ filter(λx.(¬b(x =z var));mFOL-freevars(body))))
    ∨ ((x = new ∈ ℤ) ∧ (old ∈ filter(λx.(¬b(x =z var));mFOL-freevars(body))))

---

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))))
\mvdash{}  (x  \mmember{}  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  var));mFOL-freevars(if  (var  =\msubz{}  old)
                                                                then  body
                                                                else  mFOL-rename(body;old;new)
                                                                fi  )))
\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:
AutoBoolCase  \mkleeneopen{}(var  =\msubz{}  old)\mkleeneclose{}\mcdot{}

---

Home Index