---

Step * of Lemma CLK_upd_clock_wf

∀[MsgType:ValueAllType]. (CLK_upd_clock(MsgType) ∈ Id ─→ (MsgType × ℤ) ─→ ℤ ─→ ℤ)
BY
{ ProveEmlWfLemma }

---

Latex:

---

Latex:
\mforall{}[MsgType:ValueAllType].  (CLK\_upd\_clock(MsgType)  \mmember{}  Id  {}\mrightarrow{}  (MsgType  \mtimes{}  \mBbbZ{})  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{})


By

---

Latex:
ProveEmlWfLemma

---

Home Index