---

Step * 2 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)
⊢ ([e1, e2] = ((e1, e2) @ [e2]) ∈ (E List))
⇒ (mapfilter(λe.X(e);λe.e ∈b X;[e1, e2]) = (X(e1, e2) @ if e2 ∈b X then [X(e2)] else [] fi ) ∈ (A List))
BY
{ (OldAutoBoolCase ⌈e2 ∈b X⌉⋅
   THEN (D 0 THENA Auto)
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN Reduce (-1)
   THEN Auto
   THEN (RWW "mapfilter-append" 0 THENA Auto)
   THEN Try (Fold `es-prior-interval-vals` 0)
   THEN EqCD
   THEN Auto
   THEN RepUR ``mapfilter`` 0
   THEN OldAutoSplit
   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.  \mneg{}(e1  <loc  e2)
\mvdash{}  ([e1,  e2]  =  ((e1,  e2)  @  [e2]))
{}\mRightarrow{}  (mapfilter(\mlambda{}e.X(e);\mlambda{}e.e  \mmember{}\msubb{}  X;[e1,  e2])  =  (X(e1,  e2)  @  if  e2  \mmember{}\msubb{}  X  then  [X(e2)]  else  []  fi  ))


By

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

---

Home Index