---

Step * 2 of Lemma mFOL-boundvars-of-rename


1. old : ℤ
2. new : ℤ
3. isall : 𝔹@i
4. var : ℤ@i
5. body : mFOL()@i
6. mFOL-boundvars(mFOL-rename(body;old;new)) = mFOL-boundvars(body) ∈ (ℤ List)@i
⊢ insert(var;mFOL-boundvars(if (var =z old) then body else mFOL-rename(body;old;new) fi ))
= insert(var;mFOL-boundvars(body))
∈ (ℤ List)
BY
{ AutoSplit }

---

Latex:



1.  old  :  \mBbbZ{}
2.  new  :  \mBbbZ{}
3.  isall  :  \mBbbB{}@i
4.  var  :  \mBbbZ{}@i
5.  body  :  mFOL()@i
6.  mFOL-boundvars(mFOL-rename(body;old;new))  =  mFOL-boundvars(body)@i
\mvdash{}  insert(var;mFOL-boundvars(if  (var  =\msubz{}  old)  then  body  else  mFOL-rename(body;old;new)  fi  ))
=  insert(var;mFOL-boundvars(body))


By

AutoSplit

---

Home Index