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
Lemmas :
eo-forward-member-eclass,
event-ordering+_cumulative,
top_wf,
es-E_wf,
event-ordering+_subtype,
Message_wf,
event-ordering+_wf,
name_wf,
eo-forward-info-body
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:
2015_07_23-PM-04_01_40
Last ObjectModification:
2015_01_29-AM-08_47_26
Home
Index