---

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

∀[es:EO]. ∀[e1,e2:E].  [e1;e2) = [e1 / (e1, e2)] ∈ (E List) supposing (e1 <loc e2)
BY
{ (Auto
   THEN RepUR ``es-open-interval es-closed-open-interval`` 0
   THEN (Assert ⌈(e1 ∈ before(e2))⌉⋅ THENA (GenListD 0 THEN Auto))
   THEN (InstLemma `es-before-decomp` [⌈es⌉;⌈e2⌉;⌈e1⌉]⋅ THENA Auto)
   THEN ExRepD
   THEN (RW (AddrC [2;2] (HypC (-1))) 0 THENA Auto)
   THEN RepeatFor 2 ((RWO "filter_append" 0 THENA Auto))
   THEN Reduce 0
   THEN (Subst ⌈e1 ≤loc e1 ~ tt⌉ 0⋅ THENA Auto)
   THEN Reduce 0
   THEN Assert ⌈↑null(filter(λev.e1 ≤loc ev;before(e1)))⌉⋅) }

1
.....assertion..... 
1. es : EO
2. e1 : E
3. e2 : E
4. (e1 <loc e2)
5. (e1 ∈ before(e2))
6. l : E List
7. before(e2) = (before(e1) @ [e1] @ l) ∈ (E List)
⊢ ↑null(filter(λev.e1 ≤loc ev;before(e1)))

2
1. es : EO
2. e1 : E
3. e2 : E
4. (e1 <loc e2)
5. (e1 ∈ before(e2))
6. l : E List
7. before(e2) = (before(e1) @ [e1] @ l) ∈ (E List)
8. ↑null(filter(λev.e1 ≤loc ev;before(e1)))
⊢ (filter(λev.e1 ≤loc ev;before(e1)) @ [e1 / filter(λev.e1 ≤loc ev;l)])
= [e1 / filter(λev.e1 <loc ev;before(e2))]
∈ (E List)

---

Latex:


\mforall{}[es:EO].  \mforall{}[e1,e2:E].    [e1;e2)  =  [e1  /  (e1,  e2)]  supposing  (e1  <loc  e2)


By

(Auto
  THEN  RepUR  ``es-open-interval  es-closed-open-interval``  0
  THEN  (Assert  \mkleeneopen{}(e1  \mmember{}  before(e2))\mkleeneclose{}\mcdot{}  THENA  (GenListD  0  THEN  Auto))
  THEN  (InstLemma  `es-before-decomp`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (RW  (AddrC  [2;2]  (HypC  (-1)))  0  THENA  Auto)
  THEN  RepeatFor  2  ((RWO  "filter\_append"  0  THENA  Auto))
  THEN  Reduce  0
  THEN  (Subst  \mkleeneopen{}e1  \mleq{}loc  e1  \msim{}  tt\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  Assert  \mkleeneopen{}\muparrow{}null(filter(\mlambda{}ev.e1  \mleq{}loc  ev;before(e1)))\mkleeneclose{}\mcdot{})

---

Home Index