Nuprl Lemma : mFOL-rename-bound-to-avoid_wf

fmla:mFOL(). ∀L:ℤ List.
  (mFOL-rename-bound-to-avoid(fmla;L) ∈ {fmla':mFOL()| 
                                         (mFOL-abstract(fmla') mFOL-abstract(fmla) ∈ AbstractFOFormula)
                                         ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla'))} )


Proof




Definitions occuring in Statement :  mFOL-rename-bound-to-avoid: mFOL-rename-bound-to-avoid(fmla;L) mFOL-abstract: mFOL-abstract(fmla) mFOL-boundvars: mFOL-boundvars(fmla) mFOL: mFOL() AbstractFOFormula: AbstractFOFormula l_disjoint: l_disjoint(T;l1;l2) list: List all: x:A. B[x] and: P ∧ Q member: t ∈ T set: {x:A| B[x]}  int: equal: t ∈ T
Lemmas :  lifting-strict-spread has-value_wf_base base_wf is-exception_wf lifting-strict-decide top_wf mFOL-boundvars_wf l_disjoint_wf mFOL-abstract_wf AbstractFOFormula_wf sq_exists_wf list_wf mFOL_wf all_wf sq_exists_subtype_rel subtype_rel_self
\mforall{}fmla:mFOL().  \mforall{}L:\mBbbZ{}  List.
    (mFOL-rename-bound-to-avoid(fmla;L)  \mmember{}  \{fmla':mFOL()| 
                                                                                  (mFOL-abstract(fmla')  =  mFOL-abstract(fmla))
                                                                                  \mwedge{}  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla'))\}  )



Date html generated: 2015_07_17-AM-07_54_38
Last ObjectModification: 2015_06_19-PM-01_31_27

Home Index