Nuprl Lemma : new_23_sig_vote_with_ballot-forward

[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[start:E]. ∀[Cmd,propose,notify,e,n,r:Top].
  (new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es.start;e;n;r) 
  new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r))


Proof




Definitions occuring in Statement :  new_23_sig_vote_with_ballot: new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r) 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: 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:Top].
    (new\_23\_sig\_vote\_with\_ballot(Cmd;notify;propose;f;es.start;e;n;r) 
    \msim{}  new\_23\_sig\_vote\_with\_ballot(Cmd;notify;propose;f;es;e;n;r))



Date html generated: 2015_07_23-PM-04_01_06
Last ObjectModification: 2015_01_29-AM-08_47_50

Home Index