---

Step * 1 of Lemma lg-search-property


1. [T] : Type
2. G : LabeledGraph(T)@i
3. P : T ─→ 𝔹@i
⊢ ↑isl(if (search(lg-size(G);λn.P[lg-label2(G;n)]) =z 0)
  then inr ⋅ 
  else inl (search(lg-size(G);λn.P[lg-label2(G;n)]) - 1)
  fi )
⇐⇒ ∃n:ℕlg-size(G). (↑P[lg-label2(G;n)])
BY
{ ((InstLemma `search_property` [⌈lg-size(G)⌉;⌈λn.P[lg-label2(G;n)]⌉]⋅ THENA Try (Complete (Auto)))
THENM (Reduce (-1)
       THEN AutoSplit
       THEN RepUR ``bfalse`` 0
       THEN Auto
       THEN ThinTrivial
       THEN Auto'
       THEN BackThruSomeHyp
       THEN Auto')
) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  G  :  LabeledGraph(T)@i
3.  P  :  T  {}\mrightarrow{}  \mBbbB{}@i
\mvdash{}  \muparrow{}isl(if  (search(lg-size(G);\mlambda{}n.P[lg-label2(G;n)])  =\msubz{}  0)
    then  inr  \mcdot{} 
    else  inl  (search(lg-size(G);\mlambda{}n.P[lg-label2(G;n)])  -  1)
    fi  )
\mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}lg-size(G).  (\muparrow{}P[lg-label2(G;n)])


By

---

Latex:
((InstLemma  `search\_property`  [\mkleeneopen{}lg-size(G)\mkleeneclose{};\mkleeneopen{}\mlambda{}n.P[lg-label2(G;n)]\mkleeneclose{}]\mcdot{}  THENA  Try  (Complete  (Auto)))
THENM  (Reduce  (-1)
              THEN  AutoSplit
              THEN  RepUR  ``bfalse``  0
              THEN  Auto
              THEN  ThinTrivial
              THEN  Auto'
              THEN  BackThruSomeHyp
              THEN  Auto')
)

---

Home Index