Nuprl Lemma : pv11_p1_bnum_p2a_loc

Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
accpts,ldrs,reps:bag(Id). ∀b:pv11_p1_Ballot_Num(). ∀i,l:Id. ∀s:ℤ. ∀c:Cmd.
  (pv11_p1_p2a'send(Cmd;f) i <l, b, s, c> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e)
   (∃n:ℤ(↑(pv11_p1_eq_bnums() (pv11_p1_mk_bnum() loc(e))))))


Proof




Definitions occuring in Statement :  pv11_p1_p2a'send: pv11_p1_p2a'send(Cmd;f) pv11_p1_main: pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;mf) pv11_p1_headers_type: pv11_p1_headers_type{i:l}(Cmd) pv11_p1_eq_bnums: pv11_p1_eq_bnums() pv11_p1_mk_bnum: pv11_p1_mk_bnum() pv11_p1_Ballot_Num: pv11_p1_Ballot_Num() msg-interface: Interface Message: Message(f) classrel: v ∈ X(e) event-ordering+: EO+(Info) es-loc: loc(e) es-E: E Id: Id vatype: ValueAllType assert: b all: x:A. B[x] exists: x:A. B[x] implies:  Q apply: a function: x:A ─→ B[x] pair: <a, b> 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 list_wf classrel_wf msg-interface_wf pv11_p1_main_wf pv11_p1_p2a'send_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 make-Msg-as-mk-msg pv11_p1-p2a bfalse_wf sq_stable__assert pv11_p1_eq_bnums_wf subtype_rel_sum unit_wf2 pv11_p1_mk_bnum_wf pv11_p1_eq_bnums-assert and_wf outl_wf assert_wf isl_wf pi2_wf pv11_p1_ldr_fun_loc_bnum bag-member-sq-list-member pv11_p1_LeaderStateFun_wf bool_wf

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{}accpts,ldrs,reps:bag(Id).  \mforall{}b:pv11\_p1\_Ballot\_Num().  \mforall{}i,l:Id.  \mforall{}s:\mBbbZ{}.  \mforall{}c:Cmd.
    (pv11\_p1\_p2a'send(Cmd;f)  i  <l,  b,  s,  c>  \mmember{}  pv11\_p1\_main(Cmd;accpts;ldrs;ldrs$_{uid}\000C$;reps;f)(e)
    {}\mRightarrow{}  (\mexists{}n:\mBbbZ{}.  (\muparrow{}(pv11\_p1\_eq\_bnums()  b  (pv11\_p1\_mk\_bnum()  n  loc(e))))))



Date html generated: 2015_07_23-PM-04_49_03
Last ObjectModification: 2015_02_04-AM-08_05_16

Home Index