---

Step * of Lemma first-success_wf

∀[T:Type]. ∀[A:T ⟶ Type]. ∀[f:x:T ⟶ (A[x]?)]. ∀[L:T List].  (first-success(f;L) ∈ i:ℕ||L|| × A[L[i]]?)
BY
{ (InductionOnList THEN RepUR ``first-success`` 0 THEN Try (Fold `first-success` 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[A:T  {}\mrightarrow{}  Type].  \mforall{}[f:x:T  {}\mrightarrow{}  (A[x]?)].  \mforall{}[L:T  List].
    (first-success(f;L)  \mmember{}  i:\mBbbN{}||L||  \mtimes{}  A[L[i]]?)


By

---

Latex:
(InductionOnList  THEN  RepUR  ``first-success``  0  THEN  Try  (Fold  `first-success`  0)  THEN  Auto)

---

Home Index