---

Step * 1 1 of Lemma es-closed-interval-vals-decomp


1. Info : Type
2. es : EO+(Info)
3. A : Type
4. X : EClass(A)
5. e1 : E
6. e2 : E
7. e1 ≤loc e2 
8. (e1 <loc e2)
9. [e1, e2] = [e1 / ((e1, e2) @ [e2])] ∈ (E List)@i
10. [e1, e2] = ([e1] @ (e1, e2) @ [e2]) ∈ (E List)
⊢ mapfilter(λe.X(e);λe.e ∈b X;[e1, e2])
= (if e1 ∈b X then [X(e1)] else [] fi  @ X(e1, e2) @ if e2 ∈b X then [X(e2)] else [] fi )
∈ (A List)
BY
{ (OldAutoBoolCase ⌈e2 ∈b X⌉⋅
   THEN OldAutoBoolCase ⌈e1 ∈b X⌉⋅
   THEN (HypSubst' (-3) 0 THENA Auto)
   THEN Reduce (-1)
   THEN Auto
   THEN ((RWW "mapfilter-append" 0 THENA Auto)
         THEN Reduce 0
         THEN Unfold `mapfilter` 0
         THEN Reduce 0
         THEN OldAutoSplit
         THEN OldAutoSplit
         THEN Try (((Fold `mapfilter` 0 THEN Fold `es-prior-interval-vals` 0) THEN Auto)))⋅) }

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)
3.  A  :  Type
4.  X  :  EClass(A)
5.  e1  :  E
6.  e2  :  E
7.  e1  \mleq{}loc  e2 
8.  (e1  <loc  e2)
9.  [e1,  e2]  =  [e1  /  ((e1,  e2)  @  [e2])]@i
10.  [e1,  e2]  =  ([e1]  @  (e1,  e2)  @  [e2])
\mvdash{}  mapfilter(\mlambda{}e.X(e);\mlambda{}e.e  \mmember{}\msubb{}  X;[e1,  e2])
=  (if  e1  \mmember{}\msubb{}  X  then  [X(e1)]  else  []  fi    @  X(e1,  e2)  @  if  e2  \mmember{}\msubb{}  X  then  [X(e2)]  else  []  fi  )


By

(OldAutoBoolCase  \mkleeneopen{}e2  \mmember{}\msubb{}  X\mkleeneclose{}\mcdot{}
  THEN  OldAutoBoolCase  \mkleeneopen{}e1  \mmember{}\msubb{}  X\mkleeneclose{}\mcdot{}
  THEN  (HypSubst'  (-3)  0  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  Auto
  THEN  ((RWW  "mapfilter-append"  0  THENA  Auto)
              THEN  Reduce  0
              THEN  Unfold  `mapfilter`  0
              THEN  Reduce  0
              THEN  OldAutoSplit
              THEN  OldAutoSplit
              THEN  Try  (((Fold  `mapfilter`  0  THEN  Fold  `es-prior-interval-vals`  0)  THEN  Auto)))\mcdot{})

---

Home Index