---

Step * 2 2 of Lemma FOL-bound-rename


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
7. l : mFOL()
8. mFOL-freevars(l) = mFOL-freevars(left) ∈ (ℤ List)
9. FOL-abstract(l) = FOL-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. FOL-abstract(r) = FOL-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. FOL-abstract(mFOconnect(knd;l;r))
= FOL-abstract(mFOconnect(knd;left;right))
∈ AbstractFOFormula+(mFOL-freevars(mFOconnect(knd;left;right)))
⊢ l_disjoint(ℤ;L;mFOL-boundvars(mFOconnect(knd;l;r)))
BY
{ (Unfold `mFOL-boundvars` 0 THEN Reduce 0 THEN Fold `mFOL-boundvars` 0) }

1
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
7. l : mFOL()
8. mFOL-freevars(l) = mFOL-freevars(left) ∈ (ℤ List)
9. FOL-abstract(l) = FOL-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. FOL-abstract(r) = FOL-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. FOL-abstract(mFOconnect(knd;l;r))
= FOL-abstract(mFOconnect(knd;left;right))
∈ AbstractFOFormula+(mFOL-freevars(mFOconnect(knd;left;right)))
⊢ l_disjoint(ℤ;L;mFOL-boundvars(l) ⋃ mFOL-boundvars(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{}  (FOL-abstract(fmla')  =  FOL-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{}  (FOL-abstract(fmla')  =  FOL-abstract(right))
                                        \mwedge{}  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla')))])
6.  L  :  \mBbbZ{}  List
7.  l  :  mFOL()
8.  mFOL-freevars(l)  =  mFOL-freevars(left)
9.  FOL-abstract(l)  =  FOL-abstract(left)
10.  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(l))
11.  r  :  mFOL()
12.  mFOL-freevars(r)  =  mFOL-freevars(right)
13.  FOL-abstract(r)  =  FOL-abstract(right)
14.  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(r))
15.  mFOL-freevars(mFOconnect(knd;l;r))  =  mFOL-freevars(mFOconnect(knd;left;right))
16.  FOL-abstract(mFOconnect(knd;l;r))  =  FOL-abstract(mFOconnect(knd;left;right))
\mvdash{}  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(mFOconnect(knd;l;r)))


By

---

Latex:
(Unfold  `mFOL-boundvars`  0  THEN  Reduce  0  THEN  Fold  `mFOL-boundvars`  0)

---

Home Index