---

Step * 1 of Lemma choosable-command_wf


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

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  r  :  pRunType(P.M[P])
3.  t  :  \mBbbN{}\msupplus{}
4.  x  :  pInTransit(P.M[P])
5.  Cs  :  Top
6.  G  :  LabeledDAG(pInTransit(P.M[P]))
7.  (snd((r  (t  -  1))))  =  <Cs,  G>
8.  n  :  \mBbbZ{}@i
9.  0  \mleq{}  n@i
10.  \muparrow{}lg-is-source(G;n)
\mvdash{}  n  <  lg-size(G)


By

---

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

---

Home Index