Nuprl Definition : pv11_p1_LeaderPreempted
pv11_p1_LeaderPreempted(Cmd;ldrs_uid;mf) ==
((pv11_p1_leader_preempted(Cmd;ldrs_uid) o pv11_p1_preempted'base(Cmd;mf)) o pv11_p1_LeaderState(Cmd;ldrs_uid;mf))
Definitions occuring in Statement :
pv11_p1_leader_preempted: pv11_p1_leader_preempted(Cmd;ldrs_uid),
pv11_p1_LeaderState: pv11_p1_LeaderState(Cmd;ldrs_uid;mf),
pv11_p1_preempted'base: pv11_p1_preempted'base(Cmd;mf),
eclass2: (X o Y),
eclass1: (f o X)
FDL editor aliases :
pv11_p1_LeaderPreempted
Latex:
pv11\_p1\_LeaderPreempted(Cmd;ldrs$_{uid}$;mf) ==
((pv11\_p1\_leader\_preempted(Cmd;ldrs$_{uid}$) o pv11\_p1\_preempted'base(Cmd;mf))\000C o
pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;mf))
Date html generated:
2015_07_23-PM-04_33_43
Last ObjectModification:
2014_11_26-AM-11_30_42
Home
Index