---

Step * 1 of Lemma assert-es-first


1. es : EO
2. e : E
3. ↑first(e)
4. e' : E
5. loc(e') = loc(e) ∈ Id
⊢ ¬(e' < e)
BY
{ (D 0
   THEN Auto
   THEN RepeatFor 4 (MoveToConcl (-1))
   THEN (D (-1) THEN Thin (-1))
   THEN Fold `es-base-E` (-1)
   THEN Unfold `es-first` 0
   THEN MoveToConcl (-1)) }

1
1. es : EO
⊢ ∀e:es-base-E(es)
    ((↑(pred(e) = e ∨b(¬b(es-dom(es) pred(e))))) ⇒ (∀e':E. ((loc(e') = loc(e) ∈ Id) ⇒ (e' < e) ⇒ False)))

---

Latex:



1.  es  :  EO
2.  e  :  E
3.  \muparrow{}first(e)
4.  e'  :  E
5.  loc(e')  =  loc(e)
\mvdash{}  \mneg{}(e'  <  e)


By

(D  0
  THEN  Auto
  THEN  RepeatFor  4  (MoveToConcl  (-1))
  THEN  (D  (-1)  THEN  Thin  (-1))
  THEN  Fold  `es-base-E`  (-1)
  THEN  Unfold  `es-first`  0
  THEN  MoveToConcl  (-1))

---

Home Index