---

Step * of Lemma can-find-first-ext

∀[T:Type]. ∀L:T List. ∀P:{x:T| (x ∈ L)}  ⟶ 𝔹.  ((∃x:T [first-member(T;x;L;P)]) ∨ (∀x∈L.¬↑(P x)))
BY
{ Extract of Obid: can-find-first2
  not unfolding  list_ind
  finishing with Auto
  normalizes to:
  
  λL,P. rec-case(L) of
        [] => inr (λi.Ax) 
        a::L =>
         r.case r
         of inl(z) =>
         inl if P a then a else z fi 
         | inr(none) =>
         if P a then inl a else inr (λi.if i=0 then λx.Ax else (none (i - 1)))  fi  }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}P:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbB{}.    ((\mexists{}x:T  [first-member(T;x;L;P)])  \mvee{}  (\mforall{}x\mmember{}L.\mneg{}\muparrow{}(P  x)))


By

---

Latex:
Extract  of  Obid:  can-find-first2
not  unfolding    list\_ind
finishing  with  Auto
normalizes  to:

\mlambda{}L,P.  rec-case(L)  of
            []  =>  inr  (\mlambda{}i.Ax) 
            a::L  =>
              r.case  r
              of  inl(z)  =>
              inl  if  P  a  then  a  else  z  fi 
              |  inr(none)  =>
              if  P  a  then  inl  a  else  inr  (\mlambda{}i.if  i=0  then  \mlambda{}x.Ax  else  (none  (i  -  1)))    fi 

---

Home Index