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: T List,
all: ∀x:A. B[x],
and: P ∧ Q,
member: t ∈ T,
set: {x:A| B[x]} ,
int: ℤ,
equal: s = 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