Nuprl Lemma : new_23_sig_vote_with_ballot_first-not2
∀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:ℤ. ∀i:Id.
((∃e'∈[es-init(es;e);e). (↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;i))
∧ (↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e';n;r)))) supposing
((¬↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r)) and
(↑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_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_headers_type: new_23_sig_headers_type{i:l}(Cmd;notify;propose),
Message: Message(f),
event-ordering+: EO+(Info),
es-init: es-init(es;e),
es-closed-open-interval: [e;e'),
es-E: E,
Id: Id,
l_exists: (∃x∈L. P[x]),
list: T List,
vatype: ValueAllType,
assert: ↑b,
uimplies: b supposing a,
all: ∀x:A. B[x],
not: ¬A,
and: P ∧ Q,
int: ℤ,
atom: Atom
Lemmas :
assert_witness,
new_23_sig_vote_with_ballot_and_id_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,
not_wf,
Id_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_and_id-assert-type,
assert_of_band,
new_23_sig_vote_with_ballot_wf,
es-info-body_wf,
bl-all_wf,
es-closed-open-interval_wf,
es-init_wf,
bnot_wf,
not_over_and,
decidable__assert,
new_23_sig_vote_with_ballot_and_id-implies,
not-assert-bl-all,
l_exists_iff,
assert_of_bnot,
not-not-assert,
can-find-first,
sq_stable__assert,
bl-exists_wf,
first-member-iff,
assert-bl-exists,
member_append,
iff_transitivity,
l_all_wf2,
iff_weakening_uiff,
assert-bl-all,
l_all_functionality,
member-es-closed-open-interval,
es-init-eq,
es-loc-init,
es-loc_wf,
es-le-loc,
es-le_wf,
es-locl_transitivity2,
es-le_weakening,
es-closed-open-interval-sorted-by,
sorted-by_wf,
es-locl_wf,
sorted-by-append,
sorted-by-cons,
es-le_weakening_eq,
es-locl_irreflexivity,
l_all_fwd,
new_23_sig_vote_with_ballot_and_id-snd,
assert_functionality_wrt_uiff,
assert_elim,
and_wf,
not_assert_elim,
btrue_neq_bfalse
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{}. \mforall{}i:Id.
((\mexists{}e'\mmember{}[es-init(es;e);e). (\muparrow{}new\_23\_sig\_vote\_with\_ballot\_and\_id(Cmd;notify;propose;f;es;e';n;r;i))
\mwedge{} (\muparrow{}new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es;e';n;r)))) 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\_and\_id(Cmd;notify;propose;f;es;e;n;r;i)))
Date html generated:
2015_07_23-PM-04_02_00
Last ObjectModification:
2015_02_04-PM-03_55_51
Home
Index