---

Step * 1 1 of Lemma run-msg-commands_wf


1. M : Type ─→ Type
2. r : pRunType(P.M[P])
3. t : ℕ
4. n : ℕ
5. run-command-node(r;t;n)
6. v1 : ℤ × Id@i
7. v3 : Id@i
8. v4 : pCom(P.M[P])@i
9. run-command(r;t;n) = <v1, v3, v4> ∈ pInTransit(P.M[P])@i
⊢ com-kind(v4) ∈ Atom
BY
{ Auto }

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  r  :  pRunType(P.M[P])
3.  t  :  \mBbbN{}
4.  n  :  \mBbbN{}
5.  run-command-node(r;t;n)
6.  v1  :  \mBbbZ{}  \mtimes{}  Id@i
7.  v3  :  Id@i
8.  v4  :  pCom(P.M[P])@i
9.  run-command(r;t;n)  =  <v1,  v3,  v4>@i
\mvdash{}  com-kind(v4)  \mmember{}  Atom


By

---

Latex:
Auto

---

Home Index