---

Step * 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)
⊢ ([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
{ ((D 0 THENA Auto) THEN (Assert [e1, e2] = ([e1] @ (e1, e2) @ [e2]) ∈ (E List) BY Auto)) }

1
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)

---

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)
\mvdash{}  ([e1,  e2]  =  [e1  /  ((e1,  e2)  @  [e2])])
{}\mRightarrow{}  (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

((D  0  THENA  Auto)  THEN  (Assert  [e1,  e2]  =  ([e1]  @  (e1,  e2)  @  [e2])  BY  Auto))

---

Home Index