---

Step * of Lemma es-interval-less-sq

∀[es:EO]. ∀[e,e':E].  [e, e'] ~ [e, pred(e')] @ [e'] supposing (e <loc e')
BY
{ ((((UnivCD THENA Auto) THEN Unfold `es-interval` 0 THEN RWO "filter_append" 0) THENA Auto)
   THEN (RW (AddrC [1] (RecUnfoldC `es-before`)) 0)
   THEN AutoSplit
   THEN (RWO "filter_append" 0 THENA Auto)
   THEN EqCD
   THEN Try (Trivial)
   THEN AutoSplit) }

1
1. es : EO
2. e : E
3. e' : E
4. ¬e ≤loc e' 
5. ¬↑first(e')
6. (e <loc e')
⊢ [] ~ [e']

---

Latex:


\mforall{}[es:EO].  \mforall{}[e,e':E].    [e,  e']  \msim{}  [e,  pred(e')]  @  [e']  supposing  (e  <loc  e')


By

((((UnivCD  THENA  Auto)  THEN  Unfold  `es-interval`  0  THEN  RWO  "filter\_append"  0)  THENA  Auto)
  THEN  (RW  (AddrC  [1]  (RecUnfoldC  `es-before`))  0)
  THEN  AutoSplit
  THEN  (RWO  "filter\_append"  0  THENA  Auto)
  THEN  EqCD
  THEN  Try  (Trivial)
  THEN  AutoSplit)

---

Home Index