---

Step * 2 of Lemma mFOL-bound-rename


1. knd : Atom
2. left : mFOL()
3. right : mFOL()
4. ∀L:ℤ List
     (∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(left) ∈ (ℤ List))
                    ∧ (mFOL-abstract(fmla') = mFOL-abstract(left) ∈ AbstractFOFormula(mFOL-freevars(left)))
                    ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))])
5. ∀L:ℤ List
     (∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(right) ∈ (ℤ List))
                    ∧ (mFOL-abstract(fmla') = mFOL-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))
                ∧ (mFOL-abstract(fmla')
                  = mFOL-abstract(mFOconnect(knd;left;right))
                  ∈ AbstractFOFormula(mFOL-freevars(mFOconnect(knd;left;right))))
                ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))]
BY
{ (((InstHyp [⌜L⌝] (-3)⋅ THENA Auto) THEN D -1 THEN RenameVar `l' (-2))
   THEN (InstHyp [⌜L⌝] (-4)⋅ THENA Auto)
   THEN D -1
   THEN RenameVar `r' (-2)
   THEN With ⌜mFOconnect(knd;l;r)⌝ (D 0)⋅
   THEN Auto
   THEN RepUR ``mFOL-freevars`` 0
   THEN Try (Fold `mFOL-freevars` 0)
   THEN Auto) }

1
1. knd : Atom
2. left : mFOL()
3. right : mFOL()
4. ∀L:ℤ List
     (∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(left) ∈ (ℤ List))
                    ∧ (mFOL-abstract(fmla') = mFOL-abstract(left) ∈ AbstractFOFormula(mFOL-freevars(left)))
                    ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))])
5. ∀L:ℤ List
     (∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(right) ∈ (ℤ List))
                    ∧ (mFOL-abstract(fmla') = mFOL-abstract(right) ∈ AbstractFOFormula(mFOL-freevars(right)))
                    ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))])
6. L : ℤ List
7. l : mFOL()
8. mFOL-freevars(l) = mFOL-freevars(left) ∈ (ℤ List)
9. mFOL-abstract(l) = mFOL-abstract(left) ∈ AbstractFOFormula(mFOL-freevars(left))
10. l_disjoint(ℤ;L;mFOL-boundvars(l))
11. r : mFOL()
12. mFOL-freevars(r) = mFOL-freevars(right) ∈ (ℤ List)
13. mFOL-abstract(r) = mFOL-abstract(right) ∈ AbstractFOFormula(mFOL-freevars(right))
14. l_disjoint(ℤ;L;mFOL-boundvars(r))
15. mFOL-freevars(mFOconnect(knd;l;r)) = mFOL-freevars(mFOconnect(knd;left;right)) ∈ (ℤ List)
⊢ mFOL-abstract(mFOconnect(knd;l;r))
= mFOL-abstract(mFOconnect(knd;left;right))
∈ AbstractFOFormula(val-union(IntDeq;mFOL-freevars(left);mFOL-freevars(right)))

2
1. knd : Atom
2. left : mFOL()
3. right : mFOL()
4. ∀L:ℤ List
     (∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(left) ∈ (ℤ List))
                    ∧ (mFOL-abstract(fmla') = mFOL-abstract(left) ∈ AbstractFOFormula(mFOL-freevars(left)))
                    ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))])
5. ∀L:ℤ List
     (∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(right) ∈ (ℤ List))
                    ∧ (mFOL-abstract(fmla') = mFOL-abstract(right) ∈ AbstractFOFormula(mFOL-freevars(right)))
                    ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))])
6. L : ℤ List
7. l : mFOL()
8. mFOL-freevars(l) = mFOL-freevars(left) ∈ (ℤ List)
9. mFOL-abstract(l) = mFOL-abstract(left) ∈ AbstractFOFormula(mFOL-freevars(left))
10. l_disjoint(ℤ;L;mFOL-boundvars(l))
11. r : mFOL()
12. mFOL-freevars(r) = mFOL-freevars(right) ∈ (ℤ List)
13. mFOL-abstract(r) = mFOL-abstract(right) ∈ AbstractFOFormula(mFOL-freevars(right))
14. l_disjoint(ℤ;L;mFOL-boundvars(r))
15. mFOL-freevars(mFOconnect(knd;l;r)) = mFOL-freevars(mFOconnect(knd;left;right)) ∈ (ℤ List)
16. mFOL-abstract(mFOconnect(knd;l;r))
= mFOL-abstract(mFOconnect(knd;left;right))
∈ AbstractFOFormula(mFOL-freevars(mFOconnect(knd;left;right)))
⊢ l_disjoint(ℤ;L;mFOL-boundvars(mFOconnect(knd;l;r)))

---

Latex:

---

Latex:

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


By

---

Latex:
(((InstHyp  [\mkleeneopen{}L\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)  THEN  D  -1  THEN  RenameVar  `l'  (-2))
  THEN  (InstHyp  [\mkleeneopen{}L\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  RenameVar  `r'  (-2)
  THEN  With  \mkleeneopen{}mFOconnect(knd;l;r)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  RepUR  ``mFOL-freevars``  0
  THEN  Try  (Fold  `mFOL-freevars`  0)
  THEN  Auto)

---

Home Index