---

{ [Info:Type]. [es:EO+(Info)]. [A:Type]. [f:A  ]. [X:EClass(A)].
  [size:]. [num:A  ]. [P:A  ]. [e:E].
    es-collect-filter-max-aux(X;size;v.num[v];v.P[v];v.f[v])(e)
    = <num[X(e)]
      , list-max-aux(v.f[v];mapfilter(e.X(e);
                                      e'.(num[X(e')] = num[X(e)]);
                                      (X)(e)))
      > 
    supposing e  es-collect-filter-max-aux(X;size;v.num[v];v.P[v];v.f[v]) }

{ Proof }

---

Definitions occuring in Statement :  es-collect-filter-max-aux: es-collect-filter-max-aux(X;size;v.num[v];v.P[v];v.f[v]),  es-interface-predecessors: (X)(e),  eclass-val: X(e),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-E: E,  eq_int: (i = j),  assert: b,  bool: ,  nat_plus: ,  nat: ,  uimplies: b supposing a,  uall: [x:A]. B[x],  top: Top,  so_apply: x[s],  set: {x:A| B[x]} ,  lambda: x.A[x],  function: x:A  B[x],  pair: <a, b>,  product: x:A  B[x],  union: left + right,  int: ,  universe: Type,  equal: s = t,  mapfilter: mapfilter(f;P;L),  list-max-aux: list-max-aux(x.f[x];L)
Definitions :  assert: b,  es-collect-filter-max-aux: es-collect-filter-max-aux(X;size;v.num[v];v.P[v];v.f[v]),  so_apply: x[s],  top: Top,  and: P  Q,  implies: P  Q,  member: t  T,  so_lambda: x.t[x],  ifthenelse: if b then t else f fi ,  rev_implies: P  Q,  iff: P  Q,  so_lambda: x y.t[x; y],  all: x:A. B[x],  btrue: tt,  true: True,  prop: ,  nat: ,  uall: [x:A]. B[x],  uiff: uiff(P;Q),  uimplies: b supposing a,  so_apply: x[s1;s2],  es-E-interface: E(X),  sq_type: SQType(T),  guard: {T},  list-max-aux: list-max-aux(x.f[x];L),  has-value: has-value(a),  subtype: S  T
Lemmas :  is-collect-filter-max-aux,  collect-filter-accum-val,  top_wf,  nat_wf,  rational-has-value,  int_inc,  ifthenelse_wf,  lt_int_wf,  pi1_wf_top,  eclass-val_wf,  es-E_wf,  event-ordering+_wf,  list-max-aux_wf,  mapfilter_wf,  es-E-interface_wf,  Id_wf,  es-loc_wf,  es-interface-predecessors_wf,  event-ordering+_inc,  eq_int_wf,  subtype_base_sq,  bool_wf,  bool_subtype_base,  assert_wf,  es-interface-val_wf2,  assert_elim,  in-eclass_wf,  es-collect-filter-max-aux_wf,  es-interface-subtype_rel2,  isl_wf,  nat_plus_wf,  eclass_wf

---

\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[X:EClass(A)].  \mforall{}[size:\mBbbN{}\msupplus{}].  \mforall{}[num:A  {}\mrightarrow{}  \mBbbN{}].
\mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[e:E].
    es-collect-filter-max-aux(X;size;v.num[v];v.P[v];v.f[v])(e)
    =  <num[X(e)],  list-max-aux(v.f[v];mapfilter(\mlambda{}e.X(e);\mlambda{}e'.(num[X(e')]  =\msubz{}  num[X(e)]);\mleq{}(X)(e)))> 
    supposing  \muparrow{}e  \mmember{}\msubb{}  es-collect-filter-max-aux(X;size;v.num[v];v.P[v];v.f[v])


Date html generated: 2011_08_16-PM-05_32_19
Last ObjectModification: 2011_06_20-AM-01_26_31

Home Index