---

Step * 1 of Lemma first-choosable-property2


1. M : Type ─→ Type
2. r : pRunType(P.M[P])
3. t : ℕ+
4. G : LabeledDAG(pInTransit(P.M[P]))@i
5. run-intransit(r;t) = G ∈ LabeledDAG(pInTransit(P.M[P]))@i
6. (∃i:ℕlg-size(G). (↑lg-is-source(G;i))) ⇒ 0 < search(lg-size(G);λn.lg-is-source(G;n))
7. (∃i:ℕlg-size(G). (↑lg-is-source(G;i))) ⇐ 0 < search(lg-size(G);λn.lg-is-source(G;n))
8. (↑lg-is-source(G;search(lg-size(G);λn.lg-is-source(G;n)) - 1))
   ∧ (∀j:ℕlg-size(G). ¬↑lg-is-source(G;j) supposing j < search(lg-size(G);λn.lg-is-source(G;n)) - 1) 
   supposing 0 < search(lg-size(G);λn.lg-is-source(G;n))
9. n : ℕ@i
10. ↑lg-is-source(G;n)
⊢ ↑lg-is-source(G;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
{ ((D (-5)
    THENA (Auto THEN With ⌈n⌉ (D 0)⋅ THEN Auto THEN (RepUR ``lg-is-source`` (-1) THEN SplitOnHypITE -1  THEN Auto)⋅)
    )
   THEN AutoSplit
   ) }

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  r  :  pRunType(P.M[P])
3.  t  :  \mBbbN{}\msupplus{}
4.  G  :  LabeledDAG(pInTransit(P.M[P]))@i
5.  run-intransit(r;t)  =  G@i
6.  (\mexists{}i:\mBbbN{}lg-size(G).  (\muparrow{}lg-is-source(G;i)))  {}\mRightarrow{}  0  <  search(lg-size(G);\mlambda{}n.lg-is-source(G;n))
7.  (\mexists{}i:\mBbbN{}lg-size(G).  (\muparrow{}lg-is-source(G;i)))  \mLeftarrow{}{}  0  <  search(lg-size(G);\mlambda{}n.lg-is-source(G;n))
8.  (\muparrow{}lg-is-source(G;search(lg-size(G);\mlambda{}n.lg-is-source(G;n))  -  1))
      \mwedge{}  (\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) 
      supposing  0  <  search(lg-size(G);\mlambda{}n.lg-is-source(G;n))
9.  n  :  \mBbbN{}@i
10.  \muparrow{}lg-is-source(G;n)
\mvdash{}  \muparrow{}lg-is-source(G;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  )


By

---

Latex:
((D  (-5)
    THENA  (Auto
                  THEN  With  \mkleeneopen{}n\mkleeneclose{}  (D  0)\mcdot{}
                  THEN  Auto
                  THEN  (RepUR  ``lg-is-source``  (-1)  THEN  SplitOnHypITE  -1    THEN  Auto)\mcdot{})
    )
  THEN  AutoSplit
  )

---

Home Index