Nuprl Lemma : new_23_sig_rounds_strict_inc

∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e1,e2:E. ∀n,round1,round2:ℤ.
  ((∃z:ℤ × ℤ × Cmd
     ∃round:ℤ
      ∃e:E
       (e1 ≤loc e 
       ∧ (e <loc e2)
       ∧ z ∈ new_23_sig_RoundInfo(Cmd;notify;propose;f)(e)
       ∧ round ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e)
       ∧ let z,cmd = z 
         in let n',round' = z 
            in (n' = n ∈ ℤ) ∧ round < round'))
  ⇒ (e1 <loc e2)
  ⇒ round1 ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e1)
  ⇒ round2 ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e2)
  ⇒ round1 < round2)


Proof



Definitions occuring in Statement :  new_23_sig_NewRoundsState: new_23_sig_NewRoundsState(Cmd;notify;propose;f),  new_23_sig_RoundInfo: new_23_sig_RoundInfo(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-le: e ≤loc e' ,  es-locl: (e <loc e'),  es-E: E,  list: T List,  vatype: ValueAllType,  less_than: a < b,  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  implies: P ⇒ Q,  and: P ∧ Q,  apply: f a,  spread: spread def,  product: x:A × B[x],  int: ℤ,  atom: Atom,  equal: s = t ∈ T
Lemmas :  classrel_wf,  squash_wf,  true_wf,  es-E_wf,  event-ordering+_subtype,  event-ordering+_wf,  eclass_wf,  Memory1-memory-class1,  Id_wf,  new_23_sig_update_round_wf,  new_23_sig_RoundInfo_wf,  iff_weakening_equal,  Memory-loc-class-progress,  less_than_wf,  equal-wf-base,  int_subtype_base,  single-bag_wf,  decidable__cand,  decidable__equal_int,  decidable__lt,  less_than_transitivity2,  le_weakening2,  sq_stable__less_than,  eq_int_wf,  bool_wf,  eqtt_to_assert,  assert_of_eq_int,  lt_int_wf,  assert_of_lt_int,  eqff_to_assert,  equal_wf,  bool_cases_sqequal,  subtype_base_sq,  bool_subtype_base,  assert-bnot,  neg_assert_of_eq_int,  iff_transitivity,  assert_wf,  iff_weakening_uiff,  assert_of_band,  not_wf,  Memory-loc-class_wf,  es-locl_wf,  es-le_wf,  parallel-class-single-val,  new_23_sig_retry'base_wf,  eclass0_wf,  new_23_sig_vote'base_wf,  new_23_sig_vote2retry_wf,  disjoint-classrel-symm,  eclass0-disjoint-classrel,  base-disjoint-classrel,  name_wf,  name_eq_wf,  bnot_wf,  assert-name_eq,  assert_of_bnot,  sq_stable__encodes-msg-type,  subtype_rel_dep_function,  valueall-type_wf,  cons_wf_listp,  cons_wf,  nil_wf,  l_all_fwd,  list_wf,  new_23_sig_headers_fun_wf,  new_23_sig_headers_wf,  cons_member,  l_member_wf,  subtype_rel_weakening,  ext-eq_weakening,  eclass0-single-val,  single-valued-bag-single,  base-headers-msg-val-single-val,  listp_wf,  sq_stable__subtype_rel,  exists_wf,  Message_wf,  vatype_wf,  new_23_sig_NewRoundsState_wf,  new_23_sig_headers_type_wf
Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}notify,propose:Atom  List.  \mforall{}f:new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose).
\mforall{}es:EO+(Message(f)).  \mforall{}e1,e2:E.  \mforall{}n,round1,round2:\mBbbZ{}.
    ((\mexists{}z:\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd
          \mexists{}round:\mBbbZ{}
            \mexists{}e:E
              (e1  \mleq{}loc  e 
              \mwedge{}  (e  <loc  e2)
              \mwedge{}  z  \mmember{}  new\_23\_sig\_RoundInfo(Cmd;notify;propose;f)(e)
              \mwedge{}  round  \mmember{}  new\_23\_sig\_NewRoundsState(Cmd;notify;propose;f)  n(e)
              \mwedge{}  let  z,cmd  =  z 
                  in  let  n',round'  =  z 
                        in  (n'  =  n)  \mwedge{}  round  <  round'))
    {}\mRightarrow{}  (e1  <loc  e2)
    {}\mRightarrow{}  round1  \mmember{}  new\_23\_sig\_NewRoundsState(Cmd;notify;propose;f)  n(e1)
    {}\mRightarrow{}  round2  \mmember{}  new\_23\_sig\_NewRoundsState(Cmd;notify;propose;f)  n(e2)
    {}\mRightarrow{}  round1  <  round2)


Date html generated: 2015_07_23-PM-03_51_27
Last ObjectModification: 2015_02_04-PM-01_57_44

Home Index