---

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


1. es : EO
2. e1 : E
3. e2 : E
4. n : ℤ
5. 0 < ||(e1, e2)||@i
⊢ [] = (e1, (e1, e2)[0]) ∈ (E List)
BY
{ ((RWO "select0" 0 THENA Auto)
   THEN (Assert ⌈(e1, hd((e1, e2))) ~ []⌉⋅ THENM (HypSubst' (-1) 0 THEN Auto))
   THEN BLemma `es-open-interval-nil`
   THEN Auto
   THEN (OrRight THENA Auto)) }

1
1. es : EO
2. e1 : E
3. e2 : E
4. n : ℤ
5. 0 < ||(e1, e2)||@i
⊢ (¬↑first(hd((e1, e2)))) ∧ pred(hd((e1, e2))) ≤loc e1 

---

Latex:



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


By

((RWO  "select0"  0  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}(e1,  hd((e1,  e2)))  \msim{}  []\mkleeneclose{}\mcdot{}  THENM  (HypSubst'  (-1)  0  THEN  Auto))
  THEN  BLemma  `es-open-interval-nil`
  THEN  Auto
  THEN  (OrRight  THENA  Auto))

---

Home Index