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: T List,
vatype: ValueAllType,
assert: ↑b,
uimplies: b 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