---

Step * of Lemma lg-search-property

∀[T:Type]. ∀G:LabeledGraph(T). ∀P:T ⟶ 𝔹.  (↑isl(lg-search(G;x.P[x])) ⇐⇒ lg-exists(G;x.↑P[x]))
BY
{ ((UnivCD THENA Auto) THEN (RepUR ``lg-search let lg-exists`` 0 THEN Fold `lg-label2` 0)) }

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}G:LabeledGraph(T).  \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.    (\muparrow{}isl(lg-search(G;x.P[x]))  \mLeftarrow{}{}\mRightarrow{}  lg-exists(G;x.\muparrow{}P[x]))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RepUR  ``lg-search  let  lg-exists``  0  THEN  Fold  `lg-label2`  0))

---

Home Index