Nuprl Definition : pv8_p1_LeaderState
pv8_p1_LeaderState(Cid;Op;eq_Cid;ldrs_uid) ==
Memory3(
l.{pv8_p1_init_leader(Cid;Op) l};
pv8_p1_on_propose(Cid;Op;eq_Cid);pv8_p1_propose'base(Cid;Op);
pv8_p1_when_adopted(Cid;Op;ldrs_uid);pv8_p1_adopted'base(Cid;Op);
pv8_p1_when_preempted(Cid;Op;ldrs_uid);pv8_p1_preempted'base())
Definitions occuring in Statement :
pv8_p1_when_preempted: pv8_p1_when_preempted(Cid;Op;ldrs_uid),
pv8_p1_when_adopted: pv8_p1_when_adopted(Cid;Op;ldrs_uid),
pv8_p1_on_propose: pv8_p1_on_propose(Cid;Op;eq_Cid),
pv8_p1_init_leader: pv8_p1_init_leader(Cid;Op),
pv8_p1_propose'base: pv8_p1_propose'base(Cid;Op),
pv8_p1_adopted'base: pv8_p1_adopted'base(Cid;Op),
pv8_p1_preempted'base: pv8_p1_preempted'base(),
Memory3: Memory3,
apply: f a,
lambda: x.A[x],
single-bag: {x}
FDL editor aliases :
pv8_p1_LeaderState
pv8_p1_LeaderState
pv8\_p1\_LeaderState(Cid;Op;eq$_{Cid}$;ldrs$_{uid}$) ==
Memory3(\mlambda{}l.\{pv8\_p1\_init\_leader(Cid;Op) l\};
pv8\_p1\_on\_propose(Cid;Op;eq$_{Cid}$);pv8\_p1\_propose'base(Cid;Op);
pv8\_p1\_when\_adopted(Cid;Op;ldrs$_{uid}$);pv8\_p1\_adopted'base(Cid;Op);
pv8\_p1\_when\_preempted(Cid;Op;ldrs$_{uid}$);pv8\_p1\_preempted'base())
Date html generated:
2012_02_20-PM-07_30_50
Last ObjectModification:
2012_02_06-PM-01_47_47
Home
Index