---

Step * of Lemma pv11_p1_valid-LeaderState_wf

∀[Cmd:{T:Type| valueall-type(T)} ]
  ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀ldrs_uid:Id ⟶ ℤ. ∀e:E.
    (pv11_p1_valid-LeaderState(Cmd;ldrs_uid;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{}ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}.\000C  \mforall{}e:E.
        (pv11\_p1\_valid-LeaderState(Cmd;ldrs$_{uid}$;es;e;f)  \mmember{}  \mBbbP{})


By

---

Latex:
ProveEmlWfLemma

---

Home Index