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