---

Step * 1 of Lemma run-command_wf


∀M:Type ─→ Type. ∀r:pRunType(P.M[P]). ∀t,n:ℕ.  (run-command-node(r;t;n) ⇒ (run-command(r;t;n) ∈ pInTransit(P.M[P])))
BY
{ (Unfold `pRunType` 0
   THEN RepeatFor 4 ((D 0 THENA Auto))
   THEN RepUR ``run-command-node run-command`` 0
   THEN GenConclAtAddr[1;2;1;1]
   THEN RepeatFor 2 (D -2)
   THEN Reduce 0
   THEN Auto)⋅ }

---

Latex:

---

Latex:

\mforall{}M:Type  {}\mrightarrow{}  Type.  \mforall{}r:pRunType(P.M[P]).  \mforall{}t,n:\mBbbN{}.
    (run-command-node(r;t;n)  {}\mRightarrow{}  (run-command(r;t;n)  \mmember{}  pInTransit(P.M[P])))


By

---

Latex:
(Unfold  `pRunType`  0
  THEN  RepeatFor  4  ((D  0  THENA  Auto))
  THEN  RepUR  ``run-command-node  run-command``  0
  THEN  GenConclAtAddr[1;2;1;1]
  THEN  RepeatFor  2  (D  -2)
  THEN  Reduce  0
  THEN  Auto)\mcdot{}

---

Home Index