---

Step * 1 3 of Lemma es-interval-select


1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. k : E@i
5. (k <loc j)
6. e : E@i
7. i : ℕ@i
8. i < ||[e, k]||
9. ¬(i = 0 ∈ ℤ)
⊢ ¬↑first([e, k][i])
BY
{ (((InstLemma `l_before_select` [⌜E⌝; ⌜[e, k]⌝; ⌜i⌝; ⌜0⌝])⋅ THENA Auto')
   THEN (RWO "l_before-es-interval" (-1))
   THEN Auto) }

---

Latex:

---

Latex:

1.  es  :  EO@i'
2.  WellFnd\{i\}(E;x,y.(x  <loc  y))
3.  j  :  E@i
4.  k  :  E@i
5.  (k  <loc  j)
6.  e  :  E@i
7.  i  :  \mBbbN{}@i
8.  i  <  ||[e,  k]||
9.  \mneg{}(i  =  0)
\mvdash{}  \mneg{}\muparrow{}first([e,  k][i])


By

---

Latex:
(((InstLemma  `l\_before\_select`  [\mkleeneopen{}E\mkleeneclose{};  \mkleeneopen{}[e,  k]\mkleeneclose{};  \mkleeneopen{}i\mkleeneclose{};  \mkleeneopen{}0\mkleeneclose{}])\mcdot{}  THENA  Auto')
  THEN  (RWO  "l\_before-es-interval"  (-1))
  THEN  Auto)

---

Home Index