Nuprl Lemma : bind-df-program-meaning
[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))
(df-program-meaning(dfpX>>= dfpY) = bind-dataflow(df-program-meaning(dfpX);a.df-program-meaning(dfpY a))))
Proof not projected
Definitions occuring in Statement :
bind-df-program: bind-df-program,
bind-dataflow: bind-dataflow(P;a.Q[a]),
df-program-meaning: df-program-meaning(dfp),
df-program-type: df-program-type(dfp),
dataflow-program: DataflowProgram(A),
dataflow: dataflow(A;B),
subtype_rel: A r B,
uall: [x:A]. B[x],
all: x:A. B[x],
implies: P Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x],
universe: Type,
equal: s = t,
bag: bag(T),
valueall-type: valueall-type(T)
Definitions :
uall: [x:A]. B[x],
implies: P Q,
all: x:A. B[x],
df-program-meaning: df-program-meaning(dfp),
bind-df-program: bind-df-program,
bind-df-program1: bind-df-program1(A;B;dfpX;dfpY),
member: t 
T,
prop: 
,
squash: 
T,
true: True,
spreadn: spread4,
subtype: S T,
so_lambda: 
x.t[x],
pi2: snd(t),
pi1: fst(t),
so_lambda: x y.t[x; y],
suptype: suptype(S; T),
and: P 
Q,
assert: 
b,
isl: isl(x),
outl: outl(x),
btrue: tt,
bfalse: ff,
ifthenelse: if b then t else f fi ,
cand: A c B,
top: Top,
so_apply: x[s],
bind-df-next2: bind-df-next2(F;dfpY;s;m),
bind-df-next3: bind-df-next3(F;dfpY;s;m),
let: let,
bind-nextouts2: bind-nextouts2(L;dfpY;m),
bind-nextouts1: bind-nextouts1(L;dfpY;m),
bag-combine: 
xbs.f[x],
bag-map: bag-map(f;bs),
bag-append: as + bs,
bag-mapfilter: bag-mapfilter(f;P;bs),
bag-union: bag-union(bbs),
map: map(f;as),
append: as @ bs,
bag-filter: [xb|p[x]],
filter: filter(P;l),
reduce: reduce(f;k;as),
ycomb: Y,
concat: concat(ll),
empty-bag: {},
bind-df-next: bind-df-next(F;dfpY;s;m),
bnot: 
b,
not: A,
band: p q,
false: False,
exposed-bfalse: exposed-bfalse,
guard: {T},
bind-df-next1: bind-df-next1(F;dfpY;s;m),
df-program-state: df-program-state(dfp),
df-program-in-state-ap: df-program-in-state-ap(dfp;s;m),
dataflow-program: DataflowProgram(A),
df-program-type: df-program-type(dfp),
uimplies: b supposing a,
so_apply: x[s1;s2],
exists: 
x:A. B[x],
unit: Unit,
bool: 
,
uiff: uiff(P;Q),
cons-bag: x.b,
it: 
,
bag-null: bag-null(bs),
listid: listid(L)
Lemmas :
bind-df-program1-meaning,
equal_wf,
squash_wf,
true_wf,
dataflow_wf,
bag_wf,
subtype_rel_bag,
all_wf,
subtype_rel_wf,
df-program-type_wf,
dataflow-program_wf,
valueall-type_wf,
rec-dataflow-equal,
unit_wf2,
df-program-statetype_wf,
bind-df-next2_wf,
empty-bag_wf,
bind-df-next3_wf,
bag-mapfilter_wf,
isl_wf,
pi1_wf_top,
pi2_wf,
assert_wf,
top_wf,
outl_wf,
false_wf,
and_wf,
bool_wf,
bag_to_squash_list,
bag-combine_wf,
bag-map_wf,
df-program-in-state-ap_wf,
bag-append_wf,
df-program-state_wf,
subtype_rel_simple_product,
bag_qinc,
bind-nextouts1_wf,
bind-nextouts2_wf,
bag-filter-append,
bag-filter_wf,
cons-bag_wf,
bag-map-append,
bind-df-next_wf,
ifthenelse_wf,
not_wf,
equal-empty-bag,
bag-null_wf,
uiff_transitivity,
eqtt_to_assert,
assert-bag-null,
bnot_wf,
eqff_to_assert,
assert_of_bnot,
not_functionality_wrt_uiff,
bind-df-next1_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{} (df-program-meaning(dfpX
>>= dfpY)
= bind-dataflow(df-program-meaning(dfpX);a.df-program-meaning(dfpY a))))
Date html generated:
2012_01_23-PM-12_02_58
Last ObjectModification:
2011_12_31-PM-09_10_26
Home
Index