Nuprl Lemma : pv11_p1-adopted

[Cmd:{T:Type| valueall-type(T)} ]. ∀[accpts,ldrs:bag(Id)]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[reps:bag(Id)].
[mf:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(mf))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[auth:𝔹].
[p:pv11_p1_Ballot_Num()]. ∀[L:(pv11_p1_Ballot_Num() × ℤ × Cmd) List].
  (<d, i, mk-msg(auth;``pv11_p1 adopted``;<p, L>)> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;mf)(e)
  ⇐⇒ loc(e) ↓∈ ldrs
      ∧ (↓((no ((pv11_p1_scout_output(Cmd;accpts;mf) (pv11_p1_init_ballot_num() loc(e)) pv11_p1_p1b'base(Cmd;mf)) o
               pv11_p1_ScoutState(Cmd;accpts;mf) (pv11_p1_init_ballot_num() loc(e))) prior to e)
          ∧ ((header(e) ``pv11_p1 p1b`` ∈ Name)
            ∧ has-es-info-type(es;e;mf;Id
              × pv11_p1_Ballot_Num()
              × pv11_p1_Ballot_Num()
              × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))
          ∧ ((pv11_p1_init_ballot_num() loc(e)) (fst(snd(msgval(e)))) ∈ pv11_p1_Ballot_Num())
          ∧ (d 0 ∈ ℤ)
          ∧ (i loc(e) ∈ Id)
          ∧ ((pv11_p1_init_ballot_num() loc(e)) (fst(snd(snd(msgval(e))))) ∈ pv11_p1_Ballot_Num())
          ∧ #(fst(pv11_p1_ScoutStateFun(Cmd;accpts;mf;pv11_p1_init_ballot_num() 
                                                      loc(e);es;e))) < pv11_p1_threshold(accpts)
          ∧ auth pv11_p1_init_active()
          ∧ (p (pv11_p1_init_ballot_num() loc(e)) ∈ pv11_p1_Ballot_Num())
          ∧ (L
            (snd(pv11_p1_ScoutStateFun(Cmd;accpts;mf;pv11_p1_init_ballot_num() loc(e);es;e)))
            ∈ ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))
          ∨ (∃e':{e':E| e' ≤loc 
              ((((header(e') ``pv11_p1 preempted`` ∈ Name) ∧ has-es-info-type(es;e';mf;pv11_p1_Ballot_Num()))
               ∧ (↑(pv11_p1_is_bnum() msgval(e')))
               ∧ (↑(fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e'))  < msgval(e'))))
              ∧ (no ((pv11_p1_scout_output(Cmd;accpts;mf) (pv11_p1_upd_bnum() msgval(e') loc(e')) o
                     pv11_p1_p1b'base(Cmd;mf)) pv11_p1_ScoutState(Cmd;accpts;mf) 
                                                 (pv11_p1_upd_bnum() msgval(e') loc(e'))) between e' and e)
              ∧ ((header(e) ``pv11_p1 p1b`` ∈ Name)
                ∧ has-es-info-type(es;e;mf;Id
                  × pv11_p1_Ballot_Num()
                  × pv11_p1_Ballot_Num()
                  × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))
              ∧ ((pv11_p1_upd_bnum() msgval(e') loc(e')) (fst(snd(msgval(e)))) ∈ pv11_p1_Ballot_Num())
              ∧ (d 0 ∈ ℤ)
              ∧ (i loc(e) ∈ Id)
              ∧ ((pv11_p1_upd_bnum() msgval(e') loc(e')) (fst(snd(snd(msgval(e))))) ∈ pv11_p1_Ballot_Num())
              ∧ #(fst(pv11_p1_ScoutStateFun(Cmd;accpts;mf;pv11_p1_upd_bnum() msgval(e') 
                                                          loc(e');es.e';e))) < pv11_p1_threshold(accpts)
              ∧ auth pv11_p1_init_active()
              ∧ (p (pv11_p1_upd_bnum() msgval(e') loc(e')) ∈ pv11_p1_Ballot_Num())
              ∧ (L
                (snd(pv11_p1_ScoutStateFun(Cmd;accpts;mf;pv11_p1_upd_bnum() msgval(e') loc(e');es.e';e)))
                ∈ ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))))))


Proof




Definitions occuring in Statement :  pv11_p1_main: pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;mf) pv11_p1_LeaderStateFun: pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e) pv11_p1_scout_output: pv11_p1_scout_output(Cmd;accpts;mf) pv11_p1_ScoutStateFun: pv11_p1_ScoutStateFun(Cmd;accpts;mf;x;es;e) pv11_p1_ScoutState: pv11_p1_ScoutState(Cmd;accpts;mf) pv11_p1_init_active: pv11_p1_init_active() pv11_p1_init_ballot_num: pv11_p1_init_ballot_num() pv11_p1_p1b'base: pv11_p1_p1b'base(Cmd;mf) pv11_p1_threshold: pv11_p1_threshold(accpts) pv11_p1_headers_type: pv11_p1_headers_type{i:l}(Cmd) pv11_p1_lt_bnum: pv11_p1_lt_bnum(ldrs_uid) pv11_p1_upd_bnum: pv11_p1_upd_bnum() pv11_p1_is_bnum: pv11_p1_is_bnum() pv11_p1_Ballot_Num: pv11_p1_Ballot_Num() msg-interface: Interface mk-msg: mk-msg(auth;hdr;val) es-info-body: msgval(e) has-es-info-type: has-es-info-type(es;e;f;T) es-header: header(e) Message: Message(f) eclass2: (X Y) eclass1: (f X) no-classrel-in-interval: (no between start and e) no-prior-classrel: (no prior to e) classrel: v ∈ X(e) eo-forward: eo.e event-ordering+: EO+(Info) es-le: e ≤loc e'  es-loc: loc(e) es-E: E Id: Id name: Name cons: [a b] nil: [] list: List valueall-type: valueall-type(T) assert: b bool: 𝔹 less_than: a < b uall: [x:A]. B[x] pi1: fst(t) pi2: snd(t) exists: x:A. B[x] iff: ⇐⇒ Q squash: T or: P ∨ Q and: P ∧ Q set: {x:A| B[x]}  apply: a function: x:A ─→ B[x] pair: <a, b> product: x:A × B[x] natural_number: $n int: token: "$token" universe: Type equal: t ∈ T bag-member: x ↓∈ bs bag-size: #(bs) bag: bag(T)
Lemmas :  sq_stable__and equal_wf cons_wf_listp nil_wf listp_wf vatype_wf cons_wf equal-wf-T-base sq_stable__equal squash_wf int_seg_wf length_wf name_wf pv11_p1_headers_wf l_all_iff l_member_wf pv11_p1_headers_fun_wf cons_member equal-wf-base iff_weakening_equal classrel_wf msg-interface_wf pv11_p1_main_wf make-msg-interface_wf mk-msg_wf subtype_rel_weakening ext-eq_weakening bag-member_wf es-loc_wf event-ordering+_subtype or_wf no-prior-classrel_wf eclass2_wf list_wf eclass1_wf bag_wf pv11_p1_p1b'base_wf pv11_p1_scout_output_wf pv11_p1_init_ballot_num_wf pv11_p1_ScoutState_wf es-header_wf has-es-info-type_wf es-info-body_wf int_subtype_base less_than_wf bag-size_wf pv11_p1_ScoutStateFun_wf nat_wf pv11_p1_threshold_wf bool_wf exists_wf es-E_wf es-le_wf assert_wf pv11_p1_is_bnum_wf pv11_p1_lt_bnum_wf pv11_p1_LeaderStateFun_wf no-classrel-in-interval_wf pv11_p1_upd_bnum_wf eo-forward_wf member-eo-forward-E pv11_p1_Ballot_Num_wf event-ordering+_wf Message_wf subtype_rel_dep_function pv11_p1_headers_type_wf Id_wf set_wf valueall-type_wf pv11_p1-ilf make-Msg_wf not_wf eo-forward-header eo-forward-has-es-info-type equal-wf-base-T pv11_p1_CommanderStateFun_wf pv11_p1_in_domain_wf list-subtype-bag pv11_p1_pmax_wf pv11_p1_p2b'base_wf pv11_p1_commander_output_wf pv11_p1_CommanderState_wf es-first_wf2 pv11_p1_AcceptorStateFun_wf msg-header_wf hdrmkmsg_lemma hdrmakeMsg_lemma sq_stable__no_repeats true_wf false_wf and_wf make-Msg-as-mk-msg mk-msg-equal bfalse_wf null_nil_lemma btrue_wf reduce_tl_cons_lemma tl_wf null_wf3 subtype_rel_list top_wf null_cons_lemma btrue_neq_bfalse equal_functionality_wrt_subtype_rel2 eo-forward-info-body eo-forward-loc sq_stable__bag-member

Latex:
\mforall{}[Cmd:\{T:Type|  valueall-type(T)\}  ].  \mforall{}[accpts,ldrs:bag(Id)].  \mforall{}[ldrs$_{uid}$:Id  {}\mrightarrow{}\000C  \mBbbZ{}].  \mforall{}[reps:bag(Id)].
\mforall{}[mf:pv11\_p1\_headers\_type\{i:l\}(Cmd)].  \mforall{}[es:EO+(Message(mf))].  \mforall{}[e:E].  \mforall{}[d:\mBbbZ{}].  \mforall{}[i:Id].  \mforall{}[auth:\mBbbB{}].
\mforall{}[p:pv11\_p1\_Ballot\_Num()].  \mforall{}[L:(pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List].
    (<d,  i,  mk-msg(auth;``pv11\_p1  adopted``;<p,  L>)>  \mmember{}  pv11\_p1\_main(Cmd;accpts;ldrs;ldrs$_\mbackslash{}ff7\000Cbuid}$;reps;mf)(e)
    \mLeftarrow{}{}\mRightarrow{}  loc(e)  \mdownarrow{}\mmember{}  ldrs
            \mwedge{}  (\mdownarrow{}((no  ((pv11\_p1\_scout\_output(Cmd;accpts;mf)  (pv11\_p1\_init\_ballot\_num()  loc(e))  o
                                pv11\_p1\_p1b'base(Cmd;mf))  o  pv11\_p1\_ScoutState(Cmd;accpts;mf) 
                                                                                        (pv11\_p1\_init\_ballot\_num()  loc(e)))  prior  to  e)
                    \mwedge{}  ((header(e)  =  ``pv11\_p1  p1b``)
                        \mwedge{}  has-es-info-type(es;e;mf;Id
                            \mtimes{}  pv11\_p1\_Ballot\_Num()
                            \mtimes{}  pv11\_p1\_Ballot\_Num()
                            \mtimes{}  ((pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List)))
                    \mwedge{}  ((pv11\_p1\_init\_ballot\_num()  loc(e))  =  (fst(snd(msgval(e)))))
                    \mwedge{}  (d  =  0)
                    \mwedge{}  (i  =  loc(e))
                    \mwedge{}  ((pv11\_p1\_init\_ballot\_num()  loc(e))  =  (fst(snd(snd(msgval(e))))))
                    \mwedge{}  \#(fst(pv11\_p1\_ScoutStateFun(Cmd;accpts;mf;pv11\_p1\_init\_ballot\_num() 
                                                                                                            loc(e);es;e)))  <  pv11\_p1\_threshold(accpts)
                    \mwedge{}  auth  =  pv11\_p1\_init\_active()
                    \mwedge{}  (p  =  (pv11\_p1\_init\_ballot\_num()  loc(e)))
                    \mwedge{}  (L  =  (snd(pv11\_p1\_ScoutStateFun(Cmd;accpts;mf;pv11\_p1\_init\_ballot\_num()  loc(e);es;e)))))
                    \mvee{}  (\mexists{}e':\{e':E|  e'  \mleq{}loc  e  \} 
                            ((((header(e')  =  ``pv11\_p1  preempted``)
                                \mwedge{}  has-es-info-type(es;e';mf;pv11\_p1\_Ballot\_Num()))
                              \mwedge{}  (\muparrow{}(pv11\_p1\_is\_bnum()  msgval(e')))
                              \mwedge{}  (\muparrow{}(fst(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;mf;es;e'))    <  ms\000Cgval(e'))))
                            \mwedge{}  (no  ((pv11\_p1\_scout\_output(Cmd;accpts;mf)  (pv11\_p1\_upd\_bnum()  msgval(e')  loc(e'))  o
                                          pv11\_p1\_p1b'base(Cmd;mf))  o  pv11\_p1\_ScoutState(Cmd;accpts;mf) 
                                                                                                  (pv11\_p1\_upd\_bnum()  msgval(e')  loc(e')))  between  e'
                                  and  e)
                            \mwedge{}  ((header(e)  =  ``pv11\_p1  p1b``)
                                \mwedge{}  has-es-info-type(es;e;mf;Id
                                    \mtimes{}  pv11\_p1\_Ballot\_Num()
                                    \mtimes{}  pv11\_p1\_Ballot\_Num()
                                    \mtimes{}  ((pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List)))
                            \mwedge{}  ((pv11\_p1\_upd\_bnum()  msgval(e')  loc(e'))  =  (fst(snd(msgval(e)))))
                            \mwedge{}  (d  =  0)
                            \mwedge{}  (i  =  loc(e))
                            \mwedge{}  ((pv11\_p1\_upd\_bnum()  msgval(e')  loc(e'))  =  (fst(snd(snd(msgval(e))))))
                            \mwedge{}  \#(fst(pv11\_p1\_ScoutStateFun(Cmd;accpts;mf;pv11\_p1\_upd\_bnum()  msgval(e') 
                                                                                                                    loc(e');es.e';e)))  <  ...
                            \mwedge{}  auth  =  pv11\_p1\_init\_active()
                            \mwedge{}  (p  =  (pv11\_p1\_upd\_bnum()  msgval(e')  loc(e')))
                            \mwedge{}  (L
                                =  (snd(pv11\_p1\_ScoutStateFun(Cmd;accpts;mf;pv11\_p1\_upd\_bnum()  msgval(e') 
                                                                                                                      loc(e');es.e';e))))))))



Date html generated: 2015_07_23-PM-04_43_11
Last ObjectModification: 2015_02_04-PM-02_45_25

Home Index