---

Step * 1 1 2 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. u : {a:E| loc(a) = loc(pred(e)) ∈ Id} 
9. v : {a:E| loc(a) = loc(pred(e)) ∈ Id}  List
10. ≤loc(pred(e)) = [u / v] ∈ ({a:E| loc(a) = loc(pred(e)) ∈ Id}  List)@i
⊢ (hd([u / v]) = fst ∈ E) ⇒ (hd([u / v] @ [e]) = fst ∈ E)
BY
{ (Reduce 0 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.  u  :  \{a:E|  loc(a)  =  loc(pred(e))\} 
9.  v  :  \{a:E|  loc(a)  =  loc(pred(e))\}    List
10.  \mleq{}loc(pred(e))  =  [u  /  v]@i
\mvdash{}  (hd([u  /  v])  =  fst)  {}\mRightarrow{}  (hd([u  /  v]  @  [e])  =  fst)


By

(Reduce  0  THEN  Auto)

---

Home Index