---

Step * 1 2 of Lemma first-choosable_wf


1. M : Type ─→ Type
2. t : ℕ+
3. r : ℕt ─→ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))
4. G : LabeledGraph(pInTransit(P.M[P]))@i
5. (snd(run-system(r;t))) = G ∈ LabeledGraph(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  ∈ ℕ
BY
{ Auto }

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  t  :  \mBbbN{}\msupplus{}
3.  r  :  \mBbbN{}t  {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  Id  \mtimes{}  Id  \mtimes{}  pMsg(P.M[P])?  \mtimes{}  System(P.M[P]))
4.  G  :  LabeledGraph(pInTransit(P.M[P]))@i
5.  (snd(run-system(r;t)))  =  G@i
\mvdash{}  if  0  <z  search(lg-size(G);\mlambda{}n.lg-is-source(G;n))
    then  search(lg-size(G);\mlambda{}n.lg-is-source(G;n))  -  1
    else  search(lg-size(G);\mlambda{}n.lg-is-source(G;n))
    fi    \mmember{}  \mBbbN{}


By

---

Latex:
Auto

---

Home Index