---

Step * 1 1 of Lemma nth_tl-es-open-interval


1. es : EO
2. e1 : E
3. e2 : E
4. loc(e1) = loc(e2) ∈ Id
5. 0 < ||(e1, e2)||@i
6. (e1 <loc e2)
7. e : {e:E| ¬↑first(e)} 
8. e1 = pred(e) ∈ E
⊢ tl((e1, e2)) = ((e1, e2)[0], e2) ∈ (E List)
BY
{ (D (-2)
   THEN (InstLemma `es-open-interval-closed` [⌈es⌉;⌈e⌉;⌈e2⌉]⋅ THENA Auto)
   THEN (RevHypSubst' (-2) (-1) THENA Auto)) }

1
1. es : EO
2. e1 : E
3. e2 : E
4. loc(e1) = loc(e2) ∈ Id
5. 0 < ||(e1, e2)||@i
6. (e1 <loc e2)
7. e : E
8. ¬↑first(e)
9. e1 = pred(e) ∈ E
10. (e1, e2) = [e;e2) ∈ (E List)
⊢ tl((e1, e2)) = ((e1, e2)[0], e2) ∈ (E List)

---

Latex:



1.  es  :  EO
2.  e1  :  E
3.  e2  :  E
4.  loc(e1)  =  loc(e2)
5.  0  <  ||(e1,  e2)||@i
6.  (e1  <loc  e2)
7.  e  :  \{e:E|  \mneg{}\muparrow{}first(e)\} 
8.  e1  =  pred(e)
\mvdash{}  tl((e1,  e2))  =  ((e1,  e2)[0],  e2)


By

(D  (-2)
  THEN  (InstLemma  `es-open-interval-closed`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RevHypSubst'  (-2)  (-1)  THENA  Auto))

---

Home Index