---

{ [A,B:Type]. [ins:A List]. [P:dataflow(A;bag(B))].
    (last(data-stream(delay-dataflow(P);ins)) 
    ~ let ins' = firstn(||ins|| - 1;ins) in
          if null(filter(x.0 <z bag-size(x);data-stream(P;ins')))
          then {}
          else last(filter(x.0 <z bag-size(x);data-stream(P;ins')))
          fi ) }

{ Proof }

---

Definitions occuring in Statement :  delay-dataflow: delay-dataflow(P),  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 :  Error :empty-bag_wf,  last-delay-data-stream1,  listp_wf,  Error :bag_wf,  dataflow_wf,  subtype_base_sq,  last_wf,  data-stream_wf,  delay-dataflow_wf

---

\mforall{}[A,B:Type].  \mforall{}[ins:A  List\msupplus{}].  \mforall{}[P:dataflow(A;bag(B))].
    (last(data-stream(delay-dataflow(P);ins))  \msim{}  let  ins'  =  firstn(||ins||  -  1;ins)  in
                                                                                                    if  null(filter(\mlambda{}x.0  <z  bag-size(x);
                                                                                                                                  data-stream(P;ins')))
                                                                                                    then  \{\}
                                                                                                    else  last(filter(\mlambda{}x.0  <z  bag-size(x);
                                                                                                                                      data-stream(P;ins')))
                                                                                                    fi  )


Date html generated: 2011_08_10-AM-08_18_22
Last ObjectModification: 2011_06_29-PM-03_56_10

Home Index