Nuprl Lemma : bind-df-program1-meaning
[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))
(df-program-meaning(bind-df-program1(A;B;dfpX;dfpY))
= bind-dataflow(df-program-meaning(dfpX);a.df-program-meaning(dfpY a))))
Proof not projected
Definitions occuring in Statement :
bind-df-program1: bind-df-program1(A;B;dfpX;dfpY),
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,
apply: f a,
function: x:A B[x],
universe: Type,
equal: s = t,
bag: bag(T)
Definitions :
uall: [x:A]. B[x],
implies: P Q,
all: x:A. B[x],
df-program-meaning: df-program-meaning(dfp),
bind-df-program1: bind-df-program1(A;B;dfpX;dfpY),
bind-dataflow: bind-dataflow(P;a.Q[a]),
member: t 
T,
spreadn: spread4,
bind-dataflow-aux: bind-dataflow-aux(P;dfs;a.Q[a]),
subtype: S T,
prop: 
,
so_lambda: 
x y.t[x; y],
suptype: suptype(S; T),
so_lambda: x.t[x],
top: Top,
pi1: fst(t),
df-program-statetype: df-program-statetype(dfp),
df-program-type: df-program-type(dfp),
dataflow-program: DataflowProgram(A),
df-program-in-state: df-program-in-state(dfp;s),
pi2: snd(t),
let: let,
and: P 
Q,
rev_implies: P 
Q,
iff: P Q,
squash: 
T,
true: True,
bind-df-next1: bind-df-next1(F;dfpY;s;m),
ifthenelse: if b then t else f fi ,
isl: isl(x),
outl: outl(x),
bind-nextouts1: bind-nextouts1(L;dfpY;m),
btrue: tt,
bag-combine: 
xbs.f[x],
compose: f o g,
null-dataflow: null-dataflow(),
df-program-in-state-ap: df-program-in-state-ap(dfp;s;m),
df-program-state: df-program-state(dfp),
reduce: reduce(f;k;as),
ycomb: Y,
map: map(f;as),
concat: concat(ll),
bag-map: bag-map(f;bs),
bag-union: bag-union(bbs),
empty-bag: {},
bnot: 
b,
bfalse: ff,
append: as @ bs,
bag-append: as + bs,
band: p q,
exposed-bfalse: exposed-bfalse,
assert: 
b,
cand: A c B,
or: P 
Q,
guard: {T},
uimplies: b supposing a,
so_apply: x[s1;s2],
so_apply: x[s],
unit: Unit,
bool: 
,
uiff: uiff(P;Q),
false: False,
sq_type: SQType(T),
bag: bag(T),
nat: 
,
it: 
,
bag-null: bag-null(bs)
Lemmas :
subtype_rel_bag,
rec-dataflow-equal,
bag_wf,
unit_wf2,
df-program-statetype_wf,
dataflow_wf,
bind-df-next1_wf,
empty-bag_wf,
rec-dataflow_wf,
all_wf,
subtype_rel_wf,
df-program-type_wf,
dataflow-program_wf,
dataflow-ap_wf,
let_wf,
bag-map_wf,
pi1_wf_top,
bag-combine_wf,
pi2_wf,
bag-append_wf,
df-program-meaning_wf,
dataflow_subtype,
subtype_rel_self,
df-program-halt-meaning_wf,
df-program-in-state_wf,
null-dataflow_wf,
valueall-type_wf,
equal_wf,
and_wf,
it_wf,
top_wf,
bag-combine-map,
bag-combine-append-left,
true_wf,
squash_wf,
df-program-in-state-ap-property,
bag-map-append,
df-program-state_wf,
df-program-in-state-ap_wf,
bag-union_wf,
bag-map-map,
df-program-halt-meaning-null,
equal-empty-bag,
bag-append-empty,
bag-combine-empty-left,
map_append_sq,
bag-subtype-list,
bind-nextouts1_wf,
null_wf3,
bool_wf,
eqtt_to_assert,
uiff_transitivity,
assert_wf,
bnot_wf,
not_wf,
eqff_to_assert,
assert_of_bnot,
bfalse_wf,
false_wf,
bor_wf,
btrue_wf,
or_wf,
outl_wf,
isl_wf,
bool_cases,
subtype_base_sq,
bool_subtype_base,
assert_of_band,
iff_transitivity,
iff_weakening_uiff,
assert_functionality_wrt_uiff,
bnot_thru_band,
assert_of_bor,
or_functionality_wrt_uiff2,
equals-null-dataflow,
and_functionality_wrt_uiff3,
or_functionality_wrt_uiff,
not_functionality_wrt_uiff,
permutation_wf,
band_wf,
and_functionality_wrt_uiff,
assert_of_null,
bag-null_wf,
and_functionality_wrt_uiff2,
assert-bag-null,
bag-size_wf,
nat_wf,
bag-size-map,
bag-size-append,
bag-size-zero
\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{} (df-program-meaning(bind-df-program1(A;B;dfpX;dfpY))
= bind-dataflow(df-program-meaning(dfpX);a.df-program-meaning(dfpY a))))
Date html generated:
2012_01_23-PM-12_02_32
Last ObjectModification:
2011_12_31-PM-10_03_51
Home
Index