---

Step * of Lemma es-hist-partition

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[e1,e2,e:E].
  (es-hist(es;e1;e2) = (es-hist(es;e1;pred(e)) @ es-hist(es;e;e2)) ∈ (Info List)) supposing (e ≤loc e2  and (e1 <loc e))
BY
{ (((Auto THEN Unfold `es-hist` 0 THEN RWO "map_append_sq<" 0) THENA Auto) THEN EqCD THEN Auto) }

1
.....subterm..... T:t
2:n
1. Info : Type
2. es : EO+(Info)
3. e1 : E
4. e2 : E
5. e : E
6. (e1 <loc e)
7. e ≤loc e2 
⊢ [e1, e2] = ([e1, pred(e)] @ [e, e2]) ∈ (E List)

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[e1,e2,e:E].
    (es-hist(es;e1;e2)  =  (es-hist(es;e1;pred(e))  @  es-hist(es;e;e2)))  supposing 
          (e  \mleq{}loc  e2    and 
          (e1  <loc  e))


By

(((Auto  THEN  Unfold  `es-hist`  0  THEN  RWO  "map\_append\_sq<"  0)  THENA  Auto)  THEN  EqCD  THEN  Auto)

---

Home Index