---

Step * 1 of Lemma member-es-interval


1. es : EO@i'
2. e : E@i
3. e' : E@i
4. ev : E@i
⊢ (ev ∈ [e, e']) ⇐⇒ e ≤loc ev  ∧ ev ≤loc e' 
BY
{ ((((((((Unfold `es-interval` 0 THEN RWO "member_filter" 0) THENM Reduce 0) THENM RWO "member_append" 0)
      THENM RWO "member-es-before" 0
      )
     THENM RWO "cons_member" 0
     )
    THENM RWO "nil_member" 0
    )
   THENM RWO "assert-es-ble" 0
   )
   THENA (Reduce 0 THEN Auto)
   ) }

1
1. es : EO@i'
2. e : E@i
3. e' : E@i
4. ev : E@i
⊢ ((ev <loc e') ∨ (ev = e' ∈ E) ∨ False) ∧ e ≤loc ev  ⇐⇒ e ≤loc ev  ∧ ev ≤loc e' 

---

Latex:



1.  es  :  EO@i'
2.  e  :  E@i
3.  e'  :  E@i
4.  ev  :  E@i
\mvdash{}  (ev  \mmember{}  [e,  e'])  \mLeftarrow{}{}\mRightarrow{}  e  \mleq{}loc  ev    \mwedge{}  ev  \mleq{}loc  e' 


By

((((((((Unfold  `es-interval`  0  THEN  RWO  "member\_filter"  0)  THENM  Reduce  0)
          THENM  RWO  "member\_append"  0
          )
        THENM  RWO  "member-es-before"  0
        )
      THENM  RWO  "cons\_member"  0
      )
    THENM  RWO  "nil\_member"  0
    )
  THENM  RWO  "assert-es-ble"  0
  )
  THENA  (Reduce  0  THEN  Auto)
  )

---

Home Index