---

Step * 2 of Lemma mFOL-bound-rename


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')))}
BY
{ (RepeatFor 2 ((InstHyp [⌈L⌉] (-3)⋅ THENA Auto)) THEN ExRepD THEN With ⌈mFOconnect(knd;f1;fmla')⌉ (D 0)⋅ THEN Auto) }

1
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'
7. f1 : mFOL()
8. mFOL-abstract(f1) = mFOL-abstract(left) ∈ AbstractFOFormula
9. l_disjoint(ℤ;L;mFOL-boundvars(f1))
10. fmla' : mFOL()
11. mFOL-abstract(fmla') = mFOL-abstract(right) ∈ AbstractFOFormula
12. l_disjoint(ℤ;L;mFOL-boundvars(fmla'))
⊢ mFOL-abstract(mFOconnect(knd;f1;fmla')) = mFOL-abstract(mFOconnect(knd;left;right)) ∈ AbstractFOFormula

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'
7. f1 : mFOL()
8. mFOL-abstract(f1) = mFOL-abstract(left) ∈ AbstractFOFormula
9. l_disjoint(ℤ;L;mFOL-boundvars(f1))
10. fmla' : mFOL()
11. mFOL-abstract(fmla') = mFOL-abstract(right) ∈ AbstractFOFormula
12. l_disjoint(ℤ;L;mFOL-boundvars(fmla'))
13. mFOL-abstract(mFOconnect(knd;f1;fmla')) = mFOL-abstract(mFOconnect(knd;left;right)) ∈ AbstractFOFormula
⊢ l_disjoint(ℤ;L;mFOL-boundvars(mFOconnect(knd;f1;fmla')))

---

Latex:



1.  knd  :  Atom@i'
2.  left  :  mFOL()@i'
3.  right  :  mFOL()@i'
4.  \mforall{}L:\mBbbZ{}  List
          (\mexists{}fmla':\{mFOL()|  ((mFOL-abstract(fmla')  =  mFOL-abstract(left))
                                            \mwedge{}  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla')))\})@i'
5.  \mforall{}L:\mBbbZ{}  List
          (\mexists{}fmla':\{mFOL()|  ((mFOL-abstract(fmla')  =  mFOL-abstract(right))
                                            \mwedge{}  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla')))\})@i'
6.  L  :  \mBbbZ{}  List@i'
\mvdash{}  \mexists{}fmla':\{mFOL()|  ((mFOL-abstract(fmla')  =  mFOL-abstract(mFOconnect(knd;left;right)))
                                    \mwedge{}  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla')))\}


By

(RepeatFor  2  ((InstHyp  [\mkleeneopen{}L\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto))
  THEN  ExRepD
  THEN  With  \mkleeneopen{}mFOconnect(knd;f1;fmla')\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto)

---

Home Index