---

Step * of Lemma mFOL-boundvars-of-rename

∀[fmla:mFOL()]. ∀[old,new:ℤ].  (mFOL-boundvars(mFOL-rename(fmla;old;new)) = mFOL-boundvars(fmla) ∈ (ℤ List))
BY
{ (Auto
   THEN MoveToConcl 1
   THEN BLemma `mFOL-induction`
   THEN Auto
   THEN RepUR ``mFOL-boundvars mFOL-rename`` 0
   THEN Try (Fold `mFOL-rename` 0)
   THEN Try (Fold `mFOL-boundvars` 0)) }

1
1. old : ℤ
2. new : ℤ
3. knd : Atom@i
4. left : mFOL()@i
5. right : mFOL()@i
6. mFOL-boundvars(mFOL-rename(left;old;new)) = mFOL-boundvars(left) ∈ (ℤ List)@i
7. mFOL-boundvars(mFOL-rename(right;old;new)) = mFOL-boundvars(right) ∈ (ℤ List)@i
⊢ mFOL-boundvars(mFOL-rename(left;old;new)) ∪ mFOL-boundvars(mFOL-rename(right;old;new))
= mFOL-boundvars(left) ∪ mFOL-boundvars(right)
∈ (ℤ List)

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

---

Latex:


\mforall{}[fmla:mFOL()].  \mforall{}[old,new:\mBbbZ{}].    (mFOL-boundvars(mFOL-rename(fmla;old;new))  =  mFOL-boundvars(fmla))


By

(Auto
  THEN  MoveToConcl  1
  THEN  BLemma  `mFOL-induction`
  THEN  Auto
  THEN  RepUR  ``mFOL-boundvars  mFOL-rename``  0
  THEN  Try  (Fold  `mFOL-rename`  0)
  THEN  Try  (Fold  `mFOL-boundvars`  0))

---

Home Index