---

Step * of 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 = z 
     in ↑(set-sig-member(slots) n slots2))
BY
{ MemoryMemory }

---

Latex:

---

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))


By

---

Latex:
MemoryMemory

---

Home Index