---

Step * of Lemma CLK_Clock-functional

∀[MsgType:ValueAllType]. ∀[f:CLK_headers_type{i:l}(MsgType)]. ∀[es:EO+(Message(f))].  CLK_Clock(MsgType;f) is functional
BY
{ ProveEmlLemma }

---

Latex:

---

Latex:
\mforall{}[MsgType:ValueAllType].  \mforall{}[f:CLK\_headers\_type\{i:l\}(MsgType)].  \mforall{}[es:EO+(Message(f))].
    CLK\_Clock(MsgType;f)  is  functional


By

---

Latex:
ProveEmlLemma

---

Home Index