---

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


1. old : ℤ
2. new : ℤ
3. isall : 𝔹
4. var : ℤ
5. body : mFOL()
6. mFOL-boundvars(mFOL-rename(body;old;new)) = mFOL-boundvars(body) ∈ (ℤ List)
⊢ 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:

---

Latex:

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


By

---

Latex:
AutoSplit

---

Home Index