---

Step * 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)
⊢ hd((before(pred(e)) @ [pred(e)]) @ [e]) = fst ∈ E
BY
{ (Fold `es-le-before` 0 THEN (InstHyp [⌈pred(e)⌉;⌈fst⌉] 3⋅ THENA Auto)) }

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


By

(Fold  `es-le-before`  0  THEN  (InstHyp  [\mkleeneopen{}pred(e)\mkleeneclose{};\mkleeneopen{}fst\mkleeneclose{}]  3\mcdot{}  THENA  Auto))

---

Home Index