Nuprl Lemma : new_23_sig_decided_property

∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff,flrs:ℤ]. ∀[propose,notify:Atom List].
∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))].
  (new_23_sig_message-constraint{i:l}(Cmd;clients;eq;coeff;flrs;notify;propose;reps;slots;f)
  ⇒ (∀e:E. ∀c:Cmd. ∀n:ℤ.
        (<n, c> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e)
        ⇒ (↓∃x:Id
              ∃rnd:ℕ
               ∃L:Id List
                (no_repeats(Id;L)
                ∧ (||L|| = ((coeff * flrs) + 1) ∈ ℤ)
                ∧ (∀vtr∈L.↓∃e':E. mk-msg-interface(x;make-Msg(``new_23_sig vote``;<<<n, rnd>, c>, vtr>)) ∈ new_23_sig_ma\000Cin()(e')))))))


Proof



Definitions occuring in Statement :  new_23_sig_message-constraint: new_23_sig_message-constraint{i:l}(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f),  new_23_sig_main: new_23_sig_main(),  new_23_sig_decided'base: new_23_sig_decided'base(Cmd;notify;propose;f),  new_23_sig_headers_type: new_23_sig_headers_type{i:l}(Cmd;notify;propose),  mk-msg-interface: mk-msg-interface(l;m),  msg-interface: Interface,  make-Msg: make-Msg(hdr;val),  Message: Message(f),  classrel: v ∈ X(e),  event-ordering+: EO+(Info),  es-E: E,  Id: Id,  deq: EqDecider(T),  l_all: (∀x∈L.P[x]),  no_repeats: no_repeats(T;l),  length: ||as||,  cons: [a / b],  nil: [],  list: T List,  nat: ℕ,  vatype: ValueAllType,  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  squash: ↓T,  implies: P ⇒ Q,  and: P ∧ Q,  pair: <a, b>,  product: x:A × B[x],  multiply: n * m,  add: n + m,  natural_number: $n,  int: ℤ,  token: "$token",  atom: Atom,  equal: s = t ∈ T,  bag: bag(T),  set-sig: set-sig{i:l}(Item)
Definitions :  assert: ↑b,  ifthenelse: if b then t else f fi ,  deq-member: x ∈b L),  reduce: reduce(f;k;as),  new_23_sig_headers_internal: new_23_sig_headers_internal(),  cons: [a / b],  bor: p ∨bq,  list-deq: list-deq(eq),  band: p ∧b q,  atom-deq: AtomDeq,  eq_atom: x =a y,  btrue: tt,  nil: [],  it: ⋅,  null: null(as),  true: True,  member: t ∈ T
Lemmas :  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,  base-noloc-classrel-make-Msg2,  hdrmkmsg_lemma,  msg-header_wf,  new_23_sig_headers_internal_wf,  exists_wf,  es-causl_wf,  classrel_wf,  msg-interface_wf,  new_23_sig_main_wf,  make-msg-interface_wf,  es-loc_wf,  Message_wf,  subtype_rel_dep_function,  vatype_wf,  new_23_sig_decided'base_wf,  es-E_wf,  event-ordering+_subtype,  new_23_sig_message-constraint_wf,  event-ordering+_wf,  new_23_sig_headers_type_wf,  set-sig_wf,  list_wf,  bag_wf,  Id_wf,  deq_wf,  valueall-type_wf,  msg-authentic_wf,  es-info_wf,  poss-maj-unanimous,  es-info-body_wf,  new_23_sig_QuorumStateFun_wf,  eo-forward_wf,  member-eo-forward-E,  length_of_cons_lemma,  pair-eta,  poss-maj_wf,  subtype_rel_product,  nat_wf,  top_wf,  subtype_top,  zero-le-nat,  decidable__equal_int,  pi1_wf_top,  false_wf,  not-equal-2,  le_antisymmetry_iff,  condition-implies-le,  minus-add,  minus-one-mul,  add-swap,  add-commutes,  add-associates,  zero-add,  add_functionality_wrt_le,  le-add-cancel2,  le_wf,  new_23_sig-decided,  no_repeats_cons,  new_23_sig_quorum_invariant_fun,  no_repeats_wf,  equal-wf-T-base,  int_subtype_base,  l_all_wf2,  mk-msg-interface_wf,  make-Msg_wf,  subtype_rel_weakening,  ext-eq_weakening,  and_wf,  subtype_rel_transitivity,  es-info-type_wf,  productdeq_reduce_lemma,  intdeq_reduce_lemma,  not_wf,  assert_wf,  eq_int_wf,  assert_of_eq_int,  bnot_wf,  deq-member_wf,  id-deq_wf,  iff_transitivity,  iff_weakening_uiff,  assert_of_band,  assert_of_bnot,  assert-deq-member,  es-info-mk-msg,  event-ordering+_cumulative,  es-info-auth_wf,  mk-msg_wf,  new_23_sig_assert_newvote,  make-Msg-as-mk-msg,  new_23_sig-vote,  new_23_sig_quorum_inv_vote_fun,  lelt_wf,  atom2_subtype_base,  select_wf,  sq_stable__le,  less_than_transitivity1,  le_weakening,  less_than_wf,  new_23_sig_vote'base_wf,  eo-forward-base-classrel,  eo-forward-E-subtype,  eo-forward-locl,  subtype_rel_self,  non_neg_length,  length_wf_nat,  new_23_sig_rounds_pos_fun,  less_than_transitivity2,  new_23_sig_NewRoundsStateFun_wf,  le_weakening2,  decidable__lt,  less-iff-le,  le-add-cancel,  select_member
Latex:
\mforall{}[Cmd:ValueAllType].  \mforall{}[eq:EqDecider(Cmd)].  \mforall{}[reps,clients:bag(Id)].  \mforall{}[coeff,flrs:\mBbbZ{}].
\mforall{}[propose,notify:Atom  List].  \mforall{}[slots:set-sig\{i:l\}(\mBbbZ{})].
\mforall{}[f:new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose)].  \mforall{}[es:EO+(Message(f))].
    (new\_23\_sig\_message-constraint\{i:l\}(Cmd;clients;eq;coeff;flrs;notify;propose;reps;slots;f)
    {}\mRightarrow{}  (\mforall{}e:E.  \mforall{}c:Cmd.  \mforall{}n:\mBbbZ{}.
                (<n,  c>  \mmember{}  new\_23\_sig\_decided'base(Cmd;notify;propose;f)(e)
                {}\mRightarrow{}  (\mdownarrow{}\mexists{}x:Id
                            \mexists{}rnd:\mBbbN{}
                              \mexists{}L:Id  List
                                (no\_repeats(Id;L)
                                \mwedge{}  (||L||  =  ((coeff  *  flrs)  +  1))
                                \mwedge{}  (\mforall{}vtr\mmember{}L.\mdownarrow{}\mexists{}e':E
                                                        mk-msg-interface(x;make-Msg(``new\_23\_sig  vote``;<<<n,  rnd>,  c>,  vtr>))  \mmember{}\000C  new\_23\_sig\_main()(e')))))))


Date html generated: 2015_07_23-PM-03_58_17
Last ObjectModification: 2015_02_04-PM-01_50_17

Home Index