---

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


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))
⊢ (filter(λev.e1 <loc ev;before((e1, e2)[n - 1])) @ [(e1, e2)[n - 1]]) = (e1, (e1, e2)[n]) ∈ (E List)
BY
{ ((InstLemma `filter_append_sq` [⌈λev.e1 <loc ev⌉;⌈before((e1, e2)[n - 1])⌉;⌈[(e1, e2)[n - 1]]⌉]⋅ THENA Auto)
   THEN Reduce (-1)
   THEN (SplitOnHypITE (-1) THENA Auto)) }

1
.....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. filter(λev.e1 <loc ev;before((e1, e2)[n - 1]) @ [(e1, e2)[n - 1]]) ~ filter(λev.e1 <loc ev;before((e1, e2)[n - 1]))
@ [(e1, e2)[n - 1]]
10. (e1 <loc (e1, e2)[n - 1])
⊢ (filter(λev.e1 <loc ev;before((e1, e2)[n - 1])) @ [(e1, e2)[n - 1]]) = (e1, (e1, e2)[n]) ∈ (E List)

2
.....falsecase..... 
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. filter(λev.e1 <loc ev;before((e1, e2)[n - 1]) @ [(e1, e2)[n - 1]]) ~ filter(λev.e1 <loc ev;before((e1, e2)[n - 1]))
@ []
10. ¬(e1 <loc (e1, e2)[n - 1])
⊢ (filter(λev.e1 <loc ev;before((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  <  ||(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))
\mvdash{}  (filter(\mlambda{}ev.e1  <loc  ev;before((e1,  e2)[n  -  1]))  @  [(e1,  e2)[n  -  1]])  =  (e1,  (e1,  e2)[n])


By

((InstLemma  `filter\_append\_sq`  [\mkleeneopen{}\mlambda{}ev.e1  <loc  ev\mkleeneclose{};\mkleeneopen{}before((e1,  e2)[n  -  1])\mkleeneclose{};\mkleeneopen{}[(e1,  e2)[n  -  1]]\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  Reduce  (-1)
  THEN  (SplitOnHypITE  (-1)  THENA  Auto))

---

Home Index