---

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]) ==
  q.let b,n,ok,w = q
     in if ok then {<b, w>} else {} fi   [
  CollectAccum(for v from class X
               do if num[v] increases
                       tr := <0, tt, base>
                  else tr := let n,ok,w = tr in 
                             <n + 1, ok  P[v], f[w; v]>
               until ((fst(tr) = size) ((fst(snd(tr))))) )]

---

Definitions occuring in Statement :  es-collect-accum: es-collect-accum(X;x.num[x];init;a,v.f[a; v];a.P[a]),  es-filter-image: f[X],  eq_int: (i = j),  bor: p q,  band: p  q,  bnot: b,  ifthenelse: if b then t else f fi ,  btrue: tt,  spreadn: spread4,  spreadn: spread3,  pi1: fst(t),  pi2: snd(t),  lambda: x.A[x],  pair: <a, b>,  add: n + m,  natural_number: $n,  single-bag: {x},  empty-bag: {}
Definitions :  es-filter-image: f[X],  lambda: x.A[x],  spreadn: spread4,  ifthenelse: if b then t else f fi ,  single-bag: {x},  empty-bag: {},  es-collect-accum: es-collect-accum(X;x.num[x];init;a,v.f[a; v];a.P[a]),  btrue: tt,  spreadn: spread3,  add: n + m,  natural_number: $n,  pair: <a, b>,  band: p  q,  bor: p q,  eq_int: (i = j),  bnot: b,  pi1: fst(t),  pi2: snd(t)
FDL editor aliases :  es-collect-filter-accum

---

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])  ==
    \mlambda{}q.let  b,n,ok,w  =  q
          in  if  ok  then  \{<b,  w>\}  else  \{\}  fi      [CollectAccum(for  v  from  class  X
                                                                                                              do  if  num[v]  increases
                                                                                                                              tr  :=  ɘ,  tt,  base>
                                                                                                                    else  tr  :=  let  n,ok,w  =  tr  in 
                                                                                                                                          <n  +  1,  ok  \mwedge{}\msubb{}  P[v],  f[w;  v]>
                                                                                                              until  \muparrow{}((fst(tr)  =\msubz{}  size)
                                                                                                              \mvee{}\msubb{}(\mneg{}\msubb{}(fst(snd(tr)))))  )]


Date html generated: 2011_08_16-PM-05_29_48
Last ObjectModification: 2011_01_30-PM-02_39_44

Home Index