---

Step * of Lemma pv11_p1_valid-ScoutState_wf

∀[Cmd:{T:Type| valueall-type(T)} ]
  ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀accpts:bag(Id). ∀b:pv11_p1_Ballot_Num(). ∀e,start:E.
    (((loc(e) = loc(start) ∈ Id) ⇒ start ≤loc e ) ⇒ (pv11_p1_valid-ScoutState(Cmd;accpts;b;start;es;e;f) ∈ ℙ))
BY
{ ProveEmlWfLemma }

---

Latex:

---

Latex:
\mforall{}[Cmd:\{T:Type|  valueall-type(T)\}  ]
    \mforall{}f:pv11\_p1\_headers\_type\{i:l\}(Cmd).  \mforall{}es:EO+(Message(f)).  \mforall{}accpts:bag(Id).  \mforall{}b:pv11\_p1\_Ballot\_Num().
    \mforall{}e,start:E.
        (((loc(e)  =  loc(start))  {}\mRightarrow{}  start  \mleq{}loc  e  )
        {}\mRightarrow{}  (pv11\_p1\_valid-ScoutState(Cmd;accpts;b;start;es;e;f)  \mmember{}  \mBbbP{}))


By

---

Latex:
ProveEmlWfLemma

---

Home Index