Nuprl Lemma : mFOL-abstract_wf
∀[fmla:mFOL()]. (mFOL-abstract(fmla) ∈ AbstractFOFormula)
Proof
Definitions occuring in Statement :
mFOL-abstract: mFOL-abstract(fmla),
mFOL: mFOL(),
AbstractFOFormula: AbstractFOFormula,
uall: ∀[x:A]. B[x],
member: t ∈ T
Lemmas :
mFOL_ind_wf_simple,
AbstractFOFormula_wf,
AbstractFOAtomic_wf,
list_wf,
FOConnective_wf,
mFOL_wf,
FOQuantifier_wf,
bool_wf
\mforall{}[fmla:mFOL()]. (mFOL-abstract(fmla) \mmember{} AbstractFOFormula)
Date html generated:
2015_07_17-AM-07_54_23
Last ObjectModification:
2015_01_27-AM-10_06_19
Home
Index