Nuprl Definition : new_23_sig_vote_with_ballot_first_alt
new_23_sig_vote_with_ballot_first_alt(Cmd;notify;propose;f;es;e;e';n;r;a) ==
new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;a;n;r)
∧b (¬b(∃x∈[e, e'].new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;x;n;r)
∧b es-blocl(es;x;a)
∧b (IdDeq (snd(msgval(x))) (snd(msgval(a)))))_b)
Definitions occuring in Statement :
new_23_sig_vote_with_ballot: new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r),
es-info-body: msgval(e),
es-interval: [e, e'],
es-blocl: es-blocl(es;e1;e2),
id-deq: IdDeq,
bl-exists: (∃x∈L.P[x])_b,
band: p ∧b q,
bnot: ¬bb,
pi2: snd(t),
apply: f a
FDL editor aliases :
new_23_sig_vote_with_ballot_first_alt
Latex:
new\_23\_sig\_vote\_with\_ballot\_first\_alt(Cmd;notify;propose;f;es;e;e';n;r;a) ==
new\_23\_sig\_vote\_with\_ballot(Cmd;notify;propose;f;es;a;n;r)
\mwedge{}\msubb{} (\mneg{}\msubb{}(\mexists{}x\mmember{}[e, e'].new\_23\_sig\_vote\_with\_ballot(Cmd;notify;propose;f;es;x;n;r)
\mwedge{}\msubb{} es-blocl(es;x;a)
\mwedge{}\msubb{} (IdDeq (snd(msgval(x))) (snd(msgval(a)))))\_b)
Date html generated:
2015_07_23-PM-04_02_18
Last ObjectModification:
2014_02_04-PM-00_06_44
Home
Index