---

Step * 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
⊢ e = hd([]) ∈ E
BY
{ (ApFunToHypEquands `Z' ⌈null(Z)⌉ ⌈𝔹⌉ (-1)⋅ THENA Auto) }

1
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

---

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
\mvdash{}  e  =  hd([])


By

(ApFunToHypEquands  `Z'  \mkleeneopen{}null(Z)\mkleeneclose{}  \mkleeneopen{}\mBbbB{}\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)

---

Home Index