---

Step * of Lemma new_23_sig_voter_start_unique

∀Cmd:ValueAllType. ∀propose,notify:Atom List. ∀slots:set-sig{i:l}(ℤ).
∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)). ∀n:ℤ. ∀e1,e2:E. ∀c1,c2:Cmd.
  ((¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1)))
  ⇒ <n, c1> ∈ 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)))
  ⇒ <n, c2> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e2)
  ⇒ (loc(e1) = loc(e2) ∈ Id)
  ⇒ (e1 = e2 ∈ E))
BY
{ (Unfold `vatype` 0
   THEN (UnivCD THENA Auto)
   THEN UseLoclTri ⌜es⌝⌜e1⌝⌜e2⌝⋅
   THEN Assert ⌜False⌝⋅
   THEN Auto
   THEN OnSomeHyp(\i.Complete ((Using [`slots',⌜slots⌝] (FLemma `new_23_sig_replica_state_mem_fun` [i;-1])⋅ THEN Auto)))
   ⋅) }

---

Latex:

---

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


By

---

Latex:
(Unfold  `vatype`  0
  THEN  (UnivCD  THENA  Auto)
  THEN  UseLoclTri  \mkleeneopen{}es\mkleeneclose{}\mkleeneopen{}e1\mkleeneclose{}\mkleeneopen{}e2\mkleeneclose{}\mcdot{}
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  OnSomeHyp(\mbackslash{}i.Complete  ((Using  [`slots',\mkleeneopen{}slots\mkleeneclose{}
                                                            ]  (FLemma  `new\_23\_sig\_replica\_state\_mem\_fun`  [i;-1])\mcdot{}
                                                            THEN  Auto
                                                            )))\mcdot{})

---

Home Index