---

Step * of Lemma first-choosable_wf

∀[M:Type ─→ Type]. ∀[t:ℕ+]. ∀[r:ℕt ─→ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))].  (first-choosable(r;t) ∈ ℕ)
BY
{ ((UnivCD THENA Auto) THEN RepUR ``first-choosable let`` 0) }

1
1. M : Type ─→ Type
2. t : ℕ+
3. r : ℕt ─→ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))
⊢ if 0 <z search(lg-size(snd(run-system(r;t)));λn.lg-is-source(snd(run-system(r;t));n))
  then search(lg-size(snd(run-system(r;t)));λn.lg-is-source(snd(run-system(r;t));n)) - 1
  else search(lg-size(snd(run-system(r;t)));λn.lg-is-source(snd(run-system(r;t));n))
  fi  ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[t:\mBbbN{}\msupplus{}].  \mforall{}[r:\mBbbN{}t  {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  Id  \mtimes{}  Id  \mtimes{}  pMsg(P.M[P])?  \mtimes{}  System(P.M[P]))].
    (first-choosable(r;t)  \mmember{}  \mBbbN{})


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepUR  ``first-choosable  let``  0)

---

Home Index