Nuprl Lemma : df-program-meaning_wf_null
[A:
']. [B:Type]. df-program-meaning(null-df-program(B)) 
dataflow(A;bag(B)) supposing valueall-type(B)
Proof not projected
Definitions occuring in Statement :
null-df-program: null-df-program(B),
df-program-meaning: df-program-meaning(dfp),
dataflow: dataflow(A;B),
uimplies: b supposing a,
uall: [x:A]. B[x],
member: t T,
universe: Type,
bag: bag(T),
valueall-type: valueall-type(T)
Definitions :
member: t T,
uimplies: b supposing a,
uall: [x:A]. B[x],
implies: P 
Q,
all: x:A. B[x],
prop: 
,
pi1: fst(t),
null-df-program: null-df-program(B),
df-program-type: df-program-type(dfp),
guard: {T}
Lemmas :
valueall-type_wf,
df-program-meaning_wf,
equal_wf,
df-program-type_wf,
dataflow-program_wf,
null-df-program_wf,
bag_wf,
dataflow_wf,
subtype_rel_self
\mforall{}[A:\mBbbU{}']. \mforall{}[B:Type].
df-program-meaning(null-df-program(B)) \mmember{} dataflow(A;bag(B)) supposing valueall-type(B)
Date html generated:
2012_01_23-PM-12_01_05
Last ObjectModification:
2011_12_15-AM-08_39_02
Home
Index