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