Step
*
of Lemma
can-find-first1-ext
∀[T:Type]. ∀P:T ⟶ 𝔹. ∀L:T List. ((∃x:T [first-member(T;x;L;P)]) ∨ (∀x∈L.¬↑(P x)))
BY
{ Extract of Obid: can-find-first
not unfolding list_ind subtract
finishing with Auto
normalizes to:
λP,L. 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{}P:T {}\mrightarrow{} \mBbbB{}. \mforall{}L:T List. ((\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-first
not unfolding list\_ind subtract
finishing with Auto
normalizes to:
\mlambda{}P,L. 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