---

Step * 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. hd(≤loc(pred(e))) = fst ∈ E
⊢ hd(≤loc(pred(e)) @ [e]) = fst ∈ E
BY
{ (MoveToConcl (-1) THEN GenConclAtAddr [1;2;1] THEN D -2) }

1
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)

2
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)

---

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.  hd(\mleq{}loc(pred(e)))  =  fst
\mvdash{}  hd(\mleq{}loc(pred(e))  @  [e])  =  fst


By

(MoveToConcl  (-1)  THEN  GenConclAtAddr  [1;2;1]  THEN  D  -2)

---

Home Index