---

Step * of Lemma new_23_sig_replica_state_mem_fun

∀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. ∀n:ℤ. ∀c:Cmd.
  ((e1 <loc e2)
  ⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e1)
  ⇒ (↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e2))))
BY
{ (Unfold `vatype` 0
   THEN (UnivCD THENA Auto)
   THEN InstLemma `new_23_sig_replica_state_mem` [⌜Cmd⌝;⌜notify⌝;⌜propose⌝;⌜slots⌝;⌜f⌝;⌜es⌝;⌜e1⌝;⌜e2⌝;
   ⌜new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1)⌝;
   ⌜new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e2)⌝;⌜<n, c>⌝]⋅
   THEN Auto
   THEN RWO "new_23_sig_ReplicaState-classrel" 0
   THEN Auto) }

---

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{}n:\mBbbZ{}.  \mforall{}c:Cmd.
    ((e1  <loc  e2)
    {}\mRightarrow{}  <n,  c>  \mmember{}  new\_23\_sig\_Proposal(Cmd;notify;propose;f)(e1)
    {}\mRightarrow{}  (\muparrow{}(set-sig-member(slots)  n  new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e2))))


By

---

Latex:
(Unfold  `vatype`  0
  THEN  (UnivCD  THENA  Auto)
  THEN  InstLemma  `new\_23\_sig\_replica\_state\_mem`  [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}notify\mkleeneclose{};\mkleeneopen{}propose\mkleeneclose{};\mkleeneopen{}slots\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};
  \mkleeneopen{}new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1)\mkleeneclose{};
  \mkleeneopen{}new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e2)\mkleeneclose{};\mkleeneopen{}<n,  c>\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  RWO  "new\_23\_sig\_ReplicaState-classrel"  0
  THEN  Auto)

---

Home Index