---

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

---

Definitions :  lambda: x.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  natural_number: $n,  spread: spread def,  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),  pair: <a, b>,  strict-majority-or-max: strict-majority-or-max(L),  cons: [car / cdr],  inl: inl x ,  inr: inr x 
FDL editor aliases :  inning_val

---

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


Date html generated: 2010_08_27-PM-08_30_50
Last ObjectModification: 2010_06_23-PM-11_58_22

Home Index