Nuprl Lemma : pv11_p1_adopted_from_acceptor

∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀accpts,ldrs:bag(Id).
∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id). ∀bnum:pv11_p1_Ballot_Num(). ∀pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀c:Cmd.
  (pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ <bnum, pvals> ∈ pv11_p1_adopted'base(Cmd;f)(e)
  ⇒ (<b, s, c> ∈ pvals)
  ⇒ (↓∃e':E
        ∃accepted:(pv11_p1_Ballot_Num() × ℤ × Cmd) List
         ((e' < e) ∧ <bnum, accepted> ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e') ∧ (<b, s, c> ∈ accepted))))


Proof



Definitions occuring in Statement :  pv11_p1_message-constraint: pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; mf; es),  pv11_p1_AcceptorState: pv11_p1_AcceptorState(Cmd;ldrs_uid;mf),  pv11_p1_adopted'base: pv11_p1_adopted'base(Cmd;mf),  pv11_p1_headers_type: pv11_p1_headers_type{i:l}(Cmd),  pv11_p1_Ballot_Num: pv11_p1_Ballot_Num(),  Message: Message(f),  classrel: v ∈ X(e),  event-ordering+: EO+(Info),  es-causl: (e < e'),  es-E: E,  Id: Id,  l_member: (x ∈ l),  list: T List,  vatype: ValueAllType,  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  squash: ↓T,  implies: P ⇒ Q,  and: P ∧ Q,  function: x:A ─→ B[x],  pair: <a, b>,  product: x:A × B[x],  int: ℤ,  bag: bag(T)
Lemmas :  int_seg_wf,  length_wf,  name_wf,  pv11_p1_headers_wf,  l_all_iff,  l_member_wf,  equal_wf,  pv11_p1_headers_fun_wf,  cons_wf_listp,  nil_wf,  listp_wf,  cons_member,  cons_wf,  equal-wf-base,  iff_weakening_equal,  base-noloc-classrel-make-Msg2,  hdrmkmsg_lemma,  msg-header_wf,  pv11_p1_headers_no_inputs_wf,  squash_wf,  exists_wf,  es-E_wf,  event-ordering+_subtype,  es-causl_wf,  classrel_wf,  msg-interface_wf,  pv11_p1_main_wf,  make-msg-interface_wf,  es-loc_wf,  pv11_p1_adopted'base_wf,  pv11_p1_message-constraint_wf,  list_wf,  pv11_p1_Ballot_Num_wf,  bag_wf,  Id_wf,  event-ordering+_wf,  Message_wf,  subtype_rel_dep_function,  vatype_wf,  pv11_p1_headers_type_wf,  set_wf,  valueall-type_wf,  msg-authentic_wf,  es-info_wf,  pv11_p1-adopted,  pv11_p1_scout_from_acc,  pv11_p1_ScoutStateFun_wf,  pv11_p1_ScoutState-classrel,  pair-eta,  subtype_rel_product,  top_wf,  subtype_top,  all_wf,  true_wf,  es-le_wf,  pv11_p1_p1b'base_wf,  pv11_p1-p1b,  es-causl_transitivity2,  es-causle_weakening_locl,  es-causle_weakening,  pv11_p1_AcceptorState-classrel,  pv11_p1_AcceptorState_wf,  eo-forward_wf,  member-eo-forward-E,  es-info-body_wf,  pv11_p1_upd_bnum_wf,  eo-forward-base-classrel,  event-ordering+_cumulative,  subtype_rel_weakening,  ext-eq_weakening,  eo-forward-le,  eo-forward-E-subtype
Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}f:pv11\_p1\_headers\_type\{i:l\}(Cmd).  \mforall{}es:EO+(Message(f)).  \mforall{}e:E.
\mforall{}accpts,ldrs:bag(Id).  \mforall{}ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}reps:bag(Id).  \mforall{}bnum:pv11\_p1\_Ballot\000C\_Num().
\mforall{}pvals:(pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List.  \mforall{}b:pv11\_p1\_Ballot\_Num().  \mforall{}s:\mBbbZ{}.  \mforall{}c:Cmd.
    (pv11\_p1\_message-constraint\{paxos-v11-part1.esh:o\}(Cmd;  accpts;  ldrs;  ldrs$_{uid}\mbackslash{}\000Cff24;  reps;  f;  es)
    {}\mRightarrow{}  <bnum,  pvals>  \mmember{}  pv11\_p1\_adopted'base(Cmd;f)(e)
    {}\mRightarrow{}  (<b,  s,  c>  \mmember{}  pvals)
    {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E
                \mexists{}accepted:(pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List
                  ((e'  <  e)
                  \mwedge{}  <bnum,  accepted>  \mmember{}  pv11\_p1\_AcceptorState(Cmd;ldrs$_{uid}$;f)(e')
                  \mwedge{}  (<b,  s,  c>  \mmember{}  accepted))))


Date html generated: 2015_07_23-PM-04_47_48
Last ObjectModification: 2015_02_04-AM-08_21_45

Home Index