---

Step * 2 of Lemma null-es-hist


1. Info : Type
2. es : EO+(Info)@i'
3. e1 : E@i
4. e2 : E@i
5. loc(e2) = loc(e1) ∈ Id
6. ¬(e2 <loc e1)
⊢ ↑null(es-hist(es;e1;e2)) ⇐⇒ (e2 <loc e1)
BY
{ (Unfold `es-hist` 0 THEN RWO "null-map" 0 THEN Auto) }

1
1. Info : Type
2. es : EO+(Info)@i'
3. e1 : E@i
4. e2 : E@i
5. loc(e2) = loc(e1) ∈ Id
6. ¬(e2 <loc e1)
7. ↑null([e1, e2])@i
⊢ (e2 <loc e1)

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)@i'
3.  e1  :  E@i
4.  e2  :  E@i
5.  loc(e2)  =  loc(e1)
6.  \mneg{}(e2  <loc  e1)
\mvdash{}  \muparrow{}null(es-hist(es;e1;e2))  \mLeftarrow{}{}\mRightarrow{}  (e2  <loc  e1)


By

(Unfold  `es-hist`  0  THEN  RWO  "null-map"  0  THEN  Auto)

---

Home Index