---

Step * 4 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. 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'))
BY
{ (D -1 THEN (FLemma `rsc4_quorum_invariant` [-3] THENA MaAuto) THEN Reduce (-1) THEN Auto THEN ExRepD) }

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. 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. i : 
20. i < ||cs||
21. c1 = cs[i]
22. no_repeats(Id;L)
23. ||L|| = ||cs||
24. i:||L||. (e2:E. ((e2 <loc e)  <<<n2, n1>, cs[i]>, L[i]>  rsc4_vote'base(Cmd)(e2)))
 e':E. ((e' < e)  <n2, c1>  rsc4_propose'base(Cmd)(e'))

---

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.  e1  :  E
12.  e1  c\mleq{}  e
13.  cs  :  Cmd  List
14.  L  :  Id  List
15.  n2  :  \mBbbZ{}
16.  n1  :  \mBbbZ{}
17.  c1  :  Cmd
18.  <cs,  L>  \mmember{}  rsc4\_QuorumState(Cmd)  <n2,  n1>(e)
19.  (c1  \mmember{}  cs)
\mvdash{}  \mdownarrow{}\mexists{}e':E.  ((e'  <  e)  \mwedge{}  <n2,  c1>  \mmember{}  rsc4\_propose'base(Cmd)(e'))


By

---

(D  -1
  THEN  (FLemma  `rsc4\_quorum\_invariant`  [-3]  THENA  MaAuto)
  THEN  Reduce  (-1)
  THEN  Auto
  THEN  ExRepD)



Home Index