---

mlt_inning_step() ==
  s,x.
   let n,vs,i = s in 
   case x
   of inl(v) => s
    | inr(vote) => let m,j,v = vote in 
                   if m <z n then s
                   if (j = i - 1) then <n, [v / vs], i>
                   else s
                   fi 

---

Definitions :  lambda: x.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  spreadn: spread3,  lt_int: i <z j,  ifthenelse: if b then t else f fi ,  eq_int: (i = j),  subtract: n - m,  natural_number: $n,  pair: <a, b>,  cons: [car / cdr]
FDL editor aliases :  mlt_inning_step

---

mlt\_inning\_step()  ==
    \mlambda{}s,x.
      let  n,vs,i  =  s  in 
      case  x
      of  inl(v)  =>  s
        |  inr(vote)  =>  let  m,j,v  =  vote  in 
                                      if  m  <z  n  then  s
                                      if  (j  =\msubz{}  i  -  1)  then  <n,  [v  /  vs],  i>
                                      else  s
                                      fi 


Date html generated: 2010_08_27-PM-08_30_33
Last ObjectModification: 2010_06_23-PM-11_56_57

Home Index