---

Step * 1 of Lemma mFOL-bound-rename


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')))}
BY
{ ((With ⌈name(vars)⌉ (D 0)⋅ THEN Auto) THEN RepUR ``mFOL-boundvars`` 0 THEN Auto)⋅ }

---

Latex:



1.  name  :  Atom@i'
2.  vars  :  \mBbbZ{}  List@i'
3.  L  :  \mBbbZ{}  List@i'
\mvdash{}  \mexists{}fmla':\{mFOL()|  ((mFOL-abstract(fmla')  =  mFOL-abstract(name(vars)))
                                    \mwedge{}  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla')))\}


By

((With  \mkleeneopen{}name(vars)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)  THEN  RepUR  ``mFOL-boundvars``  0  THEN  Auto)\mcdot{}

---

Home Index