---

collect_filter_accum_fun(b,v.f[b; v];base;size;v.num[v];v.P[v]) ==
  s,v.
   let n := num[v] in
   let vok := P[v] in
     let i,m,b,w = s in if n <z i then <i, m, b, inr 0 >
        if vok
          then if i <z n
               then if (1 = size)
                    then <n + 1, 0, f[base; v], inl tt >
                    else <n, 1, f[base; v], inr 0 >
                    fi 
               else let m' := m + 1 in
                    if (m' = size)
                    then <i + 1, 0, f[base; v], inl tt >
                    else <i, m', f[b; v], inr 0 >
                    fi 
               fi 
        if i <z n then <n + 1, 0, f[base; v], inl ff >
        else <i + 1, 0, f[b; v], inl ff >
        fi  

---

Definitions :  lambda: x.A[x],  spreadn: let w,x,y,z = a in t[w; x; y; z] ,  callbyvalue: callbyvalue,  eq_int: (i = j),  btrue: tt,  inr: inr x ,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  add: n + m,  natural_number: $n,  pair: <a, b>,  inl: inl x ,  bfalse: ff
FDL editor aliases :  collect_filter_accum_fun

---

collect\_filter\_accum\_fun(b,v.f[b;  v];base;size;v.num[v];v.P[v])  ==
    \mlambda{}s,v.
      let  n  :=  num[v]  in
      let  vok  :=  P[v]  in
          let  i,m,b,w  =  s  in  if  n  <z  i  then  <i,  m,  b,  inr  0  >
                if  vok
                    then  if  i  <z  n
                              then  if  (1  =\msubz{}  size)
                                        then  <n  +  1,  0,  f[base;  v],  inl  tt  >
                                        else  <n,  1,  f[base;  v],  inr  0  >
                                        fi 
                              else  let  m'  :=  m  +  1  in
                                        if  (m'  =\msubz{}  size)
                                        then  <i  +  1,  0,  f[base;  v],  inl  tt  >
                                        else  <i,  m',  f[b;  v],  inr  0  >
                                        fi 
                              fi 
                if  i  <z  n  then  <n  +  1,  0,  f[base;  v],  inl  ff  >
                else  <i  +  1,  0,  f[b;  v],  inl  ff  >
                fi   


Date html generated: 2010_08_27-AM-09_38_00
Last ObjectModification: 2009_12_16-AM-08_40_10

Home Index