---

Step * of Lemma pv11_p1_valid-proposal-transitivity

∀[Cmd:{T:Type| valueall-type(T)} ]
  ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀p:ℤ × Cmd.
    (pv11_p1_valid-proposal(Cmd;es;e;p;f) ⇒ (∀e':E. (e c≤ e' ⇒ pv11_p1_valid-proposal(Cmd;es;e';p;f))))
BY
{ (Auto THEN RepeatFor 4 (ParallelOp -3) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Cmd:\{T:Type|  valueall-type(T)\}  ]
    \mforall{}f:pv11\_p1\_headers\_type\{i:l\}(Cmd).  \mforall{}es:EO+(Message(f)).  \mforall{}e:E.  \mforall{}p:\mBbbZ{}  \mtimes{}  Cmd.
        (pv11\_p1\_valid-proposal(Cmd;es;e;p;f)
        {}\mRightarrow{}  (\mforall{}e':E.  (e  c\mleq{}  e'  {}\mRightarrow{}  pv11\_p1\_valid-proposal(Cmd;es;e';p;f))))


By

---

Latex:
(Auto  THEN  RepeatFor  4  (ParallelOp  -3)  THEN  Auto)

---

Home Index