Nuprl Lemma : pv11_p1_ldr_active2

Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
v:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).
  (v ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e)
   let bnum,active,proposals1 in 
     (↑active)
      (↓∃e':E
           ∃pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List
            ∃proposals:(ℤ × Cmd) List
             ∃b:𝔹
              ((e' <loc e)
              ∧ <bnum, pvals> ∈ pv11_p1_adopted'base(Cmd;f)(e')
              ∧ <bnum, b, proposals> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e'))))


Proof




Definitions occuring in Statement :  pv11_p1_LeaderState: pv11_p1_LeaderState(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-locl: (e <loc e') es-E: E Id: Id list: List vatype: ValueAllType assert: b bool: 𝔹 spreadn: spread3 all: x:A. B[x] exists: x:A. B[x] squash: T implies:  Q and: P ∧ Q function: x:A ─→ B[x] pair: <a, b> product: x:A × B[x] int:
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 list_wf classrel_wf squash_wf true_wf es-E_wf event-ordering+_subtype event-ordering+_wf eclass_wf pv11_p1_Ballot_Num_wf bool_wf Memory3-memory-class3 pv11_p1_init_leader_wf pv11_p1_on_propose_wf pv11_p1_propose'base_wf pv11_p1_when_adopted_wf pv11_p1_adopted'base_wf pv11_p1_when_preempted_wf pv11_p1_preempted'base_wf Memory-loc-class-invariant-sv1 assert_wf exists_wf es-locl_wf pv11_p1_LeaderState_wf disjoint-union-tr_wf single-bag_wf Id_wf disjoint-union-comb_wf disjoint-union-comb-single-val base-headers-msg-val-single-val subtype_rel_weakening ext-eq_weakening base-disjoint-classrel iff_transitivity not_wf name_eq_wf bnot_wf assert-name_eq iff_weakening_uiff assert_of_bnot sq_stable__encodes-msg-type l_all_fwd valueall-type_wf equal-wf-T-base disjoint-classrel-symm disjoint-union-comb-disjoint-classrel single-valued-bag-single es-loc_wf bag-member-single bag-member_wf disj_un_tr_ap_inl_lemma disj_un_tr_ap_inr_lemma pv11_p1_eq_bnums_wf eqtt_to_assert pv11_p1_eq_bnums-assert eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot pv11_p1_is_bnum_wf pv11_p1_lt_bnum_wf false_wf Memory-loc-class_wf Message_wf subtype_rel_dep_function vatype_wf pv11_p1_headers_type_wf set_wf disjoint-union-comb-classrel union_subtype_base unit_wf2 product_subtype_base int_subtype_base atom2_subtype_base unit_subtype_base

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}f:pv11\_p1\_headers\_type\{i:l\}(Cmd).  \mforall{}es:EO+(Message(f)).  \mforall{}e:E.  \mforall{}ldrs$_\mbackslash{}ff7\000Cbuid}$:Id  {}\mrightarrow{}  \mBbbZ{}.
\mforall{}v:pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbB{}  \mtimes{}  ((\mBbbZ{}  \mtimes{}  Cmd)  List).
    (v  \mmember{}  pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(e)
    {}\mRightarrow{}  let  bnum,active,proposals1  =  v  in 
          (\muparrow{}active)
          {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E
                      \mexists{}pvals:(pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List
                        \mexists{}proposals:(\mBbbZ{}  \mtimes{}  Cmd)  List
                          \mexists{}b:\mBbbB{}
                            ((e'  <loc  e)
                            \mwedge{}  <bnum,  pvals>  \mmember{}  pv11\_p1\_adopted'base(Cmd;f)(e')
                            \mwedge{}  <bnum,  b,  proposals>  \mmember{}  pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(e\000C'))))



Date html generated: 2015_07_23-PM-04_45_42
Last ObjectModification: 2015_02_04-AM-08_29_02

Home Index