---

Step * 1 of Lemma first-choosable_wf


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  ∈ ℕ
BY
{ (GenConcl ⌈(snd(run-system(r;t))) = G ∈ LabeledGraph(pInTransit(P.M[P]))⌉⋅ THENA Auto) }

1
.....wf..... 
1. M : Type ─→ Type
2. t : ℕ+
3. r : ℕt ─→ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))
⊢ snd(run-system(r;t)) ∈ LabeledGraph(pInTransit(P.M[P]))

2
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  ∈ ℕ

---

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]))
\mvdash{}  if  0  <z  search(lg-size(snd(run-system(r;t)));\mlambda{}n.lg-is-source(snd(run-system(r;t));n))
    then  search(lg-size(snd(run-system(r;t)));\mlambda{}n.lg-is-source(snd(run-system(r;t));n))  -  1
    else  search(lg-size(snd(run-system(r;t)));\mlambda{}n.lg-is-source(snd(run-system(r;t));n))
    fi    \mmember{}  \mBbbN{}


By

---

Latex:
(GenConcl  \mkleeneopen{}(snd(run-system(r;t)))  =  G\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index