---

Step * of Lemma FOL-bound-rename

∀fmla:mFOL(). ∀L:ℤ List.
  (∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(fmla) ∈ (ℤ List))
                 ∧ (FOL-abstract(fmla') = FOL-abstract(fmla) ∈ AbstractFOFormula+(mFOL-freevars(fmla)))
                 ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))])
BY
{ (BLemmaUp `mFOL-induction` THEN At ⌜𝕌'⌝ Auto⋅) }

1
1. name : Atom
2. vars : ℤ List
3. L : ℤ List
⊢ ∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(name(vars)) ∈ (ℤ List))
                ∧ (FOL-abstract(fmla') = FOL-abstract(name(vars)) ∈ AbstractFOFormula+(mFOL-freevars(name(vars))))
                ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))]

2
1. knd : Atom
2. left : mFOL()
3. right : mFOL()
4. ∀L:ℤ List
     (∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(left) ∈ (ℤ List))
                    ∧ (FOL-abstract(fmla') = FOL-abstract(left) ∈ AbstractFOFormula+(mFOL-freevars(left)))
                    ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))])
5. ∀L:ℤ List
     (∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(right) ∈ (ℤ List))
                    ∧ (FOL-abstract(fmla') = FOL-abstract(right) ∈ AbstractFOFormula+(mFOL-freevars(right)))
                    ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))])
6. L : ℤ List
⊢ ∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(mFOconnect(knd;left;right)) ∈ (ℤ List))
                ∧ (FOL-abstract(fmla')
                  = FOL-abstract(mFOconnect(knd;left;right))
                  ∈ AbstractFOFormula+(mFOL-freevars(mFOconnect(knd;left;right))))
                ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))]

3
1. isall : 𝔹
2. var : ℤ
3. body : mFOL()
4. ∀L:ℤ List
     (∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(body) ∈ (ℤ List))
                    ∧ (FOL-abstract(fmla') = FOL-abstract(body) ∈ AbstractFOFormula+(mFOL-freevars(body)))
                    ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))])
5. L : ℤ List
⊢ ∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(mFOquant(isall;var;body)) ∈ (ℤ List))
                ∧ (FOL-abstract(fmla')
                  = FOL-abstract(mFOquant(isall;var;body))
                  ∈ AbstractFOFormula+(mFOL-freevars(mFOquant(isall;var;body))))
                ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))]

---

Latex:

---

Latex:
\mforall{}fmla:mFOL().  \mforall{}L:\mBbbZ{}  List.
    (\mexists{}fmla':mFOL()  [((mFOL-freevars(fmla')  =  mFOL-freevars(fmla))
                                  \mwedge{}  (FOL-abstract(fmla')  =  FOL-abstract(fmla))
                                  \mwedge{}  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla')))])


By

---

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

---

Home Index