Nuprl Definition : 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 =z 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')|| =z num)
         then <tt, n + 1, [], [], f values-for-distinct(IdDeq;zip(as';vs'))>
         else <ff, n, as', vs', w>
         fi 
   fi 


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 b then t else f fi ,  lt_int: i <z j,  eq_int: (i =z j),  bfalse: ff,  btrue: tt,  let: let,  spreadn: let a,b,c,d,e = u in v[a; b; c; d; e],  spreadn: spread3,  apply: f a,  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  subtract: n - m,  add: n + 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>
                  fi 
      fi 


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

Home Index