---

Step * of Lemma CLK_msg'base_wf

∀[MsgType:ValueAllType]. ∀[f:CLK_headers_type{i:l}(MsgType)].  (CLK_msg'base(MsgType;f) ∈ EClass(MsgType × ℤ))
BY
{ ProveEmlWfLemma }

---

Latex:

---

Latex:
\mforall{}[MsgType:ValueAllType].  \mforall{}[f:CLK\_headers\_type\{i:l\}(MsgType)].
    (CLK\_msg'base(MsgType;f)  \mmember{}  EClass(MsgType  \mtimes{}  \mBbbZ{}))


By

---

Latex:
ProveEmlWfLemma

---

Home Index