Nuprl Lemma : bind-df-program1_wf
[M:Type]. [A,B:{T:Type| valueall-type(T)} ]. [dfpX:DataflowProgram(M)]. [dfpY:A 
DataflowProgram(M)].
((df-program-type(dfpX) 
r A)
(a:A. (df-program-type(dfpY a) r B))
(bind-df-program1(A;B;dfpX;dfpY) 
DataflowProgram(M)))
Proof not projected
Definitions occuring in Statement :
bind-df-program1: bind-df-program1(A;B;dfpX;dfpY),
df-program-type: df-program-type(dfp),
dataflow-program: DataflowProgram(A),
subtype_rel: A r B,
uall: [x:A]. B[x],
all: x:A. B[x],
implies: P Q,
member: t T,
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x],
universe: Type,
valueall-type: valueall-type(T)
Definitions :
uall: [x:A]. B[x],
dataflow-program: DataflowProgram(A),
implies: P Q,
df-program-type: df-program-type(dfp),
all: x:A. B[x],
member: t T,
bind-df-program1: bind-df-program1(A;B;dfpX;dfpY),
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),
and: P 
Q,
uimplies: b supposing a,
so_apply: x[s],
sq_stable: SqStable(P),
guard: {T}
Lemmas :
bind-df-next1_wf,
all_wf,
subtype_rel_wf,
df-program-type_wf,
dataflow-program_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,
subtype_rel_sum,
empty-bag_wf
\mforall{}[M:Type]. \mforall{}[A,B:\{T:Type| valueall-type(T)\} ]. \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{} (bind-df-program1(A;B;dfpX;dfpY) \mmember{} DataflowProgram(M)))
Date html generated:
2012_01_23-PM-12_02_09
Last ObjectModification:
2011_12_19-PM-03_46_25
Home
Index