Nuprl Lemma : defunct-delay-program_wf
[Info:
']. [P:eclass-program{i:l}(Info)]. (defunct-delay-program(P) 
eclass-program{i:l}(Info))
Proof not projected
Definitions occuring in Statement :
defunct-delay-program: defunct-delay-program(P),
eclass-program: eclass-program{i:l}(Info),
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
uall: [x:A]. B[x],
eclass-program: eclass-program{i:l}(Info),
member: t T,
defunct-delay-program: defunct-delay-program(P),
so_lambda: 
x.t[x],
df-program-type: df-program-type(dfp),
delay-df-program: delay-df-program(dfp),
pi1: fst(t),
spreadn: spread4,
so_apply: x[s],
dataflow-program: DataflowProgram(A)
Lemmas :
fpf-compose_wf,
fpf_wf,
dataflow-program_wf,
df-program-type_wf,
eclass-program_wf,
delay-df-program_wf
\mforall{}[Info:\mBbbU{}']. \mforall{}[P:eclass-program\{i:l\}(Info)]. (defunct-delay-program(P) \mmember{} eclass-program\{i:l\}(Info))
Date html generated:
2012_01_23-PM-12_34_58
Last ObjectModification:
2012_01_04-PM-01_22_28
Home
Index