---

Step * of Lemma last-es-hist

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[e1,e2:E].  last(es-hist(es;e1;e2)) ~ info(e2) supposing e1 ≤loc e2 
BY
{ ((((UnivCD THENA Auto) THEN Unfold `es-hist` 0 THEN RWO "last-map" 0) THENA Auto) THEN Reduce 0) }

1
1. Info : Type
2. es : EO+(Info)
3. e1 : E
4. e2 : E
5. e1 ≤loc e2 
⊢ ¬↑null([e1, e2])

2
1. Info : Type
2. es : EO+(Info)
3. e1 : E
4. e2 : E
5. e1 ≤loc e2 
⊢ info(last([e1, e2])) ~ info(e2)

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[e1,e2:E].    last(es-hist(es;e1;e2))  \msim{}  info(e2)  supposing  e1  \mleq{}loc  e2 


By

((((UnivCD  THENA  Auto)  THEN  Unfold  `es-hist`  0  THEN  RWO  "last-map"  0)  THENA  Auto)  THEN  Reduce  0)

---

Home Index