Nuprl Lemma : new_23_sig-ilf
(∀[z1:ℤ]. ∀[propose,notify:Atom List]. ∀[clients:bag(Id)]. ∀[Cmd:{T:Type| valueall-type(T)} ].
 ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[m:Message(f)].
   {<d, i, m> ∈ new_23_sig_Notify(Cmd;clients;notify;propose;f) z1(e)
   
⇐⇒ (no (new_23_sig_decision(Cmd;clients;notify;propose;f) 
            z1 o new_23_sig_decided'base(Cmd;notify;propose;f)) prior to e)
       ∧ <d, i, m> ∈
          {(new_23_sig_decision(Cmd;clients;notify;propose;f) z1 o new_23_sig_decided'base(Cmd;notify;propose;f))}(e)})
∧ (∀[z6,z1:ℤ]. ∀[reps:bag(Id)]. ∀[propose,notify:Atom List]. ∀[flrs,coeff:ℤ]. ∀[Cmd:{T:Type| valueall-type(T)} ].
   ∀[cmdeq:EqDecider(Cmd)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E].
   ∀[d:ℤ]. ∀[i:Id]. ∀[m:Message(f)].
     {<d, i, m> ∈ new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <z1, z6>(e)
     
⇐⇒ ((header(e) = ``new_23_sig vote`` ∈ Name) ∧ has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id))
         ∧ (↑(new_23_sig_newvote(Cmd) <z1, z6> msgval(e) new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es;e)))
         ∧ (||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es;e))|| = (coeff * flrs) ∈ ℤ)
         ∧ (d = 0 ∈ ℤ)
         ∧ (↓(((fst(poss-maj(cmdeq;[snd(fst(msgval(e))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>e\000Cs;e)))];snd(fst(msgval(e)))))) = ((coeff * flrs) + 1) ∈ ℤ)
             ∧ i ↓∈ reps
             ∧ (m
               = make-Msg(``new_23_sig decided``;<fst(fst(fst(msgval(e))))
                                                 , snd(poss-maj(cmdeq;[snd(fst(msgval(e))) / 
                                                                       (fst(new_23_sig_QuorumStateFun(Cmd;...;...;f;<z1
                                                                                                                    , z6
                                                                                                                    >es\000C;e)))];snd(fst(msgval(e)))))
                                                 >)
               ∈ Message(f)))
             ∨ ((¬((fst(poss-maj(cmdeq;[snd(fst(msgval(e))) / 
                                        (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es;e)))];snd(fst(ms\000Cgval(e))))))
                = ((coeff * flrs) + 1)
                ∈ ℤ))
               ∧ (i = loc(e) ∈ Id)
               ∧ (m
                 = make-Msg(``new_23_sig retry``;<<fst(fst(fst(msgval(e)))), (snd(fst(fst(msgval(e))))) + 1>
                                                 , snd(poss-maj(cmdeq;[snd(fst(msgval(e))) / 
                                                                       (fst(new_23_sig_QuorumStateFun(Cmd;...;...;f;<z1
                                                                                                                    , z6
                                                                                                                    >es\000C;e)))];snd(fst(msgval(e)))))
                                                 >)
                 ∈ Message(f))))})
∧ (∀[z1:ℤ]. ∀[propose,notify:Atom List]. ∀[clients:bag(Id)]. ∀[Cmd:{T:Type| valueall-type(T)} ].
   ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id].
   ∀[m:Message(f)].
     {<d, i, m> ∈
       (new_23_sig_decision(Cmd;clients;notify;propose;f) z1 o new_23_sig_decided'base(Cmd;notify;propose;f))(e)
     
⇐⇒ (header(e) = ``new_23_sig decided`` ∈ Name)
         ∧ has-es-info-type(es;e;f;ℤ × Cmd)
         ∧ ((fst(msgval(e))) = z1 ∈ ℤ)
         ∧ i ↓∈ clients
         ∧ (d = 0 ∈ ℤ)
         ∧ (m = make-Msg(notify;msgval(e)) ∈ Message(f))})
