---

Step * of Lemma CLK_messages-delivered_wf

∀[MsgType:ValueAllType]. ∀[locs:bag(Id)]. ∀[reply:Id ─→ MsgType ─→ (MsgType × Id)]. ∀[f:CLK_headers_type{i:l}(MsgType)].
  (CLK_messages-delivered{i:l}(MsgType;locs;reply;f) ∈ ℙ')
BY
{ ProveEmlWfLemma }

---

Latex:

---

Latex:
\mforall{}[MsgType:ValueAllType].  \mforall{}[locs:bag(Id)].  \mforall{}[reply:Id  {}\mrightarrow{}  MsgType  {}\mrightarrow{}  (MsgType  \mtimes{}  Id)].
\mforall{}[f:CLK\_headers\_type\{i:l\}(MsgType)].
    (CLK\_messages-delivered\{i:l\}(MsgType;locs;reply;f)  \mmember{}  \mBbbP{}')


By

---

Latex:
ProveEmlWfLemma

---

Home Index