Nuprl Definition : pv11_p1_commander_output

pv11_p1_commander_output(Cmd;accpts;reps;mf) ==
  λzm,ldr,z,waitfor. let bnum,slt,cmd = zm in 
                    let acloc,b,s,b' = z 
                    in if (pv11_p1_eq_bnums() bnum b) ∧b (slt =z s)
                       then if pv11_p1_eq_bnums() bnum b'
                            then if #(waitfor) <z pv11_p1_threshold(accpts)
                                 then pv11_p1_decision'broadcast(Cmd;mf) reps <slt, cmd>
                                 else {}
                                 fi 
                            else {pv11_p1_preempted'send(Cmd;mf) ldr b'}
                            fi 
                       else {}
                       fi   


Definitions occuring in Statement :  pv11_p1_decision'broadcast: pv11_p1_decision'broadcast(Cmd;mf),  pv11_p1_preempted'send: pv11_p1_preempted'send(Cmd;mf),  pv11_p1_threshold: pv11_p1_threshold(accpts),  pv11_p1_eq_bnums: pv11_p1_eq_bnums(),  band: p ∧b q,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  eq_int: (i =z j),  spreadn: spread4,  spreadn: spread3,  apply: f a,  lambda: λx.A[x],  pair: <a, b>,  bag-size: #(bs),  single-bag: {x},  empty-bag: {}
FDL editor aliases :  pv11_p1_commander_output
Latex:
pv11\_p1\_commander\_output(Cmd;accpts;reps;mf)  ==
    \mlambda{}zm,ldr,z,waitfor.  let  bnum,slt,cmd  =  zm  in 
                                        let  acloc,b,s,b'  =  z 
                                        in  if  (pv11\_p1\_eq\_bnums()  bnum  b)  \mwedge{}\msubb{}  (slt  =\msubz{}  s)
                                              then  if  pv11\_p1\_eq\_bnums()  bnum  b'
                                                        then  if  \#(waitfor)  <z  pv11\_p1\_threshold(accpts)
                                                                  then  pv11\_p1\_decision'broadcast(Cmd;mf)  reps  <slt,  cmd>
                                                                  else  \{\}
                                                                  fi 
                                                        else  \{pv11\_p1\_preempted'send(Cmd;mf)  ldr  b'\}
                                                        fi 
                                              else  \{\}
                                              fi     


Date html generated: 2015_07_23-PM-04_31_58
Last ObjectModification: 2014_11_26-AM-11_27_09

Home Index