---

Step * of Lemma first_index_property

∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].
  (↑P[L[index-of-first x in L.P[x] - 1]]) ∧ (¬(∃x∈firstn(index-of-first x in L.P[x] - 1;L). ↑P[x])) 
  supposing 0 < index-of-first x in L.P[x]
BY
{ ((UnivCD THENA Auto)
   THEN (InstLemma `search_property` [⌜||L||⌝;⌜λi.P[L[i]]⌝]⋅ THENA Auto)
   THEN Reduce (-1)
   THEN All (Unfold `first_index`)
   THEN RepeatFor 2 (D -1)
   THEN Auto
   THEN Try ((GenConclAtAddr [1;1] THEN Complete (Auto')))) }

1
1. T : Type
2. P : T ⟶ 𝔹
3. L : T List
4. 0 < search(||L||;λi.P[L[i]])
5. (∃i:ℕ||L||. (↑P[L[i]])) ⇒ 0 < search(||L||;λi.P[L[i]])
6. (∃i:ℕ||L||. (↑P[L[i]])) ⇐ 0 < search(||L||;λi.P[L[i]])
7. ↑P[L[search(||L||;λi.P[L[i]]) - 1]]
8. ∀j:ℕ||L||. ¬↑P[L[j]] supposing j < search(||L||;λi.P[L[i]]) - 1
9. ↑P[L[search(||L||;λi.P[L[i]]) - 1]]
⊢ ¬(∃x∈firstn(search(||L||;λi.P[L[i]]) - 1;L). ↑P[x])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].
    (\muparrow{}P[L[index-of-first  x  in  L.P[x]  -  1]])  \mwedge{}  (\mneg{}(\mexists{}x\mmember{}firstn(index-of-first  x  in  L.P[x]  -  1;L).  \muparrow{}P[x])) 
    supposing  0  <  index-of-first  x  in  L.P[x]


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstLemma  `search\_property`  [\mkleeneopen{}||L||\mkleeneclose{};\mkleeneopen{}\mlambda{}i.P[L[i]]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  All  (Unfold  `first\_index`)
  THEN  RepeatFor  2  (D  -1)
  THEN  Auto
  THEN  Try  ((GenConclAtAddr  [1;1]  THEN  Complete  (Auto'))))

---

Home Index