---

{ [A:Type]. [P:A  ]. [ins:A List]. [s:Top].
    (data-stream(buffer-dataflow(s;x.P[x]);ins) 
    ~ map(i.if null(filter(x.P[x];firstn(i;ins)))
             then s
             else last(filter(x.P[x];firstn(i;ins)))
             fi ;upto(||ins||))) }

{ Proof }

---

Definitions occuring in Statement :  buffer-dataflow: buffer-dataflow(s;x.P[x]),  data-stream: data-stream(P;L),  firstn: firstn(n;as),  map: map(f;as),  length: ||as||,  null: null(as),  ifthenelse: if b then t else f fi ,  bool: ,  uall: [x:A]. B[x],  top: Top,  so_apply: x[s],  lambda: x.A[x],  function: x:A  B[x],  list: type List,  universe: Type,  sqequal: s ~ t,  filter: filter(P;l),  last: last(L),  upto: upto(n)
Definitions :  uall: [x:A]. B[x],  top: Top,  buffer-dataflow: buffer-dataflow(s;x.P[x]),  so_apply: x[s],  map: map(f;as),  ifthenelse: if b then t else f fi ,  null: null(as),  filter: filter(P;l),  firstn: firstn(n;as),  upto: upto(n),  length: ||as||,  member: t  T,  ycomb: Y,  lt_int: i <z j,  reduce: reduce(f;k;as),  from-upto: [n, m),  btrue: tt,  bfalse: ff,  pi2: snd(t),  pi1: fst(t),  all: x:A. B[x],  subtype: S  T,  implies: P  Q,  prop: ,  bool: ,  unit: Unit,  iff: P  Q,  and: P  Q,  sq_type: SQType(T),  uimplies: b supposing a,  guard: {T},  int_seg: {i..j},  lelt: i  j < k,  le: A  B,  not: A,  false: False,  it:
Lemmas :  top_wf,  data-stream-cons,  upto_decomp2,  length_wf1,  non_neg_length,  length_wf_nat,  bool_wf,  iff_weakening_uiff,  assert_wf,  eqtt_to_assert,  subtype_base_sq,  int_subtype_base,  upto_wf,  lt_int_wf,  uiff_transitivity,  assert_of_lt_int,  le_wf,  le_int_wf,  bnot_wf,  eqff_to_assert,  assert_functionality_wrt_uiff,  bnot_of_lt_int,  assert_of_le_int,  last-cons,  filter_wf_top,  firstn_wf,  l_member_wf,  not_wf,  assert_of_bnot,  first0

---

\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[ins:A  List].  \mforall{}[s:Top].
    (data-stream(buffer-dataflow(s;x.P[x]);ins)  \msim{}  map(\mlambda{}i.if  null(filter(\mlambda{}x.P[x];firstn(i;ins)))
                                                                                                              then  s
                                                                                                              else  last(filter(\mlambda{}x.P[x];firstn(i;ins)))
                                                                                                              fi  ;upto(||ins||)))


Date html generated: 2011_08_10-AM-08_17_43
Last ObjectModification: 2011_06_18-AM-08_31_23

Home Index