---

Step * of Lemma lg-search-minimal

∀[T:Type]. ∀[G:LabeledGraph(T)]. ∀[P:T ⟶ 𝔹].
  ∀[n:ℕlg-size(G)]. outl(lg-search(G;x.P[x])) ≤ n supposing ↑P[lg-label(G;n)] supposing lg-exists(G;x.↑P[x])
BY
{ (Unfold `lg-exists` 0
   THEN Fold `lg-label2` 0
   THEN Auto
   THEN (InstLemma `search_property` [⌜lg-size(G)⌝;⌜λn.P[lg-label2(G;n)]⌝]⋅ THENA Auto)
   THEN Reduce (-1)
   THEN D -1
   THEN RepUR ``lg-search let`` 0
   THEN (Assert 0 < search(lg-size(G);λn.P[lg-label2(G;n)]) BY
               (BackThruSomeHyp THEN Auto))
   THEN Fold `lg-label2` 0
   THEN AutoSplit
   THEN ThinTrivial
   THEN Auto
   THEN SupposeNot
   THEN InstHyp [⌜n⌝] (-3)⋅
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[G:LabeledGraph(T)].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].
    \mforall{}[n:\mBbbN{}lg-size(G)].  outl(lg-search(G;x.P[x]))  \mleq{}  n  supposing  \muparrow{}P[lg-label(G;n)] 
    supposing  lg-exists(G;x.\muparrow{}P[x])


By

---

Latex:
(Unfold  `lg-exists`  0
  THEN  Fold  `lg-label2`  0
  THEN  Auto
  THEN  (InstLemma  `search\_property`  [\mkleeneopen{}lg-size(G)\mkleeneclose{};\mkleeneopen{}\mlambda{}n.P[lg-label2(G;n)]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  D  -1
  THEN  RepUR  ``lg-search  let``  0
  THEN  (Assert  0  <  search(lg-size(G);\mlambda{}n.P[lg-label2(G;n)])  BY
                          (BackThruSomeHyp  THEN  Auto))
  THEN  Fold  `lg-label2`  0
  THEN  AutoSplit
  THEN  ThinTrivial
  THEN  Auto
  THEN  SupposeNot
  THEN  InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  (-3)\mcdot{}
  THEN  Auto')

---

Home Index