---

Step * of Lemma es-hist-last

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[e1,e2:E].
  es-hist(es;e1;e2) = (es-hist(es;e1;pred(e2)) @ [info(e2)]) ∈ (Info List) supposing (e1 <loc e2)
BY
{ (Auto
   THEN AssertBY ⌈es-hist(es;e1;e2) = (es-hist(es;e1;pred(e2)) @ es-hist(es;e2;e2)) ∈ (Info List)⌉
     (BLemma `es-hist-partition`⋅ THEN Auto)⋅
   THEN (NthHypSq (-1))
   THEN RepeatFor 2 ((EqCD THEN Try (Trivial)))) }

1
1. Info : Type
2. es : EO+(Info)
3. e1 : E
4. e2 : E
5. (e1 <loc e2)
6. es-hist(es;e1;e2) = (es-hist(es;e1;pred(e2)) @ es-hist(es;e2;e2)) ∈ (Info List)
⊢ [info(e2)] ~ es-hist(es;e2;e2)

---

Latex:


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


By

(Auto
  THEN  AssertBY  \mkleeneopen{}es-hist(es;e1;e2)  =  (es-hist(es;e1;pred(e2))  @  es-hist(es;e2;e2))\mkleeneclose{}
      (BLemma  `es-hist-partition`\mcdot{}  THEN  Auto)\mcdot{}
  THEN  (NthHypSq  (-1))
  THEN  RepeatFor  2  ((EqCD  THEN  Try  (Trivial))))

---

Home Index