---

Collect(size v's from X with maximum num[v] such that P[v]) ==
  tr.let b,v,ok = tr in 
      if ok then {b} else {} fi [CollectAccum(for v from class X
                                              do if num[v] increases
                                                      p := <0, tt>
                                                 else p := let n,ok = p 
                                                           in <n + 1
                                                              , ok  P[v]
                                                              >
                                              until ((fst(p) = size)
                                              ((snd(p)))) )]

---

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: spread3,  pi1: fst(t),  pi2: snd(t),  lambda: x.A[x],  spread: spread def,  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: spread3,  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,  spread: spread def,  pair: <a, b>,  add: n + m,  natural_number: $n,  band: p  q,  bor: p q,  eq_int: (i = j),  pi1: fst(t),  bnot: b,  pi2: snd(t)
FDL editor aliases :  es-collect-filter

---

Collect(size  v's  from  X  with  maximum  num[v]  such  that  P[v])  ==
    \mlambda{}tr.let  b,v,ok  =  tr  in 
            if  ok  then  \{b\}  else  \{\}  fi  [CollectAccum(for  v  from  class  X
                                                                                            do  if  num[v]  increases
                                                                                                            p  :=  ɘ,  tt>
                                                                                                  else  p  :=  let  n,ok  =  p 
                                                                                                                      in  <n  +  1,  ok  \mwedge{}\msubb{}  P[v]>
                                                                                            until  \muparrow{}((fst(p)  =\msubz{}  size)  \mvee{}\msubb{}(\mneg{}\msubb{}(snd(p))))  )]


Date html generated: 2011_08_16-PM-05_28_31
Last ObjectModification: 2011_01_16-PM-08_23_09

Home Index