---

Step * of Lemma run-command_wf

∀[M:Type ⟶ Type]. ∀[r:pRunType(P.M[P])]. ∀[t,n:ℕ].
  run-command(r;t;n) ∈ pInTransit(P.M[P]) supposing run-command-node(r;t;n)
BY
{ RemoveUniform Auto Auto }

1
∀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])))

---

Latex:

---

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


By

---

Latex:
RemoveUniform  Auto  Auto

---

Home Index