---

Step * of Lemma new_23_sig_replica_state_from_proposal_fun

∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀slots:set-sig{i:l}(ℤ). ∀n:ℤ.
  ((↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
  ⇒ (∃e':E
       ∃c:Cmd
        ((e' <loc e)
        ∧ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e')
        ∧ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))))))
BY
{ (Auto
   THEN AddMessageHeaderTypes
   THEN RepeatFor 2 (MoveToHeaderType (-1))
   THEN Try (Complete (Auto))
   THEN InstLemma `new_23_sig_replica_state_from_proposal` [⌜Cmd⌝;⌜notify⌝;⌜propose⌝;⌜f⌝;⌜es⌝;⌜e⌝;⌜slots⌝;
   ⌜new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)⌝;⌜n⌝]⋅
   THEN Auto
   THEN BLemma `new_23_sig_ReplicaState-classrel`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}notify,propose:Atom  List.  \mforall{}f:new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose).
\mforall{}es:EO+(Message(f)).  \mforall{}e:E.  \mforall{}slots:set-sig\{i:l\}(\mBbbZ{}).  \mforall{}n:\mBbbZ{}.
    ((\muparrow{}(set-sig-member(slots)  n  new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
    {}\mRightarrow{}  (\mexists{}e':E
              \mexists{}c:Cmd
                ((e'  <loc  e)
                \mwedge{}  <n,  c>  \mmember{}  new\_23\_sig\_Proposal(Cmd;notify;propose;f)(e')
                \mwedge{}  (\mneg{}\muparrow{}(set-sig-member(slots)  n 
                            new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))))))


By

---

Latex:
(Auto
  THEN  AddMessageHeaderTypes
  THEN  RepeatFor  2  (MoveToHeaderType  (-1))
  THEN  Try  (Complete  (Auto))
  THEN  InstLemma  `new\_23\_sig\_replica\_state\_from\_proposal`  [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}notify\mkleeneclose{};\mkleeneopen{}propose\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};
  \mkleeneopen{}slots\mkleeneclose{};\mkleeneopen{}new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  BLemma  `new\_23\_sig\_ReplicaState-classrel`
  THEN  Auto)

---

Home Index