---

Step * of Lemma pv11_p1_acc_fun_p2a_pv

∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
∀p:pv11_p1_Ballot_Num() × ℤ × Cmd.
  ((p ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e)))
  ⇒ (∃e':E. ∃l:Id. (e' ≤loc e  ∧ <l, p> ∈ pv11_p1_p2a'base(Cmd;f)(e'))))
BY
{ (StartEmlProof
   THEN InstLemma `pv11_p1_acc_fun_p2a` [⌈Cmd⌉;⌈f⌉;⌈es⌉;⌈e⌉;⌈ldrs_uid⌉;⌈fst(p)⌉;⌈fst(snd(p))⌉;⌈snd(snd(p))⌉]⋅
   THEN Auto
   THEN Try (Complete (RepeatFor 2 ((RWO "pair-eta<" 0 THEN Auto))))
   THEN RepeatFor 2 (ParallelLast)
   THEN Auto
   THEN RepeatFor 2 ((RWO "pair-eta<" (-2) 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{}p:pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd.
    ((p  \mmember{}  snd(pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f;es;e)))
    {}\mRightarrow{}  (\mexists{}e':E.  \mexists{}l:Id.  (e'  \mleq{}loc  e    \mwedge{}  <l,  p>  \mmember{}  pv11\_p1\_p2a'base(Cmd;f)(e'))))


By

---

Latex:
(StartEmlProof
  THEN  InstLemma  `pv11\_p1\_acc\_fun\_p2a`  [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}ldrs$_{uid}$\mkleeneclose{};\mkleeneopen{}fst(p)\000C\mkleeneclose{};\mkleeneopen{}fst(snd(p))\mkleeneclose{};
  \mkleeneopen{}snd(snd(p))\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  (RepeatFor  2  ((RWO  "pair-eta<"  0  THEN  Auto))))
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Auto
  THEN  RepeatFor  2  ((RWO  "pair-eta<"  (-2)  THEN  Auto)))

---

Home Index