---

{ [A:Type]. [P:A  ]. [ins:A List]. [s:Top].
    (buffer-dataflow(s;x.P[x])*(ins) ~ let ins' = filter(x.P[x];ins) in
                                           buffer-dataflow(if null(ins')
                                           then s
                                           else last(ins')
                                           fi ;x.P[x])) }

{ Proof }

---

Definitions occuring in Statement :  buffer-dataflow: buffer-dataflow(s;x.P[x]),  iterate-dataflow: P*(inputs),  null: null(as),  ifthenelse: if b then t else f fi ,  bool: ,  let: let,  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)
Definitions :  uall: [x:A]. B[x],  let: let,  filter: filter(P;l),  ifthenelse: if b then t else f fi ,  null: null(as),  member: t  T,  reduce: reduce(f;k;as),  btrue: tt,  top: Top,  buffer-dataflow: buffer-dataflow(s;x.P[x]),  so_apply: x[s],  pi1: fst(t),  all: x:A. B[x],  implies: P  Q,  prop: ,  bfalse: ff,  subtype: S  T,  bool: ,  unit: Unit,  iff: P  Q,  and: P  Q,  it:
Lemmas :  top_wf,  bool_wf,  iff_weakening_uiff,  assert_wf,  eqtt_to_assert,  not_wf,  uiff_transitivity,  bnot_wf,  eqff_to_assert,  assert_of_bnot,  filter_wf,  last-cons

---

\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[ins:A  List].  \mforall{}[s:Top].
    (buffer-dataflow(s;x.P[x])*(ins)  \msim{}  let  ins'  =  filter(\mlambda{}x.P[x];ins)  in
                                                                                  buffer-dataflow(if  null(ins')
                                                                                  then  s
                                                                                  else  last(ins')
                                                                                  fi  ;x.P[x]))


Date html generated: 2011_08_10-AM-08_17_36
Last ObjectModification: 2011_06_18-AM-08_31_20

Home Index