---

Step * 2 3 of Lemma rsc4-validity-property


1. Cmd : {T:Type| valueall-type(T)} 
2. cmdeq : EqDecider(Cmd)
3. locs : bag(Id)
4. clients : bag(Id)
5. coeff : {2...}
6. flrs : 
7. es : EO'
8. StandardAssumptions(rsc4_Main) es
9. e : E
10. e1:E
      ((e1 < e)
       ((v:  Cmd. (v  rsc4_decided'base(Cmd)(e1)  (e':E. ((e' < e1)  v  rsc4_propose'base(Cmd)(e')))))
          (v:    Cmd  Id
              (v  rsc4_vote'base(Cmd)(e1)
               (e':E. ((e' < e1)  <fst(fst(fst(v))), snd(fst(v))>  rsc4_propose'base(Cmd)(e')))))
          (v:    Cmd
              (v  rsc4_retry'base(Cmd)(e1)
               (e':E. ((e' < e1)  <fst(fst(v)), snd(v)>  rsc4_propose'base(Cmd)(e')))))
          (e2:E
              (e2 c e1
               (cs:Cmd List. L:Id List. n,rnd:. c:Cmd.
                    (<cs, L>  rsc4_QuorumState(Cmd) <n, rnd>(e1)
                     (c  cs)
                     (e':E. ((e' < e1)  <n, c>  rsc4_propose'base(Cmd)(e')))))))))
