---

Step * of Lemma chosen-command_wf

∀[M:Type ⟶ Type]. ∀[r:fulpRunType(P.M[P])]. ∀[t:ℕ+]. ∀[x:pInTransit(P.M[P])]. ∀[env:pEnvType(P.M[P])].
  (chosen-command(P.M[P];env;r;t;x) ∈ ℙ)
BY
{ (Auto THEN Unfold `chosen-command` 0 THEN Auto) }

1
1. M : Type ⟶ Type
2. r : fulpRunType(P.M[P])
3. t : ℕ+
4. x : pInTransit(P.M[P])
5. env : pEnvType(P.M[P])
6. Cs : component(P.M[P]) List
7. G : LabeledDAG(pInTransit(P.M[P]))
8. run-system(r;t) = <Cs, G> ∈ (component(P.M[P]) List × LabeledDAG(pInTransit(P.M[P])))
9. n : ℤ@i
10. 0 ≤ n@i
11. ↑lg-is-source(G;n)
⊢ n < lg-size(G)

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[r:fulpRunType(P.M[P])].  \mforall{}[t:\mBbbN{}\msupplus{}].  \mforall{}[x:pInTransit(P.M[P])].
\mforall{}[env:pEnvType(P.M[P])].
    (chosen-command(P.M[P];env;r;t;x)  \mmember{}  \mBbbP{})


By

---

Latex:
(Auto  THEN  Unfold  `chosen-command`  0  THEN  Auto)

---

Home Index