Nuprl Lemma : feedback-df-program-meaning
[A:
']. [dfps:DataflowProgram(A) List].
[B:{B:Type| valueall-type(B)} ]. [F:k:
||dfps|| 
bag(df-program-type(dfps[k])) bag(B) bag(B)]. [buf:bag(B)]\000C.
[P:bag(B) 
].
better-feedback-dataflow(||dfps||;
k.map(dfp.df-program-meaning(dfp);dfps)[k];F;buf;x.P[x])
= df-program-meaning(feedback-df-program(B;F;buf;P;dfps))
supposing buf:bag(B). ((F (x.{}) buf) = {})
supposing 0 < ||dfps||
Proof not projected
Definitions occuring in Statement :
feedback-df-program: feedback-df-program(B;F;buf;P;dfps),
df-program-meaning: df-program-meaning(dfp),
df-program-type: df-program-type(dfp),
dataflow-program: DataflowProgram(A),
better-feedback-dataflow: better-feedback-dataflow(n;ds;F;s;x.P[x]),
dataflow: dataflow(A;B),
select: l[i],
map: map(f;as),
length: ||as||,
bool: ,
int_seg: {i..j
},
uimplies: b supposing a,
uall: [x:A]. B[x],
so_apply: x[s],
all: x:A. B[x],
less_than: a < b,
set: {x:A| B[x]} ,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
list: type List,
natural_number: $n,
universe: Type,
equal: s = t,
empty-bag: {},
bag: bag(T),
valueall-type: valueall-type(T)
Definitions :
nat: ,
ge: i 
j ,
bfalse: ff,
tl: tl(l),
hd: hd(l),
eq_int: (i =
j),
lt_int: i <z j,
ifthenelse: if b then t else f fi ,
ycomb: Y,
false: False,
not: 
A,
so_lambda: 
x.t[x],
guard: {T},
le: A 
B,
implies: P 
Q,
member: t 
T,
feedback-df-program: feedback-df-program(B;F;buf;P;dfps),
map: map(f;as),
all: x:A. B[x],
length: ||as||,
uimplies: b supposing a,
uall: [x:A]. B[x],
btrue: tt,
label: ...$L... t,
bnot: 
b,
le_int: i z j,
select: l[i],
and: P 
Q,
lelt: i j < k,
so_apply: x[s1;s2;s3],
int_seg: {i..j},
so_apply: x[s],
prop: 
,
sq_type: SQType(T),
or: P 
Q,
decidable: Dec(P)
Lemmas :
ge_wf,
nat_properties,
le_wf,
less_than_wf,
valueall-type_wf,
bool_wf,
int_seg_wf,
select_wf,
df-program-type_wf,
empty-bag_wf,
equal_wf,
bag_wf,
all_wf,
dataflow-program_wf,
length_wf,
length_wf_nat,
nat_wf,
non_neg_length,
length_cons,
length_wf_nil,
length_nil,
eq_int_wf,
ifthenelse_wf,
int_subtype_base,
subtype_base_sq,
decidable__equal_int,
feedback-df-prog2-meaning,
lelt_wf,
dataflow_wf,
better-feedback-dataflow_wf,
df-program-meaning_wf
\mforall{}[A:\mBbbU{}']. \mforall{}[dfps:DataflowProgram(A) List].
\mforall{}[B:\{B:Type| valueall-type(B)\} ]. \mforall{}[F:k:\mBbbN{}||dfps|| {}\mrightarrow{} bag(df-program-type(dfps[k]))
{}\mrightarrow{} bag(B)
{}\mrightarrow{} bag(B)]. \mforall{}[buf:bag(B)]. \mforall{}[P:bag(B) {}\mrightarrow{} \mBbbB{}].
better-feedback-dataflow(||dfps||;\mlambda{}k.map(\mlambda{}dfp.df-program-meaning(dfp);dfps)[k];F;buf;x.P[x])
= df-program-meaning(feedback-df-program(B;F;buf;P;dfps))
supposing \mforall{}buf:bag(B). ((F (\mlambda{}x.\{\}) buf) = \{\})
supposing 0 < ||dfps||
Date html generated:
2012_01_23-PM-12_00_48
Last ObjectModification:
2011_12_12-PM-06_56_47
Home
Index