---

Step * of Lemma es-closed-open-interval-decomp-last

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[e1,e2:E].  [e1;e2) = ([e1;pred(e2)) @ [pred(e2)]) ∈ (E List) supposing (e1 <loc e2)
BY
{ (Auto
   THEN (RW (AddrC [2] (LemmaC `es-closed-open-interval-eq-before`)) 0 THENA Auto)
   THEN (RW (AddrC [2] (LemmaC `es-before-split-last`)) 0 THENA Auto)
   THEN (Assert first(e2) ~ ff⋅ THENA Auto)
   THEN HypSubst' (-1) 0
   THEN Reduce 0) }

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

---

Latex:


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


By

(Auto
  THEN  (RW  (AddrC  [2]  (LemmaC  `es-closed-open-interval-eq-before`))  0  THENA  Auto)
  THEN  (RW  (AddrC  [2]  (LemmaC  `es-before-split-last`))  0  THENA  Auto)
  THEN  (Assert  first(e2)  \msim{}  ff\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  Reduce  0)

---

Home Index