Nuprl Definition : 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) ==
e ∈b new_23_sig_vote'base(Cmd;notify;propose;f)
∧b (fst(fst(fst(msgval(e)))) =z n)
∧b (snd(fst(fst(msgval(e)))) =z r)
∧b snd(msgval(e)) = i
Definitions occuring in Statement :
new_23_sig_vote'base: new_23_sig_vote'base(Cmd;notify;propose;f),
es-info-body: msgval(e),
member-eclass: e ∈b X,
eq_id: a = b,
band: p ∧b q,
eq_int: (i =z j),
pi1: fst(t),
pi2: snd(t)
FDL editor aliases :
new_23_sig_vote_with_ballot_and_id
Latex:
new\_23\_sig\_vote\_with\_ballot\_and\_id(Cmd;notify;propose;f;es;e;n;r;i) ==
e \mmember{}\msubb{} new\_23\_sig\_vote'base(Cmd;notify;propose;f)
\mwedge{}\msubb{} (fst(fst(fst(msgval(e)))) =\msubz{} n)
\mwedge{}\msubb{} (snd(fst(fst(msgval(e)))) =\msubz{} r)
\mwedge{}\msubb{} snd(msgval(e)) = i
Date html generated:
2015_07_23-PM-04_01_07
Last ObjectModification:
2013_11_23-PM-09_59_02
Home
Index