Nuprl Definition : pv11_p1_AcceptorsP2a
pv11_p1_AcceptorsP2a(Cmd;ldrs_uid;mf) ==
  let f = λloc,zj,z. let ldr,zk = zj 
                     in let b,s,zl = zk in 
                        let bnum,z = z 
                        in {pv11_p1_p2b'send(Cmd;mf) ldr <loc, b, s, bnum>} in
      ((f o pv11_p1_p2a'base(Cmd;mf)) o pv11_p1_AcceptorState(Cmd;ldrs_uid;mf))
Definitions occuring in Statement : 
pv11_p1_AcceptorState: pv11_p1_AcceptorState(Cmd;ldrs_uid;mf)
, 
pv11_p1_p2b'send: pv11_p1_p2b'send(Cmd;mf)
, 
pv11_p1_p2a'base: pv11_p1_p2a'base(Cmd;mf)
, 
eclass2: (X o Y)
, 
eclass1: (f o X)
, 
let: let, 
spreadn: spread3, 
apply: f a
, 
lambda: λx.A[x]
, 
spread: spread def, 
pair: <a, b>
, 
single-bag: {x}
FDL editor aliases : 
pv11_p1_AcceptorsP2a
Latex:
pv11\_p1\_AcceptorsP2a(Cmd;ldrs$_{uid}$;mf)  ==
    let  f  =  \mlambda{}loc,zj,z.  let  ldr,zk  =  zj 
                                          in  let  b,s,zl  =  zk  in 
                                                let  bnum,z  =  z 
                                                in  \{pv11\_p1\_p2b'send(Cmd;mf)  ldr  <loc,  b,  s,  bnum>\}  in
            ((f  o  pv11\_p1\_p2a'base(Cmd;mf))  o  pv11\_p1\_AcceptorState(Cmd;ldrs$_{uid}$;m\000Cf))
Date html generated:
2015_07_23-PM-04_13_09
Last ObjectModification:
2014_11_26-AM-11_26_15
Home
Index