---

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


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 
BY
{ ((InstLemma `member-es-open-interval` [⌈es⌉;⌈e1⌉;⌈e2⌉;⌈hd((e1, e2))⌉]⋅ THENA Auto)
   THEN (D (-1) THEN Thin (-1))
   THEN (D (-1) THENA (With ⌈0⌉ (D 0)⋅ THEN Auto THEN RWO "select0" 0 THEN Auto))
   THEN (Auto THEN (RWO "pred-hd-es-open-interval" 0 THENA Auto) THEN Auto)⋅) }

---

Latex:



1.  es  :  EO
2.  e1  :  E
3.  e2  :  E
4.  n  :  \mBbbZ{}
5.  0  <  ||(e1,  e2)||@i
\mvdash{}  (\mneg{}\muparrow{}first(hd((e1,  e2))))  \mwedge{}  pred(hd((e1,  e2)))  \mleq{}loc  e1 


By

((InstLemma  `member-es-open-interval`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}hd((e1,  e2))\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  (-1)  THEN  Thin  (-1))
  THEN  (D  (-1)  THENA  (With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  RWO  "select0"  0  THEN  Auto))
  THEN  (Auto  THEN  (RWO  "pred-hd-es-open-interval"  0  THENA  Auto)  THEN  Auto)\mcdot{})

---

Home Index