Nuprl Lemma : new_23_sig_vote_with_ballot_first-not

Cmd:ValueAllType. ∀propose,notify:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
e:E. ∀n,r:ℤ.
  ((∃e'∈[es-init(es;e);e). ↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;snd(...)))) supposing 
     ((¬↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r)) and 
     (↑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_first: new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r) 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) new_23_sig_headers_type: new_23_sig_headers_type{i:l}(Cmd;notify;propose) es-info-body: msgval(e) Message: Message(f) event-ordering+: EO+(Info) es-init: es-init(es;e) es-closed-open-interval: [e;e') es-E: E l_exists: (∃x∈L. P[x]) list: List vatype: ValueAllType assert: b uimplies: supposing a pi2: snd(t) all: x:A. B[x] not: ¬A int: atom: Atom
Lemmas :  assert_witness new_23_sig_vote_with_ballot_wf assert_wf new_23_sig_vote_with_ballot_first_wf int_seg_wf length_wf name_wf new_23_sig_headers_wf l_all_iff l_member_wf equal_wf new_23_sig_headers_fun_wf cons_member cons_wf cons_wf_listp listp_wf nil_wf equal-wf-base list_subtype_base atom_subtype_base iff_weakening_equal name_eq_wf bool_wf eqtt_to_assert assert-name_eq sq_stable__no_repeats squash_wf true_wf eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot Id_wf not_wf es-E_wf event-ordering+_subtype Message_wf subtype_rel_dep_function vatype_wf event-ordering+_wf new_23_sig_headers_type_wf list_wf valueall-type_wf new_23_sig_vote_with_ballot-assert-type assert_of_band es-info-body_wf bl-all_wf es-closed-open-interval_wf es-init_wf bnot_wf new_23_sig_vote_with_ballot_and_id_wf not_over_and decidable__assert not-assert-bl-all l_exists_iff assert_of_bnot not-not-assert

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}propose,notify:Atom  List.  \mforall{}f:new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose).
\mforall{}es:EO+(Message(f)).  \mforall{}e:E.  \mforall{}n,r:\mBbbZ{}.
    ((\mexists{}e'\mmember{}[es-init(es;e);e).  \muparrow{}...))  supposing 
          ((\mneg{}\muparrow{}new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es;e;n;r))  and 
          (\muparrow{}new\_23\_sig\_vote\_with\_ballot(Cmd;notify;propose;f;es;e;n;r)))



Date html generated: 2015_07_23-PM-04_01_55
Last ObjectModification: 2015_02_04-PM-03_54_55

Home Index