---

Step * of Lemma CLK_Clock-classrel

∀[MsgType:ValueAllType]. ∀[f:CLK_headers_type{i:l}(MsgType)].
  ∀es:EO+(Message(f)). ∀e:E. ∀v:ℤ.  (v ∈ CLK_Clock(MsgType;f)(e) ⇐⇒ v = CLK_ClockVal(MsgType;f)@e ∈ ℤ)
BY
{ ProveEmlLemma }

---

Latex:

---

Latex:
\mforall{}[MsgType:ValueAllType].  \mforall{}[f:CLK\_headers\_type\{i:l\}(MsgType)].
    \mforall{}es:EO+(Message(f)).  \mforall{}e:E.  \mforall{}v:\mBbbZ{}.    (v  \mmember{}  CLK\_Clock(MsgType;f)(e)  \mLeftarrow{}{}\mRightarrow{}  v  =  CLK\_ClockVal(MsgType;f)@e)


By

---

Latex:
ProveEmlLemma

---

Home Index