---

Step * of Lemma first-choosable-property

∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[t:ℕ+]. ∀[n:ℕ].
  first-choosable(r;t) ≤ n supposing ↑lg-is-source(run-intransit(r;t);n)
BY
{ (Intros
   THEN Try ((GenConclTerm ⌈run-intransit(r;t)⌉⋅ THEN Auto))
   THEN (Unhide THENA Auto)
   THEN ((RepUR ``first-choosable let`` 0 THEN Fold `run-intransit` 0)
         THEN (GenConcl ⌈run-intransit(r;t) = G ∈ LabeledDAG(pInTransit(P.M[P]))⌉⋅
               THENA (Auto THEN GenConclAtAddr [2;1] THEN D -2 THEN Auto)
               )
         THEN Auto)⋅) }

1
1. M : Type ─→ Type
2. r : pRunType(P.M[P])
3. t : ℕ+
4. n : ℕ
5. ↑lg-is-source(run-intransit(r;t);n)
6. G : LabeledDAG(pInTransit(P.M[P]))@i
7. run-intransit(r;t) = G ∈ LabeledDAG(pInTransit(P.M[P]))@i
⊢ if 0 <z search(lg-size(G);λn.lg-is-source(G;n))
  then search(lg-size(G);λn.lg-is-source(G;n)) - 1
  else search(lg-size(G);λn.lg-is-source(G;n))
  fi  ≤ n

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[r:pRunType(P.M[P])].  \mforall{}[t:\mBbbN{}\msupplus{}].  \mforall{}[n:\mBbbN{}].
    first-choosable(r;t)  \mleq{}  n  supposing  \muparrow{}lg-is-source(run-intransit(r;t);n)


By

---

Latex:
(Intros
  THEN  Try  ((GenConclTerm  \mkleeneopen{}run-intransit(r;t)\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Unhide  THENA  Auto)
  THEN  ((RepUR  ``first-choosable  let``  0  THEN  Fold  `run-intransit`  0)
              THEN  (GenConcl  \mkleeneopen{}run-intransit(r;t)  =  G\mkleeneclose{}\mcdot{}
                          THENA  (Auto  THEN  GenConclAtAddr  [2;1]  THEN  D  -2  THEN  Auto)
                          )
              THEN  Auto)\mcdot{})

---

Home Index