---

Step * of Lemma rsc4_voter_start_unique

Cmd:ValueAllType. eq:EqDecider(Cmd). locs,clients:bag(Id). es:EO'. n,max1,max2:. missing1,missing2: List.
e1,e2:E. c1,c2:Cmd.
  (<max1, missing1>  rsc4_ReplicaState(Cmd)(e1)
   ((max1 < n)  (n  missing1))
   <n, c1>  rsc4_Proposal(Cmd)(e1)
   <max2, missing2>  rsc4_ReplicaState(Cmd)(e2)
   ((max2 < n)  (n  missing2))
   <n, c2>  rsc4_Proposal(Cmd)(e2)
   (loc(e1) = loc(e2))
   (e1 = e2))
BY
{ (Unfold `vatype` 0
   THEN (UnivCD THENA MaAuto)
   THEN UseLoclTri ese1e2
   THEN (Assert False THEN Auto)
   THEN ((FLemma `rsc4_replica_state_mem` [-6;-8;-5] THENA Complete (Auto))
   ORELSE (FLemma `rsc4_replica_state_mem` [-3;-5;-8] THENA Complete (Auto))
   )
   THEN Reduce (-1)
   THEN RWassertPDC (-1)
   THEN SquashExRepD''
   THEN Auto) }

---

\mforall{}Cmd:ValueAllType.  \mforall{}eq:EqDecider(Cmd).  \mforall{}locs,clients:bag(Id).  \mforall{}es:EO'.  \mforall{}n,max1,max2:\mBbbZ{}.
\mforall{}missing1,missing2:\mBbbZ{}  List.  \mforall{}e1,e2:E.  \mforall{}c1,c2:Cmd.
    (<max1,  missing1>  \mmember{}  rsc4\_ReplicaState(Cmd)(e1)
    {}\mRightarrow{}  ((max1  <  n)  \mvee{}  (n  \mmember{}  missing1))
    {}\mRightarrow{}  <n,  c1>  \mmember{}  rsc4\_Proposal(Cmd)(e1)
    {}\mRightarrow{}  <max2,  missing2>  \mmember{}  rsc4\_ReplicaState(Cmd)(e2)
    {}\mRightarrow{}  ((max2  <  n)  \mvee{}  (n  \mmember{}  missing2))
    {}\mRightarrow{}  <n,  c2>  \mmember{}  rsc4\_Proposal(Cmd)(e2)
    {}\mRightarrow{}  (loc(e1)  =  loc(e2))
    {}\mRightarrow{}  (e1  =  e2))


By

---

(Unfold  `vatype`  0
  THEN  (UnivCD  THENA  MaAuto)
  THEN  UseLoclTri  \mkleeneopen{}es\mkleeneclose{}\mkleeneopen{}e1\mkleeneclose{}\mkleeneopen{}e2\mkleeneclose{}\mcdot{}
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  ((FLemma  `rsc4\_replica\_state\_mem`  [-6;-8;-5]  THENA  Complete  (Auto))
  ORELSE  (FLemma  `rsc4\_replica\_state\_mem`  [-3;-5;-8]  THENA  Complete  (Auto))
  )
  THEN  Reduce  (-1)
  THEN  RWassertPDC  (-1)
  THEN  SquashExRepD''
  THEN  Auto)



Home Index