---

Step * of Lemma es-open-interval-closed

∀[es:EO]. ∀[e1,e2:E].  (pred(e1), e2) = [e1;e2) ∈ (E List) supposing ¬↑first(e1)
BY
{ (Auto
   THEN RepUR ``es-open-interval es-closed-open-interval`` 0
   THEN RepeatFor 2 ((EqCD THEN Auto))
   THEN (BLemma `iff_imp_equal_bool` THENA Auto)
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN Auto
   THEN Try (Complete ((D (-1) THEN BLemma `es-pred-locl-implies-le` THEN Auto)))
   THEN (Assert (pred(e1) <loc e1) BY
               Auto)
   THEN Auto) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[e1,e2:E].    (pred(e1),  e2)  =  [e1;e2)  supposing  \mneg{}\muparrow{}first(e1)


By

(Auto
  THEN  RepUR  ``es-open-interval  es-closed-open-interval``  0
  THEN  RepeatFor  2  ((EqCD  THEN  Auto))
  THEN  (BLemma  `iff\_imp\_equal\_bool`  THENA  Auto)
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  Auto
  THEN  Try  (Complete  ((D  (-1)  THEN  BLemma  `es-pred-locl-implies-le`  THEN  Auto)))
  THEN  (Assert  (pred(e1)  <loc  e1)  BY
                          Auto)
  THEN  Auto)

---

Home Index