Nuprl Definition : new_23_sig_vote_with_ballot_first
new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r) ==
new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)
∧b (∀e'∈[es-init(es;e);e).¬bnew_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;snd(msgval(e))))_b
Definitions occuring in Statement :
new_23_sig_vote_with_ballot_and_id: new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i),
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-init: es-init(es;e),
es-closed-open-interval: [e;e'),
bl-all: (∀x∈L.P[x])_b,
band: p ∧b q,
bnot: ¬bb,
pi2: snd(t)
FDL editor aliases :
new_23_sig_vote_with_ballot_first
Latex:
new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es;e;n;r) ==
new\_23\_sig\_vote\_with\_ballot(Cmd;notify;propose;f;es;e;n;r)
\mwedge{}\msubb{} (\mforall{}e'\mmember{}[es-init(es;e);e).
\mneg{}\msubb{}new\_23\_sig\_vote\_with\_ballot\_and\_id(Cmd;notify;propose;f;es;e';n;r;snd(msgval(e))))\_b
Date html generated:
2015_07_23-PM-04_01_42
Last ObjectModification:
2013_11_23-PM-09_59_23
Home
Index