---

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

---

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

---

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


Date html generated: 2010_08_27-PM-02_53_50
Last ObjectModification: 2010_03_26-PM-01_33_45

Home Index