∧ (∀[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].
   ∀[m:Message(f)].
     {<d, i, m> ∈ new_23_sig_main()(e)
     
⇐⇒ loc(e) ↓∈ reps
         ∧ (↓∃e':{e':E| e' ≤loc e } 
              ∃z1:ℤ
               ∃z2:Cmd
                (((((header(e') = propose ∈ Name)
                ∧ has-es-info-type(es;e';f;ℤ × Cmd)
                ∧ (<z1, z2> = msgval(e') ∈ (ℤ × Cmd)))
                ∨ ((header(e') = ``new_23_sig vote`` ∈ Name)
                  ∧ has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
                  ∧ (z1 = (fst(fst(fst(msgval(e'))))) ∈ ℤ)
                  ∧ (z2 = (snd(fst(msgval(e')))) ∈ Cmd)))
                ∧ (¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))))
                ∧ (((no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e' and e)
                  ∧ ((((i ↓∈ reps ∧ (d = 0 ∈ ℤ) ∧ (m = make-Msg(``new_23_sig vote``;<<<z1, 0>, z2>, loc(e)>) ∈ Message(f\000C))) ∧ (e = e' ∈ E))
                    ∨ ((no new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <z1, 0> between e' and e)
                      ∧ <d, i, m> ∈ {new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <z1, 0>}(e)))
                    ∨ (∃e1:{e1:E| e1 ≤loc e } 
                        ∃z6:ℤ
                         ∃z7:Cmd
                          (new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e';e1) < z6
                          ∧ (((header(e1) = ``new_23_sig retry`` ∈ Name)
                            ∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd)
                            ∧ (<<z1, z6>, z7> = msgval(e1) ∈ (ℤ × ℤ × Cmd)))
                            ∨ ((header(e1) = ``new_23_sig vote`` ∈ Name)
                              ∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
                              ∧ (<<z1, z6>, z7> = (fst(msgval(e1))) ∈ (ℤ × ℤ × Cmd))))
                          ∧ (((... ↓∈ ... ∧ ...) ∧ ...) ∨ ...)))))
                  ∨ ...)))})
Proof
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_decision: new_23_sig_decision(Cmd;clients;notify;propose;f)
, 
new_23_sig_NewRoundsStateFun: new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;x;es;e)
, 
new_23_sig_Quorum: new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f)
, 
new_23_sig_QuorumStateFun: new_23_sig_QuorumStateFun(Cmd;notify;propose;f;x;es;e)
, 
new_23_sig_newvote: new_23_sig_newvote(Cmd)
, 
new_23_sig_decided'base: new_23_sig_decided'base(Cmd;notify;propose;f)
, 
new_23_sig_headers_type: new_23_sig_headers_type{i:l}(Cmd;notify;propose)
, 
msg-interface: Interface
, 
make-Msg: make-Msg(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)
, 
eclass0: (f o X)
, 
no-classrel-in-interval: (no X between start and e)
, 
no-prior-classrel: (no X prior to 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
, 
poss-maj: poss-maj(eq;L;x)
, 
deq: EqDecider(T)
, 
length: ||as||
, 
cons: [a / b]
, 
nil: []
, 
list: T List
, 
valueall-type: valueall-type(T)
, 
assert: ↑b
, 
less_than: a < b
, 
uall: ∀[x:A]. B[x]
, 
guard: {T}
, 
pi1: fst(t)
, 
pi2: snd(t)
, 
exists: ∃x:A. B[x]
, 
iff: P 
⇐⇒ Q
, 
not: ¬A
, 
squash: ↓T
, 
or: P ∨ Q
, 
and: P ∧ Q
, 
set: {x:A| B[x]} 
, 
apply: f a
, 
pair: <a, b>
, 
product: x:A × B[x]
, 
multiply: n * m
, 
add: n + m
, 
natural_number: $n
, 
int: ℤ
, 
token: "$token"
, 
atom: Atom
, 
universe: Type
, 
equal: s = 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, 
bool_wf, 
eqtt_to_assert, 
assert-name_eq, 
sq_stable__no_repeats, 
true_wf, 
eqff_to_assert, 
bool_cases_sqequal, 
subtype_base_sq, 
bool_subtype_base, 
assert-bnot, 
classrel_wf, 
msg-interface_wf, 
eclass0_wf, 
new_23_sig_decided'base_wf, 
new_23_sig_decision_wf, 
es-locl_wf, 
new_23_sig_Notify_wf, 
make-msg-interface_wf, 
no-prior-classrel_wf, 
es-E_wf, 
event-ordering+_subtype, 
event-ordering+_wf, 
Message_wf, 
subtype_rel_dep_function, 
new_23_sig_headers_type_wf, 
valueall-type_wf, 
bag_wf, 
Id_wf, 
list_wf, 
once-classrel-weak, 
assert_witness, 
es-info-body_wf, 
new_23_sig_newvote_wf, 
new_23_sig_QuorumStateFun_wf, 
new_23_sig_Quorum_wf, 
deq_wf, 
iff_transitivity, 
iff_weakening_uiff, 
eclass2-eclass1-classrel, 
new_23_sig_when_quorum_wf, 
new_23_sig_vote'base_wf, 
new_23_sig_QuorumState_wf, 
base-classrel-equal, 
subtype_rel_weakening, 
ext-eq_weakening, 
new_23_sig_QuorumState-classrel, 
has-es-info-type_wf, 
exists_wf, 
bag-member_wf, 
es-loc_wf, 
equal-wf-T-base, 
es-header_wf, 
bag-member-ifthenelse, 
empty-bag_wf, 
ifthenelse_functionality_wrt_iff, 
false_wf, 
bag-member-empty-weak, 
bag-member-spread-to-pi, 
eq_int_wf, 
nat_wf, 
bag-member-single-weak, 
bag-member-map, 
ifthenelse-false-right, 
new_23_sig_roundout_wf, 
assert_wf, 
poss-maj_wf, 
assert_of_eq_int, 
mk-msg-interface_wf, 
make-Msg_wf, 
neg_assert_of_eq_int, 
new_23_sig_retry'send_wf, 
new_23_sig_decided'broadcast_wf, 
single-bag_wf, 
subtype_rel_product, 
top_wf, 
sq_stable__bag-member, 
sq_stable__has-es-info-type, 
squash-assert, 
member_wf, 
int_subtype_base, 
bool_cases, 
not_wf, 
or_wf, 
eclass0-base-classrel, 
new_23_sig_notify'broadcast_wf, 
pair-eta, 
subtype_rel_transitivity, 
es-info-type_wf, 
pi1_wf_top, 
new_23_sig_main_wf, 
set-sig_wf, 
classrel-at, 
new_23_sig_Replica_wf, 
bind-class-rel-weak, 
new_23_sig_NewVoters_wf, 
new_23_sig_Voter_wf, 
set-sig-set_wf, 
new_23_sig_when_new_proposal_wf, 
new_23_sig_Proposal_wf, 
new_23_sig_ReplicaState_wf, 
parallel-classrel-weak, 
new_23_sig_propose'base_wf, 
new_23_sig_vote2prop_wf, 
new_23_sig_ReplicaState-classrel, 
new_23_sig_ReplicaStateFun_wf, 
eo-forward_wf, 
until-classrel, 
new_23_sig_Rounds_wf, 
new_23_sig_Round_wf, 
bind-class_wf, 
new_23_sig_NewRounds_wf, 
once-class_wf, 
return-loc-bag-class-classrel, 
new_23_sig_when_new_round_wf, 
new_23_sig_RoundInfo_wf, 
new_23_sig_NewRoundsState_wf, 
new_23_sig_retry'base_wf, 
new_23_sig_vote2retry_wf, 
new_23_sig_NewRoundsState-classrel, 
equal-wf-base-T, 
new_23_sig_NewRoundsStateFun_wf, 
return-loc-bag-class_wf, 
new_23_sig_vote'broadcast_wf, 
sq_or_wf, 
until-class_wf, 
es-interface-subtype_rel2, 
subtype_top, 
member-eo-forward-E, 
es-first_wf2, 
eo-forward-header, 
eo-forward-has-es-info-type, 
eo-forward-info-body, 
eo-forward-E-subtype, 
es-le_wf, 
set-sig-member_wf, 
ifthenelse-false-left, 
lt_int_wf, 
assert_of_lt_int, 
less_than_wf, 
assert_of_band, 
and_wf, 
eo-forward-no-prior-classrel, 
eo-forward-loc, 
eo-forward-first2, 
no-classrel-in-interval_wf, 
eo-forward-le, 
uiff_transitivity, 
equal-eo-forward-E, 
eo-forward-no-classrel-in-interval, 
es-le-loc, 
decidable__es-le, 
eo-forward-le2, 
subtype_rel_sets, 
eo-forward-forward2
Latex:
(\mforall{}[z1:\mBbbZ{}].  \mforall{}[propose,notify:Atom  List].  \mforall{}[clients:bag(Id)].  \mforall{}[Cmd:\{T:Type|  valueall-type(T)\}  ].
  \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{}[m:Message(f)].
      \{<d,  i,  m>  \mmember{}  new\_23\_sig\_Notify(Cmd;clients;notify;propose;f)  z1(e)
      \mLeftarrow{}{}\mRightarrow{}  (no  (new\_23\_sig\_decision(Cmd;clients;notify;propose;f) 
                        z1  o  new\_23\_sig\_decided'base(Cmd;notify;propose;f))  prior  to  e)
              \mwedge{}  <d,  i,  m>  \mmember{}
                    \{(new\_23\_sig\_decision(Cmd;clients;notify;propose;f) 
                        z1  o  new\_23\_sig\_decided'base(Cmd;notify;propose;f))\}(e)\})
\mwedge{}  (\mforall{}[z6,z1:\mBbbZ{}].  \mforall{}[reps:bag(Id)].  \mforall{}[propose,notify:Atom  List].  \mforall{}[flrs,coeff:\mBbbZ{}].
      \mforall{}[Cmd:\{T:Type|  valueall-type(T)\}  ].  \mforall{}[cmdeq:EqDecider(Cmd)].
      \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{}[m:Message(f)].
          \{<d,  i,  m>  \mmember{}  new\_23\_sig\_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f)  <z1,  z6>(e)
          \mLeftarrow{}{}\mRightarrow{}  ((header(e)  =  ``new\_23\_sig  vote``)  \mwedge{}  has-es-info-type(es;e;f;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id))
                  \mwedge{}  (\muparrow{}(new\_23\_sig\_newvote(Cmd)  <z1,  z6>  msgval(e)  new\_23\_sig\_QuorumStateFun(Cmd;notify;propos\000Ce;f;<z1,  z6>es;e)))
                  \mwedge{}  (||fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1,  z6>es;e))||  =  (coeff  *  flrs))
                  \mwedge{}  (d  =  0)
                  \mwedge{}  (\mdownarrow{}(((fst(poss-maj(cmdeq;[snd(fst(msgval(e)))  / 
                                                                        (fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1,  z6>es;\000Ce)))];snd(fst(msgval(e))))))
                            =  ((coeff  *  flrs)  +  1))
                          \mwedge{}  i  \mdownarrow{}\mmember{}  reps
                          \mwedge{}  (m
                              =  make-Msg(``new\_23\_sig  decided``;<fst(fst(fst(msgval(e))))
                                                                                                  ,  snd(poss-maj(cmdeq;[snd(fst(msgval(e)))  / 
                                                                                                                                              (fst(...))];snd(fst(...))))
                                                                                                  >)))
                          \mvee{}  ((\mneg{}((fst(poss-maj(cmdeq;[snd(fst(msgval(e)))  / 
                                                                                (fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1,  z6>\000C;es;e)))];snd(fst(msgval(e))))))
                                =  ((coeff  *  flrs)  +  1)))
                              \mwedge{}  (i  =  loc(e))
                              \mwedge{}  (m
                                  =  make-Msg(``new\_23\_sig  retry``;<<fst(fst(fst(msgval(e))))
                                                                                                    ,  (snd(fst(fst(msgval(e)))))  +  1
                                                                                                    >
                                                                                                  ,  snd(poss-maj(cmdeq;[snd(fst(msgval(e)))  / 
                                                                                                                                              (fst(...))];snd(fst(...))))
                                                                                                  >))))\})
\mwedge{}  (\mforall{}[z1:\mBbbZ{}].  \mforall{}[propose,notify:Atom  List].  \mforall{}[clients:bag(Id)].  \mforall{}[Cmd:\{T:Type|  valueall-type(T)\}  ].
      \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{}[m:Message(f)].
          \{<d,  i,  m>  \mmember{}
              (new\_23\_sig\_decision(Cmd;clients;notify;propose;f) 
                z1  o  new\_23\_sig\_decided'base(Cmd;notify;propose;f))(e)
          \mLeftarrow{}{}\mRightarrow{}  (header(e)  =  ``new\_23\_sig  decided``)
                  \mwedge{}  has-es-info-type(es;e;f;\mBbbZ{}  \mtimes{}  Cmd)
                  \mwedge{}  ((fst(msgval(e)))  =  z1)
                  \mwedge{}  i  \mdownarrow{}\mmember{}  clients
                  \mwedge{}  (d  =  0)
                  \mwedge{}  (m  =  make-Msg(notify;msgval(e)))\})
\mwedge{}  (\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{}[m:Message(f)].
          \{<d,  i,  m>  \mmember{}  new\_23\_sig\_main()(e)
          \mLeftarrow{}{}\mRightarrow{}  loc(e)  \mdownarrow{}\mmember{}  reps
                  \mwedge{}  (\mdownarrow{}\mexists{}e':\{e':E|  e'  \mleq{}loc  e  \} 
                            \mexists{}z1:\mBbbZ{}
                              \mexists{}z2:Cmd
                                (((((header(e')  =  propose)
                                \mwedge{}  has-es-info-type(es;e';f;\mBbbZ{}  \mtimes{}  Cmd)
                                \mwedge{}  (<z1,  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{}  (z1  =  (fst(fst(fst(msgval(e'))))))
                                    \mwedge{}  (z2  =  (snd(fst(msgval(e')))))))
                                \mwedge{}  (\mneg{}\muparrow{}(set-sig-member(slots)  z1 
                                            new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))))
                                \mwedge{}  (((no  new\_23\_sig\_Notify(Cmd;clients;notify;propose;f)  z1  between  e'  and  e)
                                    \mwedge{}  ((((i  \mdownarrow{}\mmember{}  reps
                                        \mwedge{}  (d  =  0)
                                        \mwedge{}  (m  =  make-Msg(``new\_23\_sig  vote``;<<<z1,  0>,  z2>,  loc(e)>)))
                                        \mwedge{}  (e  =  e'))
                                        \mvee{}  ((no  new\_23\_sig\_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f)  <z1,  0>  bet\000Cween  e'  and  e)
                                            \mwedge{}  <d,  i,  m>  \mmember{}  \{new\_23\_sig\_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) 
                                                                          <z1,  0>\}(e)))
                                        \mvee{}  (\mexists{}e1:\{e1:E|  e1  \mleq{}loc  e  \} 
                                                \mexists{}z6:\mBbbZ{}
                                                  \mexists{}z7:Cmd
                                                    (new\_23\_sig\_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e';e1)  <  z6
                                                    \mwedge{}  (((header(e1)  =  ``new\_23\_sig  retry``)
                                                        \mwedge{}  has-es-info-type(es;e1;f;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)
                                                        \mwedge{}  (<<z1,  z6>,  z7>  =  msgval(e1)))
                                                        \mvee{}  ((header(e1)  =  ``new\_23\_sig  vote``)
                                                            \mwedge{}  has-es-info-type(es;e1;f;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)
                                                            \mwedge{}  (<<z1,  z6>,  z7>  =  (fst(msgval(e1))))))
                                                    \mwedge{}  (((i  \mdownarrow{}\mmember{}  reps
                                                        \mwedge{}  (d  =  0)
                                                        \mwedge{}  (m  =  make-Msg(``new\_23\_sig  vote``;<<<z1,  z6>,  z7>,  loc(e)>)))
                                                        \mwedge{}  (e  =  e1))
                                                        \mvee{}  ((no  new\_23\_sig\_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) 
                                                                      <z1,  z6>  between  e1  and  e)
                                                            \mwedge{}  <d,  i,  m>  \mmember{}
                                                                  \{new\_23\_sig\_Quorum(Cmd;cmdeq;coeff;flrs;...;...;...;...)  ...\}(
                                                                  ...)))))))
                                    \mvee{}  ...)))\})
Date html generated:
2015_07_23-PM-03_55_13
Last ObjectModification:
2015_02_04-PM-03_35_14
Home
Index