Nuprl Lemma : new_23_sig_vote_with_ballot_and_id-forward
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[start:E]. ∀[Cmd,propose,notify,e,n,r,i:Top].
(new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es.start;e;n;r;i)
~ new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i))
Proof
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),
Message: Message(f),
eo-forward: eo.e,
event-ordering+: EO+(Info),
es-E: E,
name: Name,
uall: ∀[x:A]. B[x],
top: Top,
function: x:A ⟶ B[x],
universe: Type,
sqequal: s ~ t
Definitions unfolded in proof :
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'base: new_23_sig_vote'base(Cmd;notify;propose;f),
uall: ∀[x:A]. B[x],
member: t ∈ T,
subtype_rel: A ⊆r B,
top: Top
Latex:
\mforall{}[f:Name {}\mrightarrow{} Type]. \mforall{}[es:EO+(Message(f))]. \mforall{}[start:E]. \mforall{}[Cmd,propose,notify,e,n,r,i:Top].
(new\_23\_sig\_vote\_with\_ballot\_and\_id(Cmd;notify;propose;f;es.start;e;n;r;i)
\msim{} new\_23\_sig\_vote\_with\_ballot\_and\_id(Cmd;notify;propose;f;es;e;n;r;i))
Date html generated:
2016_05_17-PM-02_32_16
Last ObjectModification:
2015_12_29-PM-08_04_01
Theory : 2!3!consensus!with!signatures
Home
Index