---

Step * of Lemma run-msg-commands_wf

∀[M:Type ⟶ Type]. ∀[r:pRunType(P.M[P])].  (run-msg-commands(r) ∈ Type)
BY
{ ProveWfLemma }

1
1. M : Type ⟶ Type
2. r : pRunType(P.M[P])
3. t : ℕ
4. n : ℕ
5. run-command-node(r;t;n)
⊢ com-kind(snd(snd(run-command(r;t;n)))) ∈ Atom

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[r:pRunType(P.M[P])].    (run-msg-commands(r)  \mmember{}  Type)


By

---

Latex:
ProveWfLemma

---

Home Index