{ 
[A,B:Type]. [ins:A List]. [P:dataflow(A;bag(B))].
(delay-dataflow(P)*(ins)
~ seq-dataflow(P*(ins);let ins' = filter(
x.0 <z bag-size(x);
data-stream(P;ins)) in
buffer-dataflow(if null(ins')
then {}
else last(ins')
fi ;x.0 <z bag-size(x)))) }
{ Proof }
Definitions occuring in Statement :
delay-dataflow: delay-dataflow(P),
buffer-dataflow: buffer-dataflow(s;x.P[x]),
seq-dataflow: seq-dataflow(P;Q),
data-stream: data-stream(P;L),
iterate-dataflow: P*(inputs),
dataflow: dataflow(A;B),
null: null(as),
lt_int: i <z j,
ifthenelse: if b then t else f fi ,
let: let,
uall: [x:A]. B[x],
lambda: x.A[x],
list: type List,
natural_number: $n,
universe: Type,
sqequal: s ~ t,
filter: filter(P;l),
last: last(L)
Definitions :
function: x:A 
B[x],
all: x:A. B[x],
equal: s = t,
delay-dataflow: delay-dataflow(P),
bag: Error :bag,
universe: Type,
sqequal: s ~ t,
list: type List,
uall: [x:A]. B[x],
isect: 
x:A. B[x],
member: t 
T,
dataflow: dataflow(A;B),
void: Void,
top: Top,
set: {x:A| B[x]} ,
real: 
,
grp_car: |g|,
subtype: S 
T,
int: 
,
nat: 
,
let: let,
apply: f a,
filter: filter(P;l),
lambda: x.A[x],
ifthenelse: if b then t else f fi ,
null: null(as),
empty-bag: Error :empty-bag,
last: last(L),
lt_int: i <z j,
natural_number: $n,
bag-size: Error :bag-size,
data-stream: data-stream(P;L),
so_lambda: 
x.t[x],
iterate-dataflow: P*(inputs),
seq-dataflow: seq-dataflow(P;Q),
buffer-dataflow: buffer-dataflow(s;x.P[x])
Lemmas :
iterate-seq-dataflow,
iterate-buffer-dataflow,
buffer-dataflow_wf,
lt_int_wf,
Error :bag-size_wf,
nat_wf,
Error :empty-bag_wf,
data-stream_wf,
dataflow_wf,
Error :bag_wf
\mforall{}[A,B:Type]. \mforall{}[ins:A List]. \mforall{}[P:dataflow(A;bag(B))].
(delay-dataflow(P)*(ins)
\msim{} seq-dataflow(P*(ins);let ins' = filter(\mlambda{}x.0 <z bag-size(x);data-stream(P;ins)) in
buffer-dataflow(if null(ins')
then \{\}
else last(ins')
fi ;x.0 <z bag-size(x))))
Date html generated:
2011_08_10-AM-08_18_09
Last ObjectModification:
2011_06_18-AM-08_31_30
Home
Index