---

Step * of Lemma process-ordered-message_wf_simple

∀[M:Type]. ∀[nL:ℤ × ((ℤ × M) List)]. ∀[km:ℤ × M].  (process-ordered-message(nL;km) ∈ (ℤ × M) List × ℤ × ((ℤ × M) List))
BY
{ (ProveWfLemma THEN RepUR ``insert-ordered-message insert-combine`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[M:Type].  \mforall{}[nL:\mBbbZ{}  \mtimes{}  ((\mBbbZ{}  \mtimes{}  M)  List)].  \mforall{}[km:\mBbbZ{}  \mtimes{}  M].
    (process-ordered-message(nL;km)  \mmember{}  (\mBbbZ{}  \mtimes{}  M)  List  \mtimes{}  \mBbbZ{}  \mtimes{}  ((\mBbbZ{}  \mtimes{}  M)  List))


By

---

Latex:
(ProveWfLemma  THEN  RepUR  ``insert-ordered-message  insert-combine``  0  THEN  Auto)

---

Home Index