11. n1 : 
12. n : 
13. c1 : Cmd
14. l1 : Id
15. <<<n1, n>, c1>, l1>  rsc4_vote'base(Cmd)(e)
16. e' : E
17. (e' < e)
18. loc(e')  locs
19. loc(e)  locs
20. l1 = loc(e')
21. e1 : {e1:E| e1 loc e' } 
22. a2 : 
23. b2 :  List
24. <a2, b2>  Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e1)
25. (a2 < n1)  (n1  b2)
26. cmd : Cmd
27. e2 : {e1:E| e1 loc e' } 
28. b4 : 
29. b4  Memory-class(rsc4_update_round(Cmd) n1;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)
30. b4 < n
31. True
32. loc : Id
33. <<<n1, n>, c1>, loc>  Base(``rsc4 vote``;    Cmd  Id)(e2)
34. e' = e2
35. (no rsc4_Notify(Cmd;clients) n1 between e1 and e')
36. True
37. <n1, cmd>  Base([propose];  Cmd)(e1)
 (b1:. b3:Id. <<<n1, b1>, cmd>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e1))
 e':E. ((e' < e)  <n1, c1>  rsc4_propose'base(Cmd)(e'))
BY
{ (((InstHyp [e2] 10  THENM ExRepD) THENA MaAuto)
   THEN Try ((RepUR ``rsc4_vote'base`` -3
              THEN OnMaybeHyp 33 (\h. ((FHyp (-3) [h] THENA Auto)
                                       THEN Reduce (-1)
                                       THEN RepeatFor 3 (ParallelLast)
                                       THEN Complete (MaAuto)))
              ))
   ) }

---

1.  Cmd  :  \{T:Type|  valueall-type(T)\} 
2.  cmdeq  :  EqDecider(Cmd)
3.  locs  :  bag(Id)
4.  clients  :  bag(Id)
5.  coeff  :  \{2...\}
6.  flrs  :  \mBbbN{}
7.  es  :  EO'
8.  StandardAssumptions(rsc4\_Main)  es
9.  e  :  E
10.  \mforall{}e1:E
            ((e1  <  e)
            {}\mRightarrow{}  ((\mforall{}v:\mBbbZ{}  \mtimes{}  Cmd
                          (v  \mmember{}  rsc4\_decided'base(Cmd)(e1)
                          {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E.  ((e'  <  e1)  \mwedge{}  v  \mmember{}  rsc4\_propose'base(Cmd)(e')))))
                  \mwedge{}  (\mforall{}v:\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id
                            (v  \mmember{}  rsc4\_vote'base(Cmd)(e1)
                            {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E
                                        ((e'  <  e1)  \mwedge{}  <fst(fst(fst(v))),  snd(fst(v))>  \mmember{}  rsc4\_propose'base(Cmd)(e')))))
                  \mwedge{}  (\mforall{}v:\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd
                            (v  \mmember{}  rsc4\_retry'base(Cmd)(e1)
                            {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E.  ((e'  <  e1)  \mwedge{}  <fst(fst(v)),  snd(v)>  \mmember{}  rsc4\_propose'base(Cmd)(e')))))
                  \mwedge{}  (\mforall{}e2:E
                            (e2  c\mleq{}  e1
                            {}\mRightarrow{}  (\mforall{}cs:Cmd  List.  \mforall{}L:Id  List.  \mforall{}n,rnd:\mBbbZ{}.  \mforall{}c:Cmd.
                                        (<cs,  L>  \mmember{}  rsc4\_QuorumState(Cmd)  <n,  rnd>(e1)
                                        {}\mRightarrow{}  (c  \mmember{}  cs)
                                        {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E.  ((e'  <  e1)  \mwedge{}  <n,  c>  \mmember{}  rsc4\_propose'base(Cmd)(e')))))))))
11.  n1  :  \mBbbZ{}
12.  n  :  \mBbbZ{}
13.  c1  :  Cmd
14.  l1  :  Id
15.  <<<n1,  n>,  c1>,  l1>  \mmember{}  rsc4\_vote'base(Cmd)(e)
16.  e'  :  E
17.  (e'  <  e)
18.  loc(e')  \mdownarrow{}\mmember{}  locs
19.  loc(e)  \mdownarrow{}\mmember{}  locs
20.  l1  =  loc(e')
21.  e1  :  \{e1:E|  e1  \mleq{}loc  e'  \} 
22.  a2  :  \mBbbZ{}
23.  b2  :  \mBbbZ{}  List
24.  <a2,  b2>  \mmember{}  Memory-class(rsc4\_update\_replica(Cmd);rsc4\_init()  ɘ,  []>rsc4\_Proposal(Cmd))(e1)
25.  (a2  <  n1)  \mvee{}  (n1  \mmember{}  b2)
26.  cmd  :  Cmd
27.  e2  :  \{e1:E|  e1  \mleq{}loc  e'  \} 
28.  b4  :  \mBbbZ{}
29.  b4  \mmember{}  Memory-class(rsc4\_update\_round(Cmd)  n1;rsc4\_init()  0;rsc4\_RoundInfo(Cmd))(e2)
30.  b4  <  n
31.  True
32.  loc  :  Id
33.  <<<n1,  n>,  c1>,  loc>  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e2)
34.  e'  =  e2
35.  (no  rsc4\_Notify(Cmd;clients)  n1  between  e1  and  e')
36.  True
37.  <n1,  cmd>  \mmember{}  Base([propose];\mBbbZ{}  \mtimes{}  Cmd)(e1)
\mvee{}  (\mexists{}b1:\mBbbZ{}.  \mexists{}b3:Id.  <<<n1,  b1>,  cmd>,  b3>  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e1))
\mvdash{}  \mdownarrow{}\mexists{}e':E.  ((e'  <  e)  \mwedge{}  <n1,  c1>  \mmember{}  rsc4\_propose'base(Cmd)(e'))


By

---

(((InstHyp  [\mkleeneopen{}e2\mkleeneclose{}]  10  \mcdot{}  THENM  ExRepD)  THENA  MaAuto)
  THEN  Try  ((RepUR  ``rsc4\_vote'base``  -3
                        THEN  OnMaybeHyp  33  (\mbackslash{}h.  ((FHyp  (-3)  [h]  THENA  Auto)
                                                                          THEN  Reduce  (-1)
                                                                          THEN  RepeatFor  3  (ParallelLast)
                                                                          THEN  Complete  (MaAuto)))
                        )\mcdot{})
  )\mcdot{}



Home Index