---

Step * of Lemma isl-first-success

∀[T:Type]. ∀[A:T ⟶ Type].
  ∀f:x:T ⟶ (A[x]?). ∀L:T List.
    ((↑isl(first-success(f;L)))
    ⇒ (fst(outl(first-success(f;L))) < ||L||
       ∧ ((f L[fst(outl(first-success(f;L)))])
         = (inl (snd(outl(first-success(f;L)))))
         ∈ (A[L[fst(outl(first-success(f;L)))]]?))
       ∧ (∀x∈firstn(fst(outl(first-success(f;L)));L).↑isr(f x))))
BY
{ (Intros
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜first-success(f;L)⌝⋅ THENA Auto)
   THEN RepeatFor 2 (D -2)
   THEN Reduce 0
   THEN (D 0 THENA Auto)
   THEN Try (FalseHD (-1))
   THEN InstLemma `first-success-is-inl` [⌜T⌝;⌜A⌝;⌜f⌝;⌜L⌝;⌜i⌝;⌜x1⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[A:T  {}\mrightarrow{}  Type].
    \mforall{}f:x:T  {}\mrightarrow{}  (A[x]?).  \mforall{}L:T  List.
        ((\muparrow{}isl(first-success(f;L)))
        {}\mRightarrow{}  (fst(outl(first-success(f;L)))  <  ||L||
              \mwedge{}  ((f  L[fst(outl(first-success(f;L)))])  =  (inl  (snd(outl(first-success(f;L))))))
              \mwedge{}  (\mforall{}x\mmember{}firstn(fst(outl(first-success(f;L)));L).\muparrow{}isr(f  x))))


By

---

Latex:
(Intros
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}first-success(f;L)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (D  -2)
  THEN  Reduce  0
  THEN  (D  0  THENA  Auto)
  THEN  Try  (FalseHD  (-1))
  THEN  InstLemma  `first-success-is-inl`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index