---

Step * 5 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
 e  E
BY
{ 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.  e1  :  E
12.  e1  c\mleq{}  e
13.  cs  :  Cmd  List
14.  L  :  Id  List
15.  n2  :  \mBbbZ{}
16.  n1  :  \mBbbZ{}
17.  c1  :  Cmd
\mvdash{}  e  \mmember{}  E


By

---

MaAuto



Home Index