Nuprl Lemma : new_23_sig-vote

[Cmd:{T:Type| valueall-type(T)} ]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ].
[notify,propose:Atom List]. ∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)].
[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[auth:𝔹].
[k,k1:ℤ]. ∀[v:Cmd]. ∀[i1:Id].
  (<d, i, mk-msg(auth;``new_23_sig vote``;<<<k, k1>v>i1>)> ∈ new_23_sig_main()(e)
  ⇐⇒ loc(e) ↓∈ reps
      ∧ (↓∃e':{e':E| e' ≤loc 
            (((((header(e') propose ∈ Name) ∧ has-es-info-type(es;e';f;ℤ × Cmd) ∧ (<k, z2> msgval(e') ∈ (ℤ × Cmd)))
             ∨ ((header(e') ``new_23_sig vote`` ∈ Name)
               ∧ has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
               ∧ (k (fst(fst(fst(msgval(e'))))) ∈ ℤ)
               ∧ (z2 (snd(fst(msgval(e')))) ∈ Cmd)))
             ∧ (¬↑(set-sig-member(slots) new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))))
            ∧ (no new_23_sig_Notify(Cmd;clients;notify;propose;f) between e' and e)
            ∧ i ↓∈ reps
            ∧ (d 0 ∈ ℤ)
            ∧ auth ff
            ∧ (i1 loc(e) ∈ Id)
            ∧ (((k1 0 ∈ ℤ) ∧ (v z2 ∈ Cmd) ∧ (e e' ∈ E))
              ∨ (new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;k;es.e';e) < k1
                ∧ (((header(e) ``new_23_sig retry`` ∈ Name)
                  ∧ has-es-info-type(es;e;f;ℤ × ℤ × Cmd)
                  ∧ (<<k, k1>v> msgval(e) ∈ (ℤ × ℤ × Cmd)))
                  ∨ ((header(e) ``new_23_sig vote`` ∈ Name)
                    ∧ has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id)
                    ∧ (<<k, k1>v> (fst(msgval(e))) ∈ (ℤ × ℤ × Cmd)))))))))


Definitions occuring in Statement :  new_23_sig_main: new_23_sig_main() new_23_sig_ReplicaStateFun: new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e) new_23_sig_Notify: new_23_sig_Notify(Cmd;clients;notify;propose;f) new_23_sig_NewRoundsStateFun: new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;x;es;e) new_23_sig_headers_type: new_23_sig_headers_type{i:l}(Cmd;notify;propose) 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) no-classrel-in-interval: (no between start and 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 deq: EqDecider(T) cons: [a b] nil: [] list: List valueall-type: valueall-type(T) assert: b bfalse: ff bool: 𝔹 less_than: a < b uall: [x:A]. B[x] pi1: fst(t) pi2: snd(t) exists: x:A. B[x] iff: ⇐⇒ Q not: ¬A squash: T or: P ∨ Q and: P ∧ Q set: {x:A| B[x]}  apply: a pair: <a, b> product: x:A × B[x] natural_number: $n int: token: "$token" atom: Atom universe: Type equal: t ∈ T bag-member: x ↓∈ bs bag: bag(T) set-sig-member: set-sig-member(s) set-sig: set-sig{i:l}(Item)
Lemmas :  sq_stable__and equal_wf vatype_wf cons_wf_listp cons_wf nil_wf listp_wf sq_stable__equal squash_wf int_seg_wf length_wf name_wf new_23_sig_headers_wf l_all_iff l_member_wf new_23_sig_headers_fun_wf cons_member equal-wf-base list_subtype_base atom_subtype_base iff_weakening_equal name_eq_wf eqtt_to_assert assert-name_eq sq_stable__no_repeats true_wf eqff_to_assert bool_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot classrel_wf msg-interface_wf new_23_sig_main_wf make-msg-interface_wf mk-msg_wf subtype_rel_weakening ext-eq_weakening bag-member_wf es-loc_wf event-ordering+_subtype exists_wf es-E_wf es-le_wf or_wf equal-wf-T-base es-header_wf has-es-info-type_wf es-info-body_wf equal-wf-base-T int_subtype_base not_wf assert_wf set-sig-member_wf new_23_sig_ReplicaStateFun_wf no-classrel-in-interval_wf new_23_sig_Notify_wf less_than_wf new_23_sig_NewRoundsStateFun_wf eo-forward_wf member-eo-forward-E event-ordering+_wf Message_wf subtype_rel_dep_function new_23_sig_headers_type_wf set-sig_wf list_wf deq_wf bag_wf Id_wf set_wf valueall-type_wf new_23_sig-ilf eo-forward-header eo-forward-has-es-info-type new_23_sig_newvote_wf new_23_sig_QuorumStateFun_wf poss-maj_wf nat_wf make-Msg_wf eo-forward-E-subtype new_23_sig_Quorum_wf eo-forward-info-body eclass0_wf new_23_sig_decided'base_wf new_23_sig_decision_wf make-Msg-as-mk-msg mk-msg-equal bfalse_wf msg-header_wf hdrmkmsg_lemma hdrmakeMsg_lemma false_wf equal_functionality_wrt_subtype_rel2 strong-subtype-implies strong-subtype-set3 strong-subtype-eo-forward-E es-le-self member_wf and_wf subtype_rel_set

\mforall{}[Cmd:\{T:Type|  valueall-type(T)\}  ].  \mforall{}[clients:bag(Id)].  \mforall{}[cmdeq:EqDecider(Cmd)].  \mforall{}[coeff,flrs:\mBbbZ{}].
\mforall{}[notify,propose:Atom  List].  \mforall{}[reps:bag(Id)].  \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{}[e:E].  \mforall{}[d:\mBbbZ{}].
\mforall{}[i:Id].  \mforall{}[auth:\mBbbB{}].  \mforall{}[k,k1:\mBbbZ{}].  \mforall{}[v:Cmd].  \mforall{}[i1:Id].
    (<d,  i,  mk-msg(auth;``new\_23\_sig  vote``;<<<k,  k1>,  v>,  i1>)>  \mmember{}  new\_23\_sig\_main()(e)
    \mLeftarrow{}{}\mRightarrow{}  loc(e)  \mdownarrow{}\mmember{}  reps
            \mwedge{}  (\mdownarrow{}\mexists{}e':\{e':E|  e'  \mleq{}loc  e  \} 
                        (((((header(e')  =  propose)  \mwedge{}  has-es-info-type(es;e';f;\mBbbZ{}  \mtimes{}  Cmd)  \mwedge{}  (<k,  z2>  =  msgval(e')))
                          \mvee{}  ((header(e')  =  ``new\_23\_sig  vote``)
                              \mwedge{}  has-es-info-type(es;e';f;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)
                              \mwedge{}  (k  =  (fst(fst(fst(msgval(e'))))))
                              \mwedge{}  (z2  =  (snd(fst(msgval(e')))))))
                          \mwedge{}  (\mneg{}\muparrow{}(set-sig-member(slots)  k 
                        \mwedge{}  (no  new\_23\_sig\_Notify(Cmd;clients;notify;propose;f)  k  between  e'  and  e)
                        \mwedge{}  i  \mdownarrow{}\mmember{}  reps
                        \mwedge{}  (d  =  0)
                        \mwedge{}  auth  =  ff
                        \mwedge{}  (i1  =  loc(e))
                        \mwedge{}  (((k1  =  0)  \mwedge{}  (v  =  z2)  \mwedge{}  (e  =  e'))
                            \mvee{}  (new\_23\_sig\_NewRoundsStateFun(Cmd;notify;propose;f;k;es.e';e)  <  k1
                                \mwedge{}  (((header(e)  =  ``new\_23\_sig  retry``)
                                    \mwedge{}  has-es-info-type(es;e;f;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)
                                    \mwedge{}  (<<k,  k1>,  v>  =  msgval(e)))
                                    \mvee{}  ((header(e)  =  ``new\_23\_sig  vote``)
                                        \mwedge{}  has-es-info-type(es;e;f;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)
                                        \mwedge{}  (<<k,  k1>,  v>  =  (fst(msgval(e)))))))))))

Date html generated: 2015_07_23-PM-03_55_30
Last ObjectModification: 2015_02_04-PM-03_39_50

Home Index