---

Step * of Lemma rsc4-validity

[Cmd:ValueAllType]. [cmdeq:EqDecider(Cmd)]. [locs,clients:bag(Id)]. [coeff:{2...}]. [flrs:]. [es:EO'].
  ((StandardAssumptions(rsc4_Main) es)
   for every d in Base([notify];  Cmd) there is an
     earlier  p in rsc4_propose'base(Cmd) such that
     d = p)
BY
{ (Auto
   THEN MaAuto
   THEN (InstLemma `rsc4-validity-property`  [Cmd;cmdeq;locs;clients;coeff;flrs;es] THENA Auto)
   THEN Unfold `vatype` 1
   THEN ParallelLast
   THEN MaAuto
   THEN AllHyps h.DProduct h 
   THEN AllHyps h.((UseMessageConstraint h THENM RWO "rsc4-notify" (-1)) THENA MaAuto) 
   THEN ExRepD
   THEN OnMaybeHyp 9 (\h. (((InstHyp [e';<d1, d2>] h THENA RepUR ``rsc4_decided'base`` 0 THENA Auto) THEN Auto)
                           THEN RepeatFor 2 (ParallelLast)
                           THEN Auto
                           THEN Complete (MaAuto)))) }

---

\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  Base([notify];\mBbbZ{}  \mtimes{}  Cmd)  there  is  an
          earlier    p  in  rsc4\_propose'base(Cmd)  such  that
          d  =  p)


By

---

(Auto
  THEN  MaAuto
  THEN  (InstLemma  `rsc4-validity-property` 
              [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}cmdeq\mkleeneclose{};\mkleeneopen{}locs\mkleeneclose{};\mkleeneopen{}clients\mkleeneclose{};\mkleeneopen{}coeff\mkleeneclose{};\mkleeneopen{}flrs\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Unfold  `vatype`  1
  THEN  ParallelLast
  THEN  MaAuto
  THEN  AllHyps  h.DProduct  h\mcdot{} 
  THEN  AllHyps  h.((UseMessageConstraint  h  THENM  RWO  "rsc4-notify"  (-1))  THENA  MaAuto) 
  THEN  ExRepD
  THEN  OnMaybeHyp  9  (\mbackslash{}h.  (((InstHyp  [\mkleeneopen{}e'\mkleeneclose{};\mkleeneopen{}<d1,  d2>\mkleeneclose{}]  h\mcdot{}
                                                      THENA  RepUR  ``rsc4\_decided'base``  0
                                                      THENA  Auto)
                                                    THEN  Auto
                                                    )
                                                  THEN  RepeatFor  2  (ParallelLast)
                                                  THEN  Auto
                                                  THEN  Complete  (MaAuto)))\mcdot{})



Home Index