---

Step * of Lemma eo-forward-split-before

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[e,x:E].  before(e) = (before(x) @ before(e)) ∈ (E List) supposing x ≤loc e 
BY
{ (Auto
   THEN (RWO "eo-forward-before" 0 THENA Auto)
   THEN Fold `es-closed-open-interval` 0
   THEN D (-1)
   THEN Try (((HypSubst' (-1) 0 THENA Auto)
              THEN (RWO "es-closed-open-interval-nil" 0 THENA Auto)
              THEN RWO "append-nil" 0
              THEN Auto))
   THEN (InstLemma `es-before-partition` [⌜es⌝;⌜e⌝;⌜x⌝]⋅ THENA Auto)
   THEN RepUR ``es-le-before`` (-1)
   THEN (RWO "append_assoc" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN RWO "es-closed-open-interval-decomp<" (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[e,x:E].    before(e)  =  (before(x)  @  before(e))  supposing  x  \mleq{}loc  e 


By

---

Latex:
(Auto
  THEN  (RWO  "eo-forward-before"  0  THENA  Auto)
  THEN  Fold  `es-closed-open-interval`  0
  THEN  D  (-1)
  THEN  Try  (((HypSubst'  (-1)  0  THENA  Auto)
                        THEN  (RWO  "es-closed-open-interval-nil"  0  THENA  Auto)
                        THEN  RWO  "append-nil"  0
                        THEN  Auto))
  THEN  (InstLemma  `es-before-partition`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``es-le-before``  (-1)
  THEN  (RWO  "append\_assoc"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  RWO  "es-closed-open-interval-decomp<"  (-1)
  THEN  Auto)

---

Home Index