Nuprl Definition : ohc_v1_roundout1

ohc_v1_roundout1(Cmd;cmdeq;flrs) ==
  loc,zf.
   let zg,sender = zf 
   in let zh,c = zg 
      in let n,i = zh 
         in z.let cmds,z = z 
               in if (||cmds|| = flrs + 1)
                  then let k,x = poss-maj(cmdeq;[c / cmds];c) 
                       in if (k = flrs + 1) then {<inl x , x>} else {<inr  , x>} fi 
                  else {}
                  fi 


Definitions occuring in Statement :  length: ||as||,  eq_int: (i = j),  ifthenelse: if b then t else f fi ,  it: ,  lambda: x.A[x],  spread: spread def,  pair: <a, b>,  inr: inr x ,  inl: inl x ,  cons: [car / cdr],  add: n + m,  natural_number: $n,  poss-maj: poss-maj(eq;L;x),  single-bag: {x},  empty-bag: {}
FDL editor aliases :  ohc_v1_roundout1 ohc_v1_roundout1
ohc\_v1\_roundout1(Cmd;cmdeq;flrs)  ==
    \mlambda{}loc,zf.
      let  zg,sender  =  zf 
      in  let  zh,c  =  zg 
            in  let  n,i  =  zh 
                  in  \mlambda{}z.let  cmds,z  =  z 
                              in  if  (||cmds||  =\msubz{}  flrs  +  1)
                                    then  let  k,x  =  poss-maj(cmdeq;[c  /  cmds];c) 
                                              in  if  (k  =\msubz{}  flrs  +  1)  then  \{<inl  x  ,  x>\}  else  \{<inr  \mcdot{}  ,  x>\}  fi 
                                    else  \{\}
                                    fi 


Date html generated: 2012_02_20-PM-05_21_26
Last ObjectModification: 2012_02_13-PM-12_55_27

Home Index