Nuprl Lemma : bind-df-program_wf
[M,A,B:Type].
[dfpX:DataflowProgram(M)]. [dfpY:A 
DataflowProgram(M)].
((df-program-type(dfpX) 
r A) 
(a:A. (df-program-type(dfpY a) r B)) (dfpX>>= dfpY 
DataflowProgram(M)))
supposing valueall-type(A) 
valueall-type(B)
Proof not projected
Definitions occuring in Statement :
bind-df-program: bind-df-program,
df-program-type: df-program-type(dfp),
dataflow-program: DataflowProgram(A),
subtype_rel: A r B,
uimplies: b supposing a,
uall: [x:A]. B[x],
all: x:A. B[x],
implies: P Q,
and: P Q,
member: t T,
apply: f a,
function: x:A B[x],
universe: Type,
valueall-type: valueall-type(T)
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
and: P Q,
dataflow-program: DataflowProgram(A),
implies: P Q,
df-program-type: df-program-type(dfp),
all: x:A. B[x],
member: t T,
bind-df-program: bind-df-program,
spreadn: spread4,
unit: Unit,
pi1: fst(t),
pi2: snd(t),
df-program-statetype: df-program-statetype(dfp),
prop: 
,
so_lambda: 
x.t[x],
top: Top,
subtype: S T,
squash: 
T,
true: True,
suptype: suptype(S; T),
so_apply: x[s],
sq_stable: SqStable(P),
guard: {T}
Lemmas :
evalall_wf,
empty-bag_wf,
bind-df-next_wf,
all_wf,
subtype_rel_wf,
df-program-type_wf,
dataflow-program_wf,
and_wf,
valueall-type_wf,
unit_wf2,
bag_wf,
pi1_wf_top,
product-valueall-type,
union-valueall-type,
sq_stable__valueall-type,
equal-valueall-type,
bag-valueall-type,
subtype_rel_bag,
subtype_rel_transitivity,
subtype_rel_simple_product,
df-program-statetype_wf,
subtype_rel_self,
subtype_rel_product
\mforall{}[M,A,B:Type].
\mforall{}[dfpX:DataflowProgram(M)]. \mforall{}[dfpY:A {}\mrightarrow{} DataflowProgram(M)].
((df-program-type(dfpX) \msubseteq{}r A)
{}\mRightarrow{} (\mforall{}a:A. (df-program-type(dfpY a) \msubseteq{}r B))
{}\mRightarrow{} (dfpX
>>= dfpY \mmember{} DataflowProgram(M)))
supposing valueall-type(A) \mwedge{} valueall-type(B)
Date html generated:
2012_01_23-PM-12_02_39
Last ObjectModification:
2011_12_12-AM-08_25_34
Home
Index