---

Step * 2 of Lemma firstn-es-open-interval


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)
BY
{ ((D (-2) THENA Auto)
   THEN (InstLemma `firstn_decomp` [⌈E⌉;⌈n⌉;⌈(e1, e2)⌉]⋅ THENA Auto)
   THEN RevHypSubst' (-1) 0
   THEN (HypSubst' (-2) 0 THENA Auto)) }

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

---

Latex:



1.  es  :  EO
2.  e1  :  E
3.  e2  :  E
4.  n  :  \mBbbZ{}
5.  0  <  n
6.  n  -  1  <  ||(e1,  e2)||  {}\mRightarrow{}  (firstn(n  -  1;(e1,  e2))  =  (e1,  (e1,  e2)[n  -  1]))
7.  n  <  ||(e1,  e2)||@i
\mvdash{}  firstn(n;(e1,  e2))  =  (e1,  (e1,  e2)[n])


By

((D  (-2)  THENA  Auto)
  THEN  (InstLemma  `firstn\_decomp`  [\mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}(e1,  e2)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RevHypSubst'  (-1)  0
  THEN  (HypSubst'  (-2)  0  THENA  Auto))

---

Home Index