Nuprl Lemma : pv11_p1_unique_adopted_fun2

Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀accpts,ldrs:bag(Id).
ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id). ∀bnum:pv11_p1_Ballot_Num(). ∀pvals1,pvals2:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
  (pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
   <bnum, pvals1> ∈ pv11_p1_adopted'base(Cmd;f)(e1)
   <bnum, pvals2> ∈ pv11_p1_adopted'base(Cmd;f)(e2)
   (bnum (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1))) ∈ pv11_p1_Ballot_Num())
   (bnum (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2))) ∈ pv11_p1_Ballot_Num())
   (loc(e1) loc(e2) ∈ Id)
   (pvals1 pvals2 ∈ ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))


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_LeaderStateFun: pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e) 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-loc: loc(e) es-E: E Id: Id list: List vatype: ValueAllType pi1: fst(t) all: x:A. B[x] implies:  Q function: x:A ─→ B[x] pair: <a, b> product: x:A × B[x] int: equal: t ∈ T 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 es-loc_wf pv11_p1_LeaderStateFun_wf bool_wf list_wf classrel_wf pv11_p1_adopted'base_wf pv11_p1_message-constraint_wf pv11_p1_Ballot_Num_wf bag_wf Id_wf es-E_wf event-ordering+_subtype event-ordering+_wf Message_wf subtype_rel_dep_function vatype_wf pv11_p1_headers_type_wf set_wf valueall-type_wf es-locl-trichotomy pv11_p1_unique_adopted_fun es-le_weakening single-valued-base-classrel event-ordering+_cumulative and_wf pi2_wf

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}f:pv11\_p1\_headers\_type\{i:l\}(Cmd).  \mforall{}es:EO+(Message(f)).  \mforall{}e1,e2:E.
\mforall{}accpts,ldrs:bag(Id).  \mforall{}ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}reps:bag(Id).  \mforall{}bnum:pv11\_p1\_Ballot\000C\_Num().
\mforall{}pvals1,pvals2:(pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List.
    (pv11\_p1\_message-constraint\{paxos-v11-part1.esh:o\}(Cmd;  accpts;  ldrs;  ldrs$_{uid}\mbackslash{}\000Cff24;  reps;  f;  es)
    {}\mRightarrow{}  <bnum,  pvals1>  \mmember{}  pv11\_p1\_adopted'base(Cmd;f)(e1)
    {}\mRightarrow{}  <bnum,  pvals2>  \mmember{}  pv11\_p1\_adopted'base(Cmd;f)(e2)
    {}\mRightarrow{}  (bnum  =  (fst(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e1))))
    {}\mRightarrow{}  (bnum  =  (fst(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e2))))
    {}\mRightarrow{}  (loc(e1)  =  loc(e2))
    {}\mRightarrow{}  (pvals1  =  pvals2))



Date html generated: 2015_07_23-PM-04_48_25
Last ObjectModification: 2015_02_04-AM-08_12_34

Home Index