Nuprl Lemma : defined-class_wf
[Info:Type]. [p:eclass-program{i:l}(Info)]. (defined-class(p) 
EClass(eclass-program-type(p)))
Proof not projected
Definitions occuring in Statement :
defined-class: defined-class(prg),
eclass-program-type: eclass-program-type(prg),
eclass-program: eclass-program{i:l}(Info),
eclass: EClass(A[eo; e]),
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
so_lambda: 
x.t[x],
pi1: fst(t),
defined-class: defined-class(prg),
eclass-program-type: eclass-program-type(prg),
member: t T,
uall: [x:A]. B[x],
true: True,
squash: 
T,
implies: P 
Q,
all: x:A. B[x],
prop: 
,
so_apply: x[s],
eclass-program: eclass-program{i:l}(Info),
uimplies: b supposing a,
sq_stable: SqStable(P)
Lemmas :
eclass-program_wf,
Id_wf,
dataflow-set-class_wf,
subtype_rel_bag,
subtype_rel_self,
bag_wf,
dataflow_subtype,
null-df-program_wf,
id-deq_wf,
df-program-type_wf,
dataflow-program_wf,
fpf-cap_wf,
df-program-meaning_wf,
equal_wf,
ext-eq_weakening,
subtype_rel_weakening,
sq_stable__subtype_rel
\mforall{}[Info:Type]. \mforall{}[p:eclass-program\{i:l\}(Info)]. (defined-class(p) \mmember{} EClass(eclass-program-type(p)))
Date html generated:
2012_01_23-PM-12_30_01
Last ObjectModification:
2011_12_14-PM-09_31_23
Home
Index