Nuprl Lemma : normal-decl-set_wf
[dd:DeclSet]. (normal-decl-set(dd) 
)
Proof not projected
Definitions occuring in Statement :
normal-decl-set: normal-decl-set(dd),
es-decl-set: DeclSet,
uall: [x:A]. B[x],
prop: ,
member: t T
Definitions :
spreadn: spread3,
normal-decl-set: normal-decl-set(dd),
member: t T,
uall: [x:A]. B[x],
so_lambda: 
x.t[x],
and: P 
Q,
all: x:A. B[x],
prop: ,
true: True,
cand: A c B,
implies: P 
Q,
normal-da: Normal(da),
es-decl-set: DeclSet,
so_apply: x[s]
Lemmas :
es-decl-set_wf,
l_member_wf,
all_wf,
Id_wf,
normal-ds_wf,
hasloc_wf,
assert_wf,
Knd_wf,
fpf_wf
\mforall{}[dd:DeclSet]. (normal-decl-set(dd) \mmember{} \mBbbP{})
Date html generated:
2012_01_23-PM-12_14_13
Last ObjectModification:
2011_12_13-AM-10_34_44
Home
Index