---

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

.....truecase..... 
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))
9. (e1 <loc (e1, e2)[n - 1])
10. ↑first((e1, e2)[n])
⊢ (before((e1, e2)[n - 1]) @ [(e1, e2)[n - 1]]) = [] ∈ (E List)
BY
{ ((Assert ⌈False⌉⋅ THEN Auto)
   THEN (InstLemma `member-es-open-interval` [⌈es⌉;⌈e1⌉;⌈e2⌉;⌈(e1, e2)[n]⌉]⋅ THENA Auto)
   THEN (D (-1) THEN Thin (-1))
   THEN D (-1)
   THEN Auto
   THEN With ⌈n⌉ (D 0)⋅
   THEN Auto) }

---

Latex:


.....truecase..... 
1.  es  :  EO
2.  e1  :  E
3.  e2  :  E
4.  n  :  \mBbbZ{}
5.  0  <  n
6.  n  <  ||(e1,  e2)||@i
7.  firstn(n  -  1;(e1,  e2))  =  (e1,  (e1,  e2)[n  -  1])
8.  firstn(n  -  1;(e1,  e2))  @  [(e1,  e2)[n  -  1]]  \msim{}  firstn(n;(e1,  e2))
9.  (e1  <loc  (e1,  e2)[n  -  1])
10.  \muparrow{}first((e1,  e2)[n])
\mvdash{}  (before((e1,  e2)[n  -  1])  @  [(e1,  e2)[n  -  1]])  =  []


By

((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (InstLemma  `member-es-open-interval`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}(e1,  e2)[n]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  (-1)  THEN  Thin  (-1))
  THEN  D  (-1)
  THEN  Auto
  THEN  With  \mkleeneopen{}n\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto)

---

Home Index