---

es-collect-filter-max-aux(X;size;v.num[v];v.P[v];v.f[v]) ==
  Collect(size v's from X with maximum num[v] such that P[v]
           initialze a:=inr     on each  v set a:=let n := f[v] in
                                                   case a
                                                   of inl(p) => if fst(p) <z n
                                                                then inl <n, v> 
                                                                else a
                                                                fi 
                                                    | inr(q) => inl <n, v> )

---

Definitions :  es-collect-filter-accum: es-collect-filter-accum,  inr: inr x ,  it: ,  callbyvalue: callbyvalue,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  pi1: fst(t),  inl: inl x ,  pair: <a, b>
FDL editor aliases :  es-collect-filter-max-aux

---

es-collect-filter-max-aux(X;size;v.num[v];v.P[v];v.f[v])  ==
    Collect(size  v's  from  X  with  maximum  num[v]  such  that  P[v]    initialze  a:=inr  \mcdot{}   
                      on  each    v  set  a:=let  n  :=  f[v]  in
                                                          case  a
                                                          of  inl(p)  =>  if  fst(p)  <z  n  then  inl  <n,  v>    else  a  fi 
                                                            |  inr(q)  =>  inl  <n,  v>  )


Date html generated: 2010_08_27-PM-03_05_31
Last ObjectModification: 2010_03_31-AM-11_38_45

Home Index