---

Step * 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)
⊢ com-kind(snd(snd(run-command(r;t;n)))) ∈ Atom
BY
{ (GenConclAtAddr [2;1;1;1] THEN RepeatFor 2 (D -2) THEN Reduce 0) }

1
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

---

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)
\mvdash{}  com-kind(snd(snd(run-command(r;t;n))))  \mmember{}  Atom


By

---

Latex:
(GenConclAtAddr  [2;1;1;1]  THEN  RepeatFor  2  (D  -2)  THEN  Reduce  0)

---

Home Index