---

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


1. es : EO@i'
2. e : E@i
3. ∀e1:E. ((e1 < e) ⇒ (∀fst:E. ((↑first(fst)) ⇒ fst ≤loc e1  ⇒ (hd(≤loc(e1)) = fst ∈ E))))
4. fst : E@i
5. ↑first(fst)@i
6. fst ≤loc e @i
7. ¬↑first(e)
8. ≤loc(pred(e)) = [] ∈ ({a:E| loc(a) = loc(pred(e)) ∈ Id}  List)@i
⊢ (hd([]) = fst ∈ E) ⇒ (hd([] @ [e]) = fst ∈ E)
BY
{ (Unfold `es-le-before` (-1) THEN Auto) }

---

Latex:



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


By

(Unfold  `es-le-before`  (-1)  THEN  Auto)

---

Home Index