Nuprl Lemma : new_23_sig_replica_state_mem

Cmd:ValueAllType. ∀notify,propose:Atom List. ∀slots:set-sig{i:l}(ℤ).
f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀slots1,slots2:set-sig-set(slots).
z:ℤ × Cmd.
  ((e1 <loc e2)
   z ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e1)
   slots1 ∈ new_23_sig_ReplicaState(Cmd;notify;propose;slots;f)(e1)
   slots2 ∈ new_23_sig_ReplicaState(Cmd;notify;propose;slots;f)(e2)
   let n,cmd 
     in ↑(set-sig-member(slots) slots2))


Proof




Definitions occuring in Statement :  new_23_sig_ReplicaState: new_23_sig_ReplicaState(Cmd;notify;propose;slots;f) new_23_sig_Proposal: new_23_sig_Proposal(Cmd;notify;propose;f) new_23_sig_headers_type: new_23_sig_headers_type{i:l}(Cmd;notify;propose) Message: Message(f) classrel: v ∈ X(e) event-ordering+: EO+(Info) es-locl: (e <loc e') es-E: E list: List vatype: ValueAllType assert: b all: x:A. B[x] implies:  Q apply: a spread: spread def product: x:A × B[x] int: atom: Atom set-sig-member: set-sig-member(s) set-sig-set: set-sig-set(s) set-sig: set-sig{i:l}(Item)
Lemmas :  int_seg_wf length_wf name_wf new_23_sig_headers_wf l_all_iff l_member_wf equal_wf new_23_sig_headers_fun_wf cons_member cons_wf cons_wf_listp listp_wf nil_wf equal-wf-base list_subtype_base atom_subtype_base iff_weakening_equal name_eq_wf bool_wf eqtt_to_assert assert-name_eq sq_stable__no_repeats squash_wf true_wf eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot Id_wf classrel_wf es-E_wf event-ordering+_subtype event-ordering+_wf eclass_wf set-sig-set_wf Memory1-memory-class1 set-sig-empty_wf new_23_sig_update_replica_wf new_23_sig_Proposal_wf Memory-loc-class-mem assert_wf set-sig-member_wf single-bag_wf set-sig-add-prop int_subtype_base parallel-class-single-val new_23_sig_propose'base_wf eclass0_wf new_23_sig_vote'base_wf new_23_sig_vote2prop_wf disjoint-classrel-symm eclass0-disjoint-classrel base-disjoint-classrel length_of_cons_lemma length_of_nil_lemma false_wf le_wf not_wf less_than_wf nat_wf sq_stable__encodes-msg-type l_all_fwd list_wf valueall-type_wf subtype_rel_weakening ext-eq_weakening top_wf eclass0-single-val single-valued-bag-single base-headers-msg-val-single-val new_23_sig_ReplicaState_wf es-locl_wf Message_wf subtype_rel_dep_function vatype_wf new_23_sig_headers_type_wf set-sig_wf set_wf

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}notify,propose:Atom  List.  \mforall{}slots:set-sig\{i:l\}(\mBbbZ{}).
\mforall{}f:new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose).  \mforall{}es:EO+(Message(f)).  \mforall{}e1,e2:E.
\mforall{}slots1,slots2:set-sig-set(slots).  \mforall{}z:\mBbbZ{}  \mtimes{}  Cmd.
    ((e1  <loc  e2)
    {}\mRightarrow{}  z  \mmember{}  new\_23\_sig\_Proposal(Cmd;notify;propose;f)(e1)
    {}\mRightarrow{}  slots1  \mmember{}  new\_23\_sig\_ReplicaState(Cmd;notify;propose;slots;f)(e1)
    {}\mRightarrow{}  slots2  \mmember{}  new\_23\_sig\_ReplicaState(Cmd;notify;propose;slots;f)(e2)
    {}\mRightarrow{}  let  n,cmd  =  z 
          in  \muparrow{}(set-sig-member(slots)  n  slots2))



Date html generated: 2015_07_23-PM-03_52_20
Last ObjectModification: 2015_02_04-PM-01_53_43

Home Index