---

Step * of Lemma pv11_p1_scout_fun_from_acc

∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀accpts:bag(Id).
∀b:pv11_p1_Ballot_Num(). ∀p:pv11_p1_Ballot_Num() × ℤ × Cmd.
  ((p ∈ snd(pv11_p1_ScoutStateFun(Cmd;accpts;f;b;es;e)))
  ⇒ (∃e':E
       ∃l:Id
        ∃r:(pv11_p1_Ballot_Num() × ℤ × Cmd) List. (e' ≤loc e  ∧ <l, b, b, r> ∈ pv11_p1_p1b'base(Cmd;f)(e') ∧ (p ∈ r))))
BY
{ (StartEmlProof
   THEN (InstLemma `pv11_p1_scout_from_acc` [⌈Cmd⌉;⌈f⌉;⌈es⌉;⌈e⌉;⌈accpts⌉;⌈pv11_p1_ScoutStateFun(Cmd;accpts;f;b;es;e)⌉;
         ⌈b⌉]⋅
         THENA (Auto THEN BLemma `pv11_p1_ScoutState-classrel` THEN Auto)
         )
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN GenConclAtAddr [1;2;1]
   THEN D -2
   THEN Reduce 0
   THEN Auto
   THEN BHyp (-1)
   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{}accpts:bag(Id).
\mforall{}b:pv11\_p1\_Ballot\_Num().  \mforall{}p:pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd.
    ((p  \mmember{}  snd(pv11\_p1\_ScoutStateFun(Cmd;accpts;f;b;es;e)))
    {}\mRightarrow{}  (\mexists{}e':E
              \mexists{}l:Id
                \mexists{}r:(pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List
                  (e'  \mleq{}loc  e    \mwedge{}  <l,  b,  b,  r>  \mmember{}  pv11\_p1\_p1b'base(Cmd;f)(e')  \mwedge{}  (p  \mmember{}  r))))


By

---

Latex:
(StartEmlProof
  THEN  (InstLemma  `pv11\_p1\_scout\_from\_acc`  [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}accpts\mkleeneclose{};
              \mkleeneopen{}pv11\_p1\_ScoutStateFun(Cmd;accpts;f;b;es;e)\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  BLemma  `pv11\_p1\_ScoutState-classrel`  THEN  Auto)
              )
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  GenConclAtAddr  [1;2;1]
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto
  THEN  BHyp  (-1)
  THEN  Auto)

---

Home Index