---

Step * of Lemma first-success-is-inl

No Annotations
∀[T:Type]. ∀[A:T ⟶ Type]. ∀[f:x:T ⟶ (A[x]?)]. ∀[L:T List]. ∀[j:ℕ||L||]. ∀[a:A[L[j]]].
  (first-success(f;L) = (inl <j, a>) ∈ (i:ℕ||L|| × A[L[i]]?)
  ⇐⇒ j < ||L|| ∧ ((f L[j]) = (inl a) ∈ (A[L[j]]?)) ∧ (∀x∈firstn(j;L).↑isr(f x)))
BY
{ (InductionOnList
   THEN RepUR ``first-success`` 0
   THEN Try ((Fold `first-success` 0 THEN (GenConclTerm ⌜f u⌝⋅ THENA Auto) THEN D -2 THEN Reduce 0))) }

1
1. T : Type
2. A : T ⟶ Type
3. f : x:T ⟶ (A[x]?)
⊢ ∀[j:ℕ0]. ∀[a:A[⊥]].
    ((inr ⋅ ) = (inl <j, a>) ∈ (i:ℕ0 × A[⊥]?) ⇐⇒ j < 0 ∧ ((f ⊥) = (inl a) ∈ (A[⊥]?)) ∧ (∀x∈firstn(j;[]).↑isr(f x)))

2
1. T : Type
2. A : T ⟶ Type
3. f : x:T ⟶ (A[x]?)
4. u : T
5. v : T List
6. ∀[j:ℕ||v||]. ∀[a:A[v[j]]].
     (first-success(f;v) = (inl <j, a>) ∈ (i:ℕ||v|| × A[v[i]]?)
     ⇐⇒ j < ||v|| ∧ ((f v[j]) = (inl a) ∈ (A[v[j]]?)) ∧ (∀x∈firstn(j;v).↑isr(f x)))
7. x : A[u]
8. (f u) = (inl x) ∈ (A[u]?)
⊢ ∀[j:ℕ||v|| + 1]. ∀[a:A[[u / v][j]]].
    ((inl <0, x>) = (inl <j, a>) ∈ (i:ℕ||v|| + 1 × A[[u / v][i]]?)
    ⇐⇒ j < ||v|| + 1 ∧ ((f [u / v][j]) = (inl a) ∈ (A[[u / v][j]]?)) ∧ (∀x∈firstn(j;[u / v]).↑isr(f x)))

3
1. T : Type
2. A : T ⟶ Type
3. f : x:T ⟶ (A[x]?)
4. u : T
5. v : T List
6. ∀[j:ℕ||v||]. ∀[a:A[v[j]]].
     (first-success(f;v) = (inl <j, a>) ∈ (i:ℕ||v|| × A[v[i]]?)
     ⇐⇒ j < ||v|| ∧ ((f v[j]) = (inl a) ∈ (A[v[j]]?)) ∧ (∀x∈firstn(j;v).↑isr(f x)))
7. y : Unit
8. (f u) = (inr y ) ∈ (A[u]?)
⊢ ∀[j:ℕ||v|| + 1]. ∀[a:A[[u / v][j]]].
    (case first-success(f;v) of inl(p) => let i,x = p in inl <i + 1, x> | inr(z) => inr z 
     = (inl <j, a>)
     ∈ (i:ℕ||v|| + 1 × A[[u / v][i]]?)
    ⇐⇒ j < ||v|| + 1 ∧ ((f [u / v][j]) = (inl a) ∈ (A[[u / v][j]]?)) ∧ (∀x∈firstn(j;[u / v]).↑isr(f x)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[A:T  {}\mrightarrow{}  Type].  \mforall{}[f:x:T  {}\mrightarrow{}  (A[x]?)].  \mforall{}[L:T  List].  \mforall{}[j:\mBbbN{}||L||].  \mforall{}[a:A[L[j]]].
    (first-success(f;L)  =  (inl  <j,  a>)  \mLeftarrow{}{}\mRightarrow{}  j  <  ||L||  \mwedge{}  ((f  L[j])  =  (inl  a))  \mwedge{}  (\mforall{}x\mmember{}firstn(j;L).\muparrow{}isr(f  x\000C)))


By

---

Latex:
(InductionOnList
  THEN  RepUR  ``first-success``  0
  THEN  Try  ((Fold  `first-success`  0  THEN  (GenConclTerm  \mkleeneopen{}f  u\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2  THEN  Reduce  0)))

---

Home Index