---

Step * 1 1 1 1 of Lemma hd-es-le-before-is-first


1. es : EO
2. e : E@i
3. ∀e1:E. ((e1 < e) ⇒ first(hd(≤loc(e1))) = tt)
4. ¬↑first(e)
5. first(hd(≤loc(pred(e)))) = tt
6. ≤loc(pred(e)) = [] ∈ ({a:E| loc(a) = loc(pred(e)) ∈ Id}  List)@i
7. null(≤loc(pred(e))) = null([])
⊢ e = hd([]) ∈ E
BY
{ (RWO "es-le-before-not-null" (-1)⋅ THEN Reduce (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  es  :  EO
2.  e  :  E@i
3.  \mforall{}e1:E.  ((e1  <  e)  {}\mRightarrow{}  first(hd(\mleq{}loc(e1)))  =  tt)
4.  \mneg{}\muparrow{}first(e)
5.  first(hd(\mleq{}loc(pred(e))))  =  tt
6.  \mleq{}loc(pred(e))  =  []@i
7.  null(\mleq{}loc(pred(e)))  =  null([])
\mvdash{}  e  =  hd([])


By

---

Latex:
(RWO  "es-le-before-not-null"  (-1)\mcdot{}  THEN  Reduce  (-1)  THEN  Auto)

---

Home Index