---

Step * of Lemma l_before-es-interval

∀es:EO. ∀e,e',a,b:E.  (a before b ∈ [e, e'] ⇐⇒ (a <loc b) ∧ e ≤loc a  ∧ b ≤loc e' )
BY
{ ((((((((((((((UnivCD THENA Auto) THEN Unfold `es-interval` 0 THEN RWO "l_before_filter" 0) THENA (Reduce 0 THEN Auto))
             THEN Reduce 0
             THEN RWO "assert-es-ble" 0)
            THENA Auto
            )
           THEN RWO "l_before_append_iff" 0
           )
          THENA Auto
          )
         THEN RWO "member_singleton" 0
         )
        THENA Auto
        )
       THEN RWO "l_before-es-before-iff" 0
       )
      THENA Auto
      )
     THEN RWO "member-es-before" 0
     )
    THENA Auto
    )
   THEN RWO "singleton_before" 0
   THEN Auto) }

1
1. es : EO@i'
2. e : E@i
3. e' : E@i
4. a : E@i
5. b : E@i
6. e ≤loc a @i
7. e ≤loc b @i
8. ((a <loc b) ∧ (b <loc e')) ∨ False ∨ ((a <loc e') ∧ (b = e' ∈ E))@i
⊢ (a <loc b)

2
1. es : EO@i'
2. e : E@i
3. e' : E@i
4. a : E@i
5. b : E@i
6. e ≤loc a @i
7. e ≤loc b @i
8. ((a <loc b) ∧ (b <loc e')) ∨ False ∨ ((a <loc e') ∧ (b = e' ∈ E))@i
⊢ b ≤loc e' 

3
1. es : EO@i'
2. e : E@i
3. e' : E@i
4. a : E@i
5. b : E@i
6. (a <loc b)@i
7. e ≤loc a @i
8. b ≤loc e' @i
⊢ ((a <loc b) ∧ (b <loc e')) ∨ False ∨ ((a <loc e') ∧ (b = e' ∈ E))

---

Latex:

---

Latex:
\mforall{}es:EO.  \mforall{}e,e',a,b:E.    (a  before  b  \mmember{}  [e,  e']  \mLeftarrow{}{}\mRightarrow{}  (a  <loc  b)  \mwedge{}  e  \mleq{}loc  a    \mwedge{}  b  \mleq{}loc  e'  )


By

---

Latex:
((((((((((((((UnivCD  THENA  Auto)  THEN  Unfold  `es-interval`  0  THEN  RWO  "l\_before\_filter"  0)
                        THENA  (Reduce  0  THEN  Auto)
                        )
                      THEN  Reduce  0
                      THEN  RWO  "assert-es-ble"  0)
                    THENA  Auto
                    )
                  THEN  RWO  "l\_before\_append\_iff"  0
                  )
                THENA  Auto
                )
              THEN  RWO  "member\_singleton"  0
              )
            THENA  Auto
            )
          THEN  RWO  "l\_before-es-before-iff"  0
          )
        THENA  Auto
        )
      THEN  RWO  "member-es-before"  0
      )
    THENA  Auto
    )
  THEN  RWO  "singleton\_before"  0
  THEN  Auto)

---

Home Index