{ 
[A,B:Type]. [ins:A List
]. [P:dataflow(A;bag(B))]. [init:bag(B)].
(last(data-stream(seq-dataflow(P;buffer-dataflow(init;x.0 <z ...));ins))
~ let ins' = firstn(||ins|| - 1;ins) in
if null(filter(
x.0 <z bag-size(x);data-stream(P;ins')))
then init
else last(filter(x.0 <z bag-size(x);data-stream(P;ins')))
fi ) }
{ Proof }
Definitions occuring in Statement :
buffer-dataflow: buffer-dataflow(s;x.P[x]),
seq-dataflow: seq-dataflow(P;Q),
data-stream: data-stream(P;L),
dataflow: dataflow(A;B),
firstn: firstn(n;as),
length: ||as||,
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],
subtract: n - m,
natural_number: $n,
universe: Type,
sqequal: s ~ t,
filter: filter(P;l),
listp: A List,
last: last(L)
Lemmas :
bnot_wf,
le_int_wf,
assert_of_le_int,
bnot_of_lt_int,
assert_functionality_wrt_uiff,
eqff_to_assert,
assert_wf,
assert_of_lt_int,
eqtt_to_assert,
uiff_transitivity,
bool_wf,
lt_int_wf,
select-from-upto,
from-upto_wf,
length-from-upto,
firstn-data-stream,
int_subtype_base,
set_subtype_base,
dataflow_wf,
listp_wf,
delay-data-stream1,
upto_decomp2,
nat_plus_wf,
subtype_rel_wf,
listp_properties,
length_wf_nat,
nat_wf,
le_wf,
not_wf,
false_wf,
last-map,
member_wf,
length_wf1,
top_wf,
int_seg_wf,
data-stream_wf,
firstn_wf,
filter_wf,
last_wf,
ifthenelse_wf,
Error :bag_wf,
subtype_base_sq,
upto_wf
\mforall{}[A,B:Type]. \mforall{}[ins:A List\msupplus{}]. \mforall{}[P:dataflow(A;bag(B))]. \mforall{}[init:bag(B)].
(last(data-stream(seq-dataflow(P;buffer-dataflow(init;x.0 <z bag-size(x)));ins))
\msim{} let ins' = firstn(||ins|| - 1;ins) in
if null(filter(\mlambda{}x.0 <z bag-size(x);data-stream(P;ins')))
then init
else last(filter(\mlambda{}x.0 <z bag-size(x);data-stream(P;ins')))
fi )
Date html generated:
2011_08_10-AM-08_18_19
Last ObjectModification:
2011_06_29-PM-03_55_25
Home
Index