---

Step * 1 of Lemma first-choosable-property


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
BY
{ (InstLemma `search_property` [⌈lg-size(G)⌉;⌈λn.lg-is-source(G;n)⌉]⋅
   THEN Reduce (-1)
   THEN Auto
   THEN AutoSplit
   THEN ThinTrivial
   THEN Auto
   THEN SupposeNot
   THEN Auto
   THEN Assert ⌈¬↑lg-is-source(G;n)⌉⋅
   THEN Auto)⋅ }

1
.....wf..... 
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
8. 0 < search(lg-size(G);λn.lg-is-source(G;n))
9. ↑lg-is-source(G;search(lg-size(G);λn.lg-is-source(G;n)) - 1)
10. ∀j:ℕlg-size(G). ¬↑lg-is-source(G;j) supposing j < search(lg-size(G);λn.lg-is-source(G;n)) - 1
11. ∃i:ℕlg-size(G). (↑lg-is-source(G;i))
12. 0 < search(lg-size(G);λn.lg-is-source(G;n))
13. ¬((search(lg-size(G);λn.lg-is-source(G;n)) - 1) ≤ n)
14. ¬↑lg-is-source(G;n)
15. ↑lg-is-source(run-intransit(r;t);n)
⊢ lg-is-source(run-intransit(r;t);n) ∈ 𝔹

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  r  :  pRunType(P.M[P])
3.  t  :  \mBbbN{}\msupplus{}
4.  n  :  \mBbbN{}
5.  \muparrow{}lg-is-source(run-intransit(r;t);n)
6.  G  :  LabeledDAG(pInTransit(P.M[P]))@i
7.  run-intransit(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    \mleq{}  n


By

---

Latex:
(InstLemma  `search\_property`  [\mkleeneopen{}lg-size(G)\mkleeneclose{};\mkleeneopen{}\mlambda{}n.lg-is-source(G;n)\mkleeneclose{}]\mcdot{}
  THEN  Reduce  (-1)
  THEN  Auto
  THEN  AutoSplit
  THEN  ThinTrivial
  THEN  Auto
  THEN  SupposeNot
  THEN  Auto
  THEN  Assert  \mkleeneopen{}\mneg{}\muparrow{}lg-is-source(G;n)\mkleeneclose{}\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index