---

Step * 2 1 1 of Lemma mFOL-rename-bound-to-avoid_wf


1. fmla : mFOL()@i
2. L : ℤ List@i
3. v : fmla:mFOL()
─→ L:(ℤ List)
─→ (∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(fmla) ∈ AbstractFOFormula)
                    ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))})@i'
4. TERMOF{mFOL-bound-rename:o, 1:l, i:l}
= v
∈ (∀fmla:mFOL(). ∀L:ℤ List.
     (∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(fmla) ∈ AbstractFOFormula)
                      ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))}))@i'
⊢ v fmla L ∈ {fmla':mFOL()| 
              (mFOL-abstract(fmla') = mFOL-abstract(fmla) ∈ AbstractFOFormula) ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla'))} 
BY
{ DoSubsume }

1
1. fmla : mFOL()@i
2. L : ℤ List@i
3. v : fmla:mFOL()
─→ L:(ℤ List)
─→ (∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(fmla) ∈ AbstractFOFormula)
                    ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))})@i'
4. TERMOF{mFOL-bound-rename:o, 1:l, i:l}
= v
∈ (∀fmla:mFOL(). ∀L:ℤ List.
     (∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(fmla) ∈ AbstractFOFormula)
                      ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))}))@i'
⊢ v fmla L ∈ ∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(fmla) ∈ AbstractFOFormula)
                             ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))}

2
1. fmla : mFOL()@i
2. L : ℤ List@i
3. v : fmla:mFOL()
─→ L:(ℤ List)
─→ (∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(fmla) ∈ AbstractFOFormula)
                    ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))})@i'
4. TERMOF{mFOL-bound-rename:o, 1:l, i:l}
= v
∈ (∀fmla:mFOL(). ∀L:ℤ List.
     (∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(fmla) ∈ AbstractFOFormula)
                      ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))}))@i'
5. (v fmla L)
= (v fmla L)
∈ (∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(fmla) ∈ AbstractFOFormula)
                   ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))})
⊢ (∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(fmla) ∈ AbstractFOFormula)
                   ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))}) ⊆r {fmla':mFOL()| 
                                                                  (mFOL-abstract(fmla')
                                                                  = mFOL-abstract(fmla)
                                                                  ∈ AbstractFOFormula)
                                                                  ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla'))} 

---

Latex:



1.  fmla  :  mFOL()@i
2.  L  :  \mBbbZ{}  List@i
3.  v  :  fmla:mFOL()
{}\mrightarrow{}  L:(\mBbbZ{}  List)
{}\mrightarrow{}  (\mexists{}fmla':\{mFOL()|  ((mFOL-abstract(fmla')  =  mFOL-abstract(fmla))
                                        \mwedge{}  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla')))\})@i'
4.  TERMOF\{mFOL-bound-rename:o,  1:l,  i:l\}  =  v@i'
\mvdash{}  v  fmla  L  \mmember{}  \{fmla':mFOL()| 
                            (mFOL-abstract(fmla')  =  mFOL-abstract(fmla))  \mwedge{}  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla'))\} 


By

DoSubsume

---

Home Index