---

consensus-accum-num(num;f;s;r) ==
  let b,n,as,vs,w = s in case r
  of inl(v) => if (n = 0) then <tt, 1, [], [], v> else <ff, n, as, vs, w> fi 
   | inr(z) => let a,i,v = z in 
               if i <z n - 1 then <ff, n, as, vs, w>
               if n - 1 <z i then <tt, i + 1, [a], [v], v>
               else let as' = as @ [a] in
                     let vs' = vs @ [v] in
                     if (||remove-repeats(IdDeq;as')|| = num)
                     then <tt
                          , n + 1
                          , []
                          , []
                          , f values-for-distinct(IdDeq;zip(as';vs'))>
                     else <ff, n, as', vs', w>
                     fi 
               fi 

---

Definitions :  spreadn: let a,b,c,d,e = u in v[a; b; c; d; e],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  spreadn: spread3,  lt_int: i <z j,  subtract: n - m,  let: let,  append: as @ bs,  cons: [car / cdr],  ifthenelse: if b then t else f fi ,  eq_int: (i = j),  length: ||as||,  remove-repeats: remove-repeats(eq;L),  btrue: tt,  add: n + m,  natural_number: $n,  nil: [],  apply: f a,  values-for-distinct: values-for-distinct(eq;L),  id-deq: IdDeq,  zip: zip(as;bs),  bfalse: ff,  pair: <a, b>
FDL editor aliases :  consensus-accum-num

---

consensus-accum-num(num;f;s;r)  ==
    let  b,n,as,vs,w  =  s  in  case  r
    of  inl(v)  =>  if  (n  =\msubz{}  0)  then  <tt,  1,  [],  [],  v>  else  <ff,  n,  as,  vs,  w>  fi 
      |  inr(z)  =>  let  a,i,v  =  z  in 
                              if  i  <z  n  -  1  then  <ff,  n,  as,  vs,  w>
                              if  n  -  1  <z  i  then  <tt,  i  +  1,  [a],  [v],  v>
                              else  let  as'  =  as  @  [a]  in
                                          let  vs'  =  vs  @  [v]  in
                                          if  (||remove-repeats(IdDeq;as')||  =\msubz{}  num)
                                          then  <tt,  n  +  1,  [],  [],  f  values-for-distinct(IdDeq;zip(as';vs'))>
                                          else  <ff,  n,  as',  vs',  w>
                                          fi 
                              fi 


Date html generated: 2010_08_27-AM-12_57_39
Last ObjectModification: 2009_12_23-PM-03_32_40

Home Index