---

Step * of Lemma first-choosable-property2

∀[M:Type ⟶ Type]. ∀[r:pRunType(P.M[P])]. ∀[t:ℕ+]. ∀[n:ℕ].
  ↑lg-is-source(run-intransit(r;t);first-choosable(r;t)) supposing ↑lg-is-source(run-intransit(r;t);n)
BY
{ (BasicUniformUnivCD Auto
   THEN UseWitness ⌜Ax⌝⋅
   THEN MoveToConcl (-1)
   THEN (RepUR ``first-choosable let`` 0 THEN Fold `run-intransit` 0)
   THEN (GenConcl ⌜run-intransit(r;t) = G ∈ LabeledDAG(pInTransit(P.M[P]))⌝⋅
         THENA (Auto THEN GenConclAtAddr [2;1] THEN D -2 THEN Auto)
         )
   THEN InstLemma `search_property` [⌜lg-size(G)⌝;⌜λn.lg-is-source(G;n)⌝]⋅
   THEN Reduce (-1)
   THEN Auto) }

1
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 )

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[r:pRunType(P.M[P])].  \mforall{}[t:\mBbbN{}\msupplus{}].  \mforall{}[n:\mBbbN{}].
    \muparrow{}lg-is-source(run-intransit(r;t);first-choosable(r;t)) 
    supposing  \muparrow{}lg-is-source(run-intransit(r;t);n)


By

---

Latex:
(BasicUniformUnivCD  Auto
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  MoveToConcl  (-1)
  THEN  (RepUR  ``first-choosable  let``  0  THEN  Fold  `run-intransit`  0)
  THEN  (GenConcl  \mkleeneopen{}run-intransit(r;t)  =  G\mkleeneclose{}\mcdot{}
              THENA  (Auto  THEN  GenConclAtAddr  [2;1]  THEN  D  -2  THEN  Auto)
              )
  THEN  InstLemma  `search\_property`  [\mkleeneopen{}lg-size(G)\mkleeneclose{};\mkleeneopen{}\mlambda{}n.lg-is-source(G;n)\mkleeneclose{}]\mcdot{}
  THEN  Reduce  (-1)
  THEN  Auto)

---

Home Index