---

Step * of Lemma new_23_sig-notify

∀[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:ℤ]. ∀[v:Cmd].
  (<d, i, mk-msg(auth;notify;<k, v>)> ∈ new_23_sig_main()(e)
  ⇐⇒ loc(e) ↓∈ reps
      ∧ (↓∃z2:Cmd
           ∃e':{e':E| e' ≤loc e } 
            ((header(e) = ``new_23_sig decided`` ∈ Name)
            ∧ has-es-info-type(es;e;f;ℤ × Cmd)
            ∧ i ↓∈ clients
            ∧ (d = 0 ∈ ℤ)
            ∧ auth = ff
            ∧ (<k, v> = msgval(e) ∈ (f notify))
            ∧ (((header(e') = propose ∈ Name)
              ∧ has-es-info-type(es;e';f;ℤ × Cmd)
              ∧ (<fst(msgval(e)), z2> = msgval(e') ∈ (ℤ × Cmd)))
              ∨ ((header(e') = ``new_23_sig vote`` ∈ Name)
                ∧ has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
                ∧ ((fst(msgval(e))) = (fst(fst(fst(msgval(e'))))) ∈ ℤ)
                ∧ (z2 = (snd(fst(msgval(e')))) ∈ Cmd)))
            ∧ (¬↑(set-sig-member(slots) (fst(msgval(e))) new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e')))
            ∧ (no (new_23_sig_decision(Cmd;clients;notify;propose;f) 
                   (fst(msgval(e))) o new_23_sig_decided'base(Cmd;notify;propose;f)) between e' and e))))
BY
{ ProveILF_instance "notify""new_23_sig" }

---

Latex:

---

Latex:
\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:\mBbbZ{}].  \mforall{}[v:Cmd].
    (<d,  i,  mk-msg(auth;notify;<k,  v>)>  \mmember{}  new\_23\_sig\_main()(e)
    \mLeftarrow{}{}\mRightarrow{}  loc(e)  \mdownarrow{}\mmember{}  reps
            \mwedge{}  (\mdownarrow{}\mexists{}z2:Cmd
                      \mexists{}e':\{e':E|  e'  \mleq{}loc  e  \} 
                        ((header(e)  =  ``new\_23\_sig  decided``)
                        \mwedge{}  has-es-info-type(es;e;f;\mBbbZ{}  \mtimes{}  Cmd)
                        \mwedge{}  i  \mdownarrow{}\mmember{}  clients
                        \mwedge{}  (d  =  0)
                        \mwedge{}  auth  =  ff
                        \mwedge{}  (<k,  v>  =  msgval(e))
                        \mwedge{}  (((header(e')  =  propose)
                            \mwedge{}  has-es-info-type(es;e';f;\mBbbZ{}  \mtimes{}  Cmd)
                            \mwedge{}  (<fst(msgval(e)),  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{}  ((fst(msgval(e)))  =  (fst(fst(fst(msgval(e'))))))
                                \mwedge{}  (z2  =  (snd(fst(msgval(e')))))))
                        \mwedge{}  (\mneg{}\muparrow{}(set-sig-member(slots)  (fst(msgval(e))) 
                                    new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e')))
                        \mwedge{}  (no  (new\_23\_sig\_decision(Cmd;clients;notify;propose;f) 
                                      (fst(msgval(e)))  o  new\_23\_sig\_decided'base(Cmd;notify;propose;f))  between  e'  and
                              e))))


By

---

Latex:
ProveILF\_instance  "notify""new\_23\_sig"

---

Home Index