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