Nuprl Definition : pv11_p1_LeaderAdopted

pv11_p1_LeaderAdopted(Cmd;ldrs_uid;mf) ==
  ((pv11_p1_leader_adopted(Cmd;ldrs_uid) pv11_p1_adopted'base(Cmd;mf)) pv11_p1_LeaderState(Cmd;ldrs_uid;mf))



Definitions occuring in Statement :  pv11_p1_leader_adopted: pv11_p1_leader_adopted(Cmd;ldrs_uid) pv11_p1_LeaderState: pv11_p1_LeaderState(Cmd;ldrs_uid;mf) pv11_p1_adopted'base: pv11_p1_adopted'base(Cmd;mf) eclass2: (X Y) eclass1: (f X)
FDL editor aliases :  pv11_p1_LeaderAdopted

Latex:
pv11\_p1\_LeaderAdopted(Cmd;ldrs$_{uid}$;mf)  ==
    ((pv11\_p1\_leader\_adopted(Cmd;ldrs$_{uid}$)  o  pv11\_p1\_adopted'base(Cmd;mf))  o
    pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;mf))



Date html generated: 2015_07_23-PM-04_33_34
Last ObjectModification: 2014_11_26-AM-11_30_25

Home Index