---

{ [Info,A,B:Type]. [base:B]. [f:B  A  B]. [X:EClass(A)]. [size:].
  [num:A  ]. [P:A  ].
    (Collect(size v's from X with maximum num[v] such that P[v]
              initialze x:=base   on each  v set x:=f[x;v])  EClass(  B)) }

{ Proof }

---

Definitions occuring in Statement :  es-collect-filter-accum: es-collect-filter-accum,  eclass: EClass(A[eo; e]),  bool: ,  nat_plus: ,  nat: ,  uall: [x:A]. B[x],  so_apply: x[s1;s2],  so_apply: x[s],  member: t  T,  function: x:A  B[x],  product: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  member: t  T,  es-collect-filter-accum: es-collect-filter-accum,  so_apply: x[s],  so_apply: x[s1;s2],  spreadn: spread4,  spreadn: spread3,  top: Top,  so_lambda: x.t[x],  all: x:A. B[x],  subtype: S  T,  so_lambda: x y.t[x; y],  nat_plus:
Lemmas :  es-filter-image_wf,  nat_wf,  bool_wf,  ifthenelse_wf,  top_wf,  es-collect-accum_wf,  bor_wf,  eq_int_wf,  pi1_wf_top,  bnot_wf,  pi2_wf,  btrue_wf,  band_wf,  nat_plus_wf,  eclass_wf,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf

---

\mforall{}[Info,A,B:Type].  \mforall{}[base:B].  \mforall{}[f:B  {}\mrightarrow{}  A  {}\mrightarrow{}  B].  \mforall{}[X:EClass(A)].  \mforall{}[size:\mBbbN{}\msupplus{}].  \mforall{}[num:A  {}\mrightarrow{}  \mBbbN{}].
\mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].
    (Collect(size  v's  from  X  with  maximum  num[v]  such  that  P[v]    initialze  x:=base 
                        on  each    v  set  x:=f[x;v])  \mmember{}  EClass(\mBbbN{}  \mtimes{}  B))


Date html generated: 2011_08_16-PM-05_29_56
Last ObjectModification: 2011_06_20-AM-01_24_56

Home Index