Nuprl Definition : pv11_p1_LeaderPreempted-program

pv11_p1_LeaderPreempted-program(Cmd;ldrs_uid;mf) ==
  eclass1-program(pv11_p1_leader_preempted(Cmd;ldrs_uid);pv11_p1_preempted'base-program(Cmd;mf))
  pv11_p1_LeaderState-program(Cmd;ldrs_uid;mf)



Definitions occuring in Statement :  pv11_p1_leader_preempted: pv11_p1_leader_preempted(Cmd;ldrs_uid) pv11_p1_LeaderState-program: pv11_p1_LeaderState-program(Cmd;ldrs_uid;mf) pv11_p1_preempted'base-program: pv11_p1_preempted'base-program(Cmd;mf) eclass2-program: Xpr Ypr eclass1-program: eclass1-program(f;pr)
FDL editor aliases :  pv11_p1_LeaderPreempted-program

Latex:
pv11\_p1\_LeaderPreempted-program(Cmd;ldrs$_{uid}$;mf)  ==
    eclass1-program(pv11\_p1\_leader\_preempted(Cmd;ldrs$_{uid}$);pv11\_p1\_preempted'b\000Case-program(Cmd;mf))
    o  pv11\_p1\_LeaderState-program(Cmd;ldrs$_{uid}$;mf)



Date html generated: 2015_07_23-PM-04_33_46
Last ObjectModification: 2014_11_26-AM-11_30_48

Home Index