Nuprl Lemma : null-df-program_wf
[A:
']. [B:Type]. null-df-program(B) 
{dfp:DataflowProgram(A)| df-program-type(dfp) = B} supposing valueall-type(B)
Proof not projected
Definitions occuring in Statement :
null-df-program: null-df-program(B),
df-program-type: df-program-type(dfp),
dataflow-program: DataflowProgram(A),
uimplies: b supposing a,
uall: [x:A]. B[x],
member: t T,
set: {x:A| B[x]} ,
universe: Type,
equal: s = t,
valueall-type: valueall-type(T)
Definitions :
member: t T,
uimplies: b supposing a,
uall: [x:A]. B[x],
unit: Unit,
null-df-program: null-df-program(B),
dataflow-program: DataflowProgram(A),
pi1: fst(t),
df-program-type: df-program-type(dfp)
Lemmas :
valueall-type_wf,
df-program-type_wf,
bag_wf,
empty-bag_wf,
it_wf,
equal-valueall-type,
unit_wf2
\mforall{}[A:\mBbbU{}']. \mforall{}[B:Type].
null-df-program(B) \mmember{} \{dfp:DataflowProgram(A)| df-program-type(dfp) = B\} supposing valueall-type(B\000C)
Date html generated:
2012_01_23-PM-12_01_01
Last ObjectModification:
2011_12_14-AM-09_19_58
Home
Index