---

Step * of Lemma null-es-hist

∀[Info:Type]. ∀es:EO+(Info). ∀e1,e2:E.  ↑null(es-hist(es;e1;e2)) ⇐⇒ (e2 <loc e1) supposing loc(e2) = loc(e1) ∈ Id
BY
{ (((UnivCD THENA Auto) THEN Decide ⌜(e2 <loc e1)⌝⋅) THENA 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)
⊢ ↑null(es-hist(es;e1;e2)) ⇐⇒ (e2 <loc e1)

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

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}e1,e2:E.    \muparrow{}null(es-hist(es;e1;e2))  \mLeftarrow{}{}\mRightarrow{}  (e2  <loc  e1)  supposing  loc(e2)  =  loc(e1)


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  Decide  \mkleeneopen{}(e2  <loc  e1)\mkleeneclose{}\mcdot{})  THENA  Auto)

---

Home Index