---

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

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A:Type]. ∀[X:EClass(A)]. ∀[e1,e2:E].
  X[e1;e2]
  = (if e1 <loc e2 ∧b e1 ∈b X then [X(e1)] else [] fi  @ X(e1, e2) @ if e2 ∈b X then [X(e2)] else [] fi )
  ∈ (A List) 
  supposing e1 ≤loc e2 
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``es-closed-interval-vals`` 0
   THEN (InstLemma `es-interval-open-interval` [⌈es⌉;⌈e2⌉;⌈e1⌉]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN OldAutoBoolCase ⌈e1 <loc e2⌉⋅) }

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)
⊢ ([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))

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

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A:Type].  \mforall{}[X:EClass(A)].  \mforall{}[e1,e2:E].
    X[e1;e2]
    =  (if  e1  <loc  e2  \mwedge{}\msubb{}  e1  \mmember{}\msubb{}  X  then  [X(e1)]  else  []  fi 
        @  X(e1,  e2)
        @  if  e2  \mmember{}\msubb{}  X  then  [X(e2)]  else  []  fi  ) 
    supposing  e1  \mleq{}loc  e2 


By

((UnivCD  THENA  Auto)
  THEN  RepUR  ``es-closed-interval-vals``  0
  THEN  (InstLemma  `es-interval-open-interval`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  OldAutoBoolCase  \mkleeneopen{}e1  <loc  e2\mkleeneclose{}\mcdot{})

---

Home Index