---

Step * of Lemma firstn-es-open-interval

∀[es:EO]. ∀[e1,e2:E]. ∀[n:ℕ||(e1, e2)||].  (firstn(n;(e1, e2)) = (e1, (e1, e2)[n]) ∈ (E List))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert ⌜∀n:ℕ. (n < ||(e1, e2)|| ⇒ (firstn(n;(e1, e2)) = (e1, (e1, e2)[n]) ∈ (E List)))⌝⋅
   THENM (BHyp -1  THEN Auto)
   )
   THEN Thin (-1)
   THEN InductionOnNat
   THEN Reduce 0
   THEN Auto) }

1
1. es : EO
2. e1 : E
3. e2 : E
4. n : ℤ
5. 0 < ||(e1, e2)||@i
⊢ firstn(0;(e1, e2)) = (e1, (e1, e2)[0]) ∈ (E List)

2
1. es : EO
2. e1 : E
3. e2 : E
4. n : ℤ
5. 0 < n
6. n - 1 < ||(e1, e2)|| ⇒ (firstn(n - 1;(e1, e2)) = (e1, (e1, e2)[n - 1]) ∈ (E List))
7. n < ||(e1, e2)||@i
⊢ firstn(n;(e1, e2)) = (e1, (e1, e2)[n]) ∈ (E List)

---

Latex:

---

Latex:
\mforall{}[es:EO].  \mforall{}[e1,e2:E].  \mforall{}[n:\mBbbN{}||(e1,  e2)||].    (firstn(n;(e1,  e2))  =  (e1,  (e1,  e2)[n]))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  (n  <  ||(e1,  e2)||  {}\mRightarrow{}  (firstn(n;(e1,  e2))  =  (e1,  (e1,  e2)[n])))\mkleeneclose{}\mcdot{}
  THENM  (BHyp  -1    THEN  Auto)
  )
  THEN  Thin  (-1)
  THEN  InductionOnNat
  THEN  Reduce  0
  THEN  Auto)

---

Home Index