---

Step * of Lemma rsc4-validity-property

[Cmd:ValueAllType]. [cmdeq:EqDecider(Cmd)]. [locs,clients:bag(Id)]. [coeff:{2...}]. [flrs:]. [es:EO'].
  ((StandardAssumptions(rsc4_Main) es)
   for every d in rsc4_decided'base(Cmd) there is an
     earlier  p in rsc4_propose'base(Cmd) such that
     d = p)
BY
{ (Unfold `vatype` 0
   THEN Auto
   THEN Assert e:E
                  ((v:  Cmd
                      (v  rsc4_decided'base(Cmd)(e)  (e':E. ((e' < e)  v  rsc4_propose'base(Cmd)(e')))))
                   (v:    Cmd  Id
                       (v  rsc4_vote'base(Cmd)(e)
                        (e':E. ((e' < e)  <fst(fst(fst(v))), snd(fst(v))>  rsc4_propose'base(Cmd)(e')))))
                   (v:    Cmd
                       (v  rsc4_retry'base(Cmd)(e)
                        (e':E. ((e' < e)  <fst(fst(v)), snd(v)>  rsc4_propose'base(Cmd)(e')))))
                   (e1:E
                       (e1 c e
                        (cs:Cmd List. L:Id List. n,rnd:. c:Cmd.
                             (<cs, L>  rsc4_QuorumState(Cmd) <n, rnd>(e)
                              (c  cs)
                              (e':E. ((e' < e)  <n, c>  rsc4_propose'base(Cmd)(e'))))))))
   THEN Try (((D 0 THEN Auto)
              THEN InstHyp [e] (-4)
              THEN Auto
              THEN FHyp (-4) [-5]
              THEN Auto
              THEN (RepeatFor 2 (ParallelLast) THEN Auto)
              THEN With d (D 0)
              THEN Auto))
   THEN (CausalInd'
         THEN Auto
         THEN Try ((UseMessageConstraint (-1) THENA MaAuto))
         THEN RepeatFor 3 (AllHyps h.DProduct h )
         THEN RenameTypedVars [,`n';Cmd,`c']
         THEN (RWW "rsc4-retry rsc4-vote rsc4-decided" (-1) THENA MaAuto)
         THEN SquashExRepD
         THEN Reduce 0)) }

