---

Step * 1 of Lemma mFOL-bound-rename


1. name : Atom
2. vars : ℤ List
3. L : ℤ List
⊢ ∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(name(vars)) ∈ (ℤ List))
                ∧ (mFOL-abstract(fmla') = mFOL-abstract(name(vars)) ∈ AbstractFOFormula(mFOL-freevars(name(vars))))
                ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))]
BY
{ ((With ⌜name(vars)⌝ (D 0)⋅ THEN Auto) THEN RepUR ``mFOL-boundvars`` 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

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

---

Home Index