---

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


1. fmla : mFOL()
2. L : ℤ List
3. v : ∀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')))])
4. TERMOF{FOL-bound-rename:o, 1:l, i:l}
= v
∈ (∀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')))]))
⊢ v fmla L ∈ {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
{ (Unfold `all` (-2) THEN DoSubsume) }

1
1. fmla : mFOL()
2. L : ℤ List
3. v : 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')))])
4. TERMOF{FOL-bound-rename:o, 1:l, i:l}
= v
∈ (∀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')))]))
⊢ v fmla L ∈ ∃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')))]

2
1. fmla : mFOL()
2. L : ℤ List
3. v : 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')))])
4. TERMOF{FOL-bound-rename:o, 1:l, i:l}
= v
∈ (∀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')))]))
5. (v fmla L)
= (v fmla L)
∈ (∃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')))])
⊢ (∃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')))]) ⊆r {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'))} 

---

Latex:

---

Latex:

1.  fmla  :  mFOL()
2.  L  :  \mBbbZ{}  List
3.  v  :  \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')))])
4.  TERMOF\{FOL-bound-rename:o,  1:l,  i:l\}  =  v
\mvdash{}  v  fmla  L  \mmember{}  \{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:
(Unfold  `all`  (-2)  THEN  DoSubsume)

---

Home Index