---

collect_accum(x.num[x];init;a,v.f[a; v];a.P[a]) ==
  s,v.
   let n := num[v] in
   let i,a,w = s in 
   if n <z i then <i, a, inr 0 >
   if i <z n
     then if P[f[init; v]]
          then <n + 1, init, inl f[init; v] >
          else <n, f[init; v], inr 0 >
          fi 
   if P[f[a; v]] then <i + 1, init, inl f[a; v] >
   else <i, f[a; v], inr 0 >
   fi 

---

Definitions :  lambda: x.A[x],  callbyvalue: callbyvalue,  spreadn: spread3,  lt_int: i <z j,  ifthenelse: if b then t else f fi ,  add: n + m,  inl: inl x ,  pair: <a, b>,  inr: inr x ,  natural_number: $n
FDL editor aliases :  collect_accum

---

collect\_accum(x.num[x];init;a,v.f[a;  v];a.P[a])  ==
    \mlambda{}s,v.
      let  n  :=  num[v]  in
      let  i,a,w  =  s  in 
      if  n  <z  i  then  <i,  a,  inr  0  >
      if  i  <z  n
          then  if  P[f[init;  v]]  then  <n  +  1,  init,  inl  f[init;  v]  >  else  <n,  f[init;  v],  inr  0  >  fi 
      if  P[f[a;  v]]  then  <i  +  1,  init,  inl  f[a;  v]  >
      else  <i,  f[a;  v],  inr  0  >
      fi 


Date html generated: 2010_08_27-AM-09_37_39
Last ObjectModification: 2009_12_16-AM-08_39_21

Home Index