---

Step * of Lemma choosable-command_wf

∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[t:ℕ+]. ∀[x:pInTransit(P.M[P])].  (choosable-command(P.M[P];r;t;x) ∈ ℙ)
BY
{ (RepUR ``choosable-command run-system`` 0 THEN Auto) }

1
1. M : Type ─→ Type
2. r : pRunType(P.M[P])
3. t : ℕ+
4. x : pInTransit(P.M[P])
5. Cs : Top
6. G : LabeledDAG(pInTransit(P.M[P]))
7. (snd((r (t - 1)))) = <Cs, G> ∈ (Top × LabeledDAG(pInTransit(P.M[P])))
8. n : ℤ@i
9. 0 ≤ n@i
10. ↑lg-is-source(G;n)
⊢ n < lg-size(G)

---

Latex:

---

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


By

---

Latex:
(RepUR  ``choosable-command  run-system``  0  THEN  Auto)

---

Home Index