---

Step * of Lemma mFOL-bound-rename

∀fmla:mFOL(). ∀L:ℤ List.
  (∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(fmla) ∈ AbstractFOFormula)
                   ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))})
BY
{ (BLemmaUp `mFOL-induction` THEN At ⌈𝕌'⌉ Auto⋅) }

1
1. name : Atom@i'
2. vars : ℤ List@i'
3. L : ℤ List@i'
⊢ ∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(name(vars)) ∈ AbstractFOFormula)
                  ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))}

2
1. knd : Atom@i'
2. left : mFOL()@i'
3. right : mFOL()@i'
4. ∀L:ℤ List
     (∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(left) ∈ AbstractFOFormula)
                      ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))})@i'
5. ∀L:ℤ List
     (∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(right) ∈ AbstractFOFormula)
                      ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))})@i'
6. L : ℤ List@i'
⊢ ∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(mFOconnect(knd;left;right)) ∈ AbstractFOFormula)
                  ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))}

3
1. isall : 𝔹@i'
2. var : ℤ@i'
3. body : mFOL()@i'
4. ∀L:ℤ List
     (∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(body) ∈ AbstractFOFormula)
                      ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))})@i'
5. L : ℤ List@i'
⊢ ∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(mFOquant(isall;var;body)) ∈ AbstractFOFormula)
                  ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))}

---

Latex:


\mforall{}fmla:mFOL().  \mforall{}L:\mBbbZ{}  List.
    (\mexists{}fmla':\{mFOL()|  ((mFOL-abstract(fmla')  =  mFOL-abstract(fmla))
                                      \mwedge{}  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla')))\})


By

(BLemmaUp  `mFOL-induction`  THEN  At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  Auto\mcdot{})

---

Home Index