1
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. n : 
12. c : Cmd
13. <n, c>  rsc4_decided'base(Cmd)(e)
14. e' : E
15. (e' < e)
16. loc(e')  locs
17. loc(e) = loc(e')
18. e1 : {e1:E| e1 loc e' } 
19. a : 
20. a2 : 
21. b2 :  List
22. <a2, b2>  Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e1)
23. (a2 < a)  (a  b2)
24. b : Cmd
25. True
26. <a, b>  Base([propose];  Cmd)(e1)
 (b1:. b3:Id. <<<a, b1>, b>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e1))
27. ((b1:
        b2:Cmd
         b3:Id
          (<<<n, b1>, b2>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e')
           (a2:Cmd List
              ((((||a2|| = (coeff * flrs))  ((fst(poss-maj(cmdeq;[b2 / a2];b2))) = ((coeff * flrs) + 1)))
               (c = (snd(poss-maj(cmdeq;[b2 / a2];b2)))))
               (b4:Id List
                  (<a2, b4>  Memory-class(rsc4_add_to_quorum(Cmd) <a, 0>;rsc4_init() <[], []>;rsc4_vote'base(Cmd))(e')
                   ((rsc4_newvote(Cmd) <a, 0> <<<n, b1>, b2>, b3> <a2, b4>))))))))
 ((no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e1 and e')))
 ((e2:{e1:E| e1 loc e' } 
      b:
       (((((no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b> between e2 and e'))
        (b1:
            b2:Cmd
             b3:Id
              (<<<n, b1>, b2>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e')
               (a2:Cmd List
                  ((((||a2|| = (coeff * flrs))  ((fst(poss-maj(cmdeq;[b2 / a2];b2))) = ((coeff * flrs) + 1)))
                   (c = (snd(poss-maj(cmdeq;[b2 / a2];b2)))))
                   (b4:Id List
                      (<a2, b4>  Memory-class(rsc4_add_to_quorum(Cmd) <a, b>;rsc4_init() <[], []>;rsc4_vote'base(Cmd))(
                                  e')
                       ((rsc4_newvote(Cmd) <a, b> <<<n, b1>, b2>, b3> <a2, b4>)))))))))
        (b1:Cmd
           (<<a, b>, b1>  Base(``rsc4 retry``;    Cmd)(e2)
            (b5:Id. <<<a, b>, b1>, b5>  Base(``rsc4 vote``;    Cmd  Id)(e2)))))
        (b4:. (b4  Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)  (b4 < b)))))
   (no rsc4_Notify(Cmd;clients) a between e1 and e'))
 e':E. ((e' < e)  <n, c>  rsc4_propose'base(Cmd)(e'))

2
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. c : Cmd
14. v2 : Id
15. <<<n1, n>, c>, v2>  rsc4_vote'base(Cmd)(e)
16. e' : E
17. (e' < e)
18. loc(e')  locs
19. loc(e)  locs
20. v2 = 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. b : Cmd
27. ((e' = e1)  (c = b)  (n = 0))
 ((e2:{e1:E| e1 loc e' } 
      (((b4:. (b4  Memory-class(rsc4_update_round(Cmd) n1;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)  (b4 < n)))
       (<<n1, n>, c>  Base(``rsc4 retry``;    Cmd)(e2)
         (b5:Id. <<<n1, n>, c>, b5>  Base(``rsc4 vote``;    Cmd  Id)(e2))))
       (e' = e2)))
   (no rsc4_Notify(Cmd;clients) n1 between e1 and e'))
28. True
29. <n1, b>  Base([propose];  Cmd)(e1)
 (b1:. b3:Id. <<<n1, b1>, b>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e1))
 e':E. ((e' < e)  <n1, c>  rsc4_propose'base(Cmd)(e'))

3
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. c : Cmd
14. <<n1, n>, c>  rsc4_retry'base(Cmd)(e)
15. e' : E
16. (e' < e)
17. loc(e')  locs
18. loc(e) = loc(e')
19. e1 : {e1:E| e1 loc e' } 
20. a : 
21. a2 : 
22. b2 :  List
23. <a2, b2>  Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e1)
24. (a2 < a)  (a  b2)
25. b : Cmd
26. True
27. <a, b>  Base([propose];  Cmd)(e1)
 (b1:. b3:Id. <<<a, b1>, b>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e1))
28. ((b1:
        ((n = (b1 + 1))
         (b2:Cmd
            b3:Id
             (<<<n1, b1>, b2>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e')
              (a2:Cmd List
                 ((((||a2|| = (coeff * flrs))  (((fst(poss-maj(cmdeq;[b2 / a2];b2))) = ((coeff * flrs) + 1))))
                  (c = (snd(poss-maj(cmdeq;[b2 / a2];b2)))))
                  (b4:Id List
                     (<a2, b4>  Memory-class(rsc4_add_to_quorum(Cmd) <a, 0>;rsc4_init() <[], []>;rsc4_vote'base(Cmd))(
                                 e')
                      ((rsc4_newvote(Cmd) <a, 0> <<<n1, b1>, b2>, b3> <a2, b4>))))))))))
 ((no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e1 and e')))
 ((e2:{e1:E| e1 loc e' } 
      b:
       ((((b4:. (b4  Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)  (b4 < b)))
        (b1:Cmd
           (<<a, b>, b1>  Base(``rsc4 retry``;    Cmd)(e2)
            (b5:Id. <<<a, b>, b1>, b5>  Base(``rsc4 vote``;    Cmd  Id)(e2)))))
        (b1:
            ((n = (b1 + 1))
             (b2:Cmd
                b3:Id
                 (<<<n1, b1>, b2>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e')
                  (a2:Cmd List
                     ((((||a2|| = (coeff * flrs))  (((fst(poss-maj(cmdeq;[b2 / a2];b2))) = ((coeff * flrs) + 1))))
                      (c = (snd(poss-maj(cmdeq;[b2 / a2];b2)))))
                      (b4:Id List
                         (<a2, b4>  Memory-class(rsc4_add_to_quorum(Cmd) <a, b>;rsc4_init() 
                                                                                 <[], []>;rsc4_vote'base(Cmd))(e')
                          ((rsc4_newvote(Cmd) <a, b> <<<n1, b1>, b2>, b3> <a2, b4>)))))))))))
        ((no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b> between e2 and e'))))
   (no rsc4_Notify(Cmd;clients) a between e1 and e'))
 e':E. ((e' < e)  <n1, c>  rsc4_propose'base(Cmd)(e'))

4
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. e1 : E
12. e1 c e
13. cs : Cmd List
14. L : Id List
15. n2 : 
16. n1 : 
17. c1 : Cmd
18. <cs, L>  rsc4_QuorumState(Cmd) <n2, n1>(e)
19. (c1  cs)
 e':E. ((e' < e)  <n2, c1>  rsc4_propose'base(Cmd)(e'))

5
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. e1 : E
12. e1 c e
13. cs : Cmd List
14. L : Id List
15. n2 : 
16. n1 : 
17. c1 : Cmd
 e  E

---

\mforall{}[Cmd:ValueAllType].  \mforall{}[cmdeq:EqDecider(Cmd)].  \mforall{}[locs,clients:bag(Id)].  \mforall{}[coeff:\{2...\}].  \mforall{}[flrs:\mBbbN{}].
\mforall{}[es:EO'].
    ((StandardAssumptions(rsc4\_Main)  es)
    {}\mRightarrow{}  for  every  d  in  rsc4\_decided'base(Cmd)  there  is  an
          earlier    p  in  rsc4\_propose'base(Cmd)  such  that
          d  =  p)


By

---

(Unfold  `vatype`  0
  THEN  Auto
  THEN  Assert  \mkleeneopen{}\mforall{}e:E
                                ((\mforall{}v:\mBbbZ{}  \mtimes{}  Cmd
                                        (v  \mmember{}  rsc4\_decided'base(Cmd)(e)
                                        {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E.  ((e'  <  e)  \mwedge{}  v  \mmember{}  rsc4\_propose'base(Cmd)(e')))))
                                \mwedge{}  (\mforall{}v:\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id
                                          (v  \mmember{}  rsc4\_vote'base(Cmd)(e)
                                          {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E
                                                      ((e'  <  e)
                                                      \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)(e)
                                          {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E.  ((e'  <  e)  \mwedge{}  <fst(fst(v)),  snd(v)>  \mmember{}  rsc4\_propose'base(Cmd)(e')))))
                                \mwedge{}  (\mforall{}e1:E
                                          (e1  c\mleq{}  e
                                          {}\mRightarrow{}  (\mforall{}cs:Cmd  List.  \mforall{}L:Id  List.  \mforall{}n,rnd:\mBbbZ{}.  \mforall{}c:Cmd.
                                                      (<cs,  L>  \mmember{}  rsc4\_QuorumState(Cmd)  <n,  rnd>(e)
                                                      {}\mRightarrow{}  (c  \mmember{}  cs)
                                                      {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E.  ((e'  <  e)  \mwedge{}  <n,  c>  \mmember{}  rsc4\_propose'base(Cmd)(e'))))))))\mkleeneclose{}\mcdot{}
  THEN  Try  (((D  0\mcdot{}  THEN  Auto)
                        THEN  InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-4)\mcdot{}
                        THEN  Auto
                        THEN  FHyp  (-4)  [-5]
                        THEN  Auto
                        THEN  (RepeatFor  2  (ParallelLast)  THEN  Auto)
                        THEN  With  \mkleeneopen{}d\mkleeneclose{}  (D  0)\mcdot{}
                        THEN  Auto)\mcdot{})
  THEN  (CausalInd'
              THEN  Auto
              THEN  Try  ((UseMessageConstraint  (-1)  THENA  MaAuto))
              THEN  RepeatFor  3  (AllHyps  h.DProduct  h\mcdot{}  )
              THEN  RenameTypedVars  [\mkleeneopen{}\mBbbZ{}\mkleeneclose{},`n';\mkleeneopen{}Cmd\mkleeneclose{},`c']\mcdot{}
              THEN  (RWW  "rsc4-retry  rsc4-vote  rsc4-decided"  (-1)  THENA  MaAuto)
              THEN  SquashExRepD
              THEN  Reduce  0)\mcdot{})



Home Index