---

Step * 1 1 of Lemma first-choosable-property

.....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) ∈ 𝔹
BY
{ (GenConclAtAddr [2;1] THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
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
8.  0  <  search(lg-size(G);\mlambda{}n.lg-is-source(G;n))
9.  \muparrow{}lg-is-source(G;search(lg-size(G);\mlambda{}n.lg-is-source(G;n))  -  1)
10.  \mforall{}j:\mBbbN{}lg-size(G).  \mneg{}\muparrow{}lg-is-source(G;j)  supposing  j  <  search(lg-size(G);\mlambda{}n.lg-is-source(G;n))  -  1
11.  \mexists{}i:\mBbbN{}lg-size(G).  (\muparrow{}lg-is-source(G;i))
12.  0  <  search(lg-size(G);\mlambda{}n.lg-is-source(G;n))
13.  \mneg{}((search(lg-size(G);\mlambda{}n.lg-is-source(G;n))  -  1)  \mleq{}  n)
14.  \mneg{}\muparrow{}lg-is-source(G;n)
15.  \muparrow{}lg-is-source(run-intransit(r;t);n)
\mvdash{}  lg-is-source(run-intransit(r;t);n)  \mmember{}  \mBbbB{}


By

---

Latex:
(GenConclAtAddr  [2;1]  THEN  Auto)

---

Home Index