---

Step * of Lemma es-le-before-no_repeats

∀[es:EO]. ∀[e:E].  no_repeats(E;≤loc(e))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `es-le-before` 0
   THEN (RWO "no_repeats-append" 0 THENA Auto)
   THEN Unfold `guard` 0
   THEN Auto
   THEN Try (Complete ((BLemma `es-before-no_repeats` THEN Auto)))
   THEN Try (Complete ((BLemma `no_repeats-single` THEN Auto)))
   THEN (RWO "l_disjoint_singleton" 0 THENA Auto)
   THEN (D 0 THENA Auto)
   THEN (RWO "member-es-before" (-1) THENA Auto)
   THEN Auto) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[e:E].    no\_repeats(E;\mleq{}loc(e))


By

((UnivCD  THENA  Auto)
  THEN  Unfold  `es-le-before`  0
  THEN  (RWO  "no\_repeats-append"  0  THENA  Auto)
  THEN  Unfold  `guard`  0
  THEN  Auto
  THEN  Try  (Complete  ((BLemma  `es-before-no\_repeats`  THEN  Auto)))
  THEN  Try  (Complete  ((BLemma  `no\_repeats-single`  THEN  Auto)))
  THEN  (RWO  "l\_disjoint\_singleton"  0  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (RWO  "member-es-before"  (-1)  THENA  Auto)
  THEN  Auto)

---

Home Index