---

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

---

Definitions :  lambda: x.A[x],  spreadn: spread3,  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,  pair: <a, b>,  natural_number: $n,  inl: inl x ,  bfalse: ff
FDL editor aliases :  collectfilteracc

---

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


Date html generated: 2010_08_27-PM-02_53_35
Last ObjectModification: 2010_03_26-PM-12_10_31

Home Index