---

Step * of Lemma pv11_p1_acc_fun_p2a

∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ⟶ ℤ.
∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀c:Cmd.
  ((<b, s, c> ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e)))
  ⇒ (∃e':E. ∃l:Id. (e' ≤loc e  ∧ <l, b, s, c> ∈ pv11_p1_p2a'base(Cmd;f)(e'))))
BY
{ (StartEmlProof
   THEN (InstLemma `pv11_p1_acc_p2a` [⌜Cmd⌝;⌜f⌝;⌜es⌝;⌜e⌝;⌜ldrs_uid⌝;⌜pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e)⌝;⌜b⌝;
         ⌜s⌝;⌜c⌝]⋅
         THENA (Auto THEN BLemma `pv11_p1_AcceptorState-classrel` THEN Auto)
         )
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN GenConclAtAddr [1;2;1]
   THEN D -2
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}f:pv11\_p1\_headers\_type\{i:l\}(Cmd).  \mforall{}es:EO+(Message(f)).  \mforall{}e:E.  \mforall{}ldrs$_\mbackslash{}ff7\000Cbuid}$:Id  {}\mrightarrow{}  \mBbbZ{}.
\mforall{}b:pv11\_p1\_Ballot\_Num().  \mforall{}s:\mBbbZ{}.  \mforall{}c:Cmd.
    ((<b,  s,  c>  \mmember{}  snd(pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f;es;e)))
    {}\mRightarrow{}  (\mexists{}e':E.  \mexists{}l:Id.  (e'  \mleq{}loc  e    \mwedge{}  <l,  b,  s,  c>  \mmember{}  pv11\_p1\_p2a'base(Cmd;f)(e'))))


By

---

Latex:
(StartEmlProof
  THEN  (InstLemma  `pv11\_p1\_acc\_p2a`  [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}ldrs$_{uid}$\mkleeneclose{};
              \mkleeneopen{}pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f;es;e)\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  BLemma  `pv11\_p1\_AcceptorState-classrel`  THEN  Auto)
              )
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  GenConclAtAddr  [1;2;1]
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto)

---

Home Index