---

{ [L:Top List]. [P:Top].
    (last(data-stream(P;L)) ~ if null(L)
    then []
    else snd(P*(firstn(||L|| - 1;L))(last(L)))
    fi ) }

{ Proof }

---

Definitions occuring in Statement :  data-stream: data-stream(P;L),  iterate-dataflow: P*(inputs),  dataflow-ap: df(a),  firstn: firstn(n;as),  length: ||as||,  null: null(as),  ifthenelse: if b then t else f fi ,  uall: [x:A]. B[x],  top: Top,  pi2: snd(t),  nil: [],  list: type List,  subtract: n - m,  natural_number: $n,  sqequal: s ~ t,  last: last(L)
Definitions :  uall: [x:A]. B[x],  ifthenelse: if b then t else f fi ,  member: t  T,  all: x:A. B[x],  implies: P  Q,  btrue: tt,  prop: ,  bfalse: ff,  last: last(L),  select: l[i],  false: False,  length: ||as||,  ycomb: Y,  bool: ,  unit: Unit,  iff: P  Q,  and: P  Q,  not: A,  le: A  B,  uimplies: b supposing a,  it:
Lemmas :  null_wf3,  bool_wf,  iff_weakening_uiff,  uiff_transitivity,  assert_wf,  eqtt_to_assert,  assert_of_null,  not_wf,  bnot_wf,  eqff_to_assert,  assert_of_bnot,  not_functionality_wrt_uiff,  top_wf,  select-data-stream,  length-data-stream,  lt_int_wf,  length_wf1,  assert_of_lt_int,  le_wf,  le_int_wf,  assert_functionality_wrt_uiff,  bnot_of_lt_int,  assert_of_le_int,  non_neg_length,  length_wf_nat

---

\mforall{}[L:Top  List].  \mforall{}[P:Top].
    (last(data-stream(P;L))  \msim{}  if  null(L)  then  []  else  snd(P*(firstn(||L||  -  1;L))(last(L)))  fi  )


Date html generated: 2011_08_10-AM-08_14_58
Last ObjectModification: 2011_06_18-AM-08_30_17

Home Index