---

Step * 1 of Lemma chosen-command_wf


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)
BY
{ (Unfold `lg-is-source` (-1) THEN SplitOnHypITE -1  THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  r  :  fulpRunType(P.M[P])
3.  t  :  \mBbbN{}\msupplus{}
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>
9.  n  :  \mBbbZ{}@i
10.  0  \mleq{}  n@i
11.  \muparrow{}lg-is-source(G;n)
\mvdash{}  n  <  lg-size(G)


By

---

Latex:
(Unfold  `lg-is-source`  (-1)  THEN  SplitOnHypITE  -1    THEN  Auto)\mcdot{}

---

Home Index