---

Step * of Lemma CLK_ClockFun_wf

∀[MsgType:ValueAllType]. ∀[f:CLK_headers_type{i:l}(MsgType)]. ∀[es:EO+(Message(f))]. ∀[e:E].
  (CLK_ClockVal(MsgType;f)@e ∈ ℤ)
BY
{ ProveEmlWfLemma }

---

Latex:

---

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


By

---

Latex:
ProveEmlWfLemma

---

Home Index