---

mlt_inning_val() ==
  z.let s,x = z in
       let n,vs,i = s in 
      case x
      of inl(v) => inl inl <n, 0, v>  
       | inr(vote) => let m,j,v = vote in 
                      if n <z m then inl inl vote  
                      if i z j then inl inl vote  
                      if (xvs.(x = v))_b
                        then inl inl <n, i, strict-majority-or-max([v / vs])>  
                      else inl (inr <n, v> ) 
                      fi 

---

Definitions :  lambda: x.A[x],  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  natural_number: $n,  spreadn: spread3,  lt_int: i <z j,  le_int: i z j,  ifthenelse: if b then t else f fi ,  bl-exists: (xL.P[x])_b,  bnot: b,  eq_int: (i = j),  strict-majority-or-max: strict-majority-or-max(L),  cons: [car / cdr],  inl: inl x ,  inr: inr x ,  pair: <a, b>
FDL editor aliases :  mlt_inning_val

---

mlt\_inning\_val()  ==
    \mlambda{}z.let  s,x  =  z  in
              let  n,vs,i  =  s  in 
            case  x
            of  inl(v)  =>  inl  inl  <n,  0,  v>   
              |  inr(vote)  =>  let  m,j,v  =  vote  in 
                                            if  n  <z  m  then  inl  inl  vote   
                                            if  i  \mleq{}z  j  then  inl  inl  vote   
                                            if  (\mexists{}x\mmember{}vs.\mneg{}\msubb{}(x  =\msubz{}  v))\_b
                                                then  inl  inl  <n,  i,  strict-majority-or-max([v  /  vs])>   
                                            else  inl  (inr  <n,  v>  ) 
                                            fi 


Date html generated: 2010_08_27-PM-08_30_55
Last ObjectModification: 2010_06_23-PM-11_58_45

Home Index