Nuprl Definition : consensus-accum-num

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

Definitions occuring in Statement :  id-deq: IdDeq values-for-distinct: values-for-distinct(eq;L) remove-repeats: remove-repeats(eq;L) zip: zip(as;bs) length: ||as|| append: as bs cons: [a b] nil: [] ifthenelse: if then else fi  lt_int: i <j eq_int: (i =z j) bfalse: ff btrue: tt let: let spreadn: let a,b,c,d,e in v[a; b; c; d; e] spreadn: spread3 apply: a pair: <a, b> decide: case of inl(x) => s[x] inr(y) => t[y] subtract: m add: m natural_number: $n
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>

Date html generated: 2015_07_17-AM-11_48_46
Last ObjectModification: 2012_02_25-AM-11_49_58

Home Index