---

Step * of Lemma iseg-es-before-is-before

∀[es:EO]. ∀[e,x:E]. ∀[L:E List].  L = before(x) ∈ (E List) supposing L @ [x] ≤ before(e)
BY
{ (Auto
   THEN D (-1)
   THEN (Assert ⌜(x <loc e)⌝⋅
         THENA ((Assert ⌜(x ∈ before(e))⌝⋅ THENM GenListD (-1))
                THEN HypSubst' (-1) 0
                THEN GenListD 0
                THEN (OrLeft THENA Auto)
                THEN GenListD 0
                THEN (OrRight THENA Auto)
                THEN GenListD 0)
         )
   THEN (InstLemma `es-before-partition` [⌜es⌝;⌜e⌝;⌜x⌝]⋅ THENA Auto)
   THEN RepUR ``es-le-before`` (-1)
   THEN (InstLemma `es-before-no_repeats` [⌜es⌝;⌜e⌝]⋅ THENA Auto)
   THEN (HypSubst' (-4) (-1) THENA Auto)
   THEN (HypSubst' (-4) (-2) THENA Auto)
   THEN FLemma `list-decomp-no_repeats` [-2]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[es:EO].  \mforall{}[e,x:E].  \mforall{}[L:E  List].    L  =  before(x)  supposing  L  @  [x]  \mleq{}  before(e)


By

---

Latex:
(Auto
  THEN  D  (-1)
  THEN  (Assert  \mkleeneopen{}(x  <loc  e)\mkleeneclose{}\mcdot{}
              THENA  ((Assert  \mkleeneopen{}(x  \mmember{}  before(e))\mkleeneclose{}\mcdot{}  THENM  GenListD  (-1))
                            THEN  HypSubst'  (-1)  0
                            THEN  GenListD  0
                            THEN  (OrLeft  THENA  Auto)
                            THEN  GenListD  0
                            THEN  (OrRight  THENA  Auto)
                            THEN  GenListD  0)
              )
  THEN  (InstLemma  `es-before-partition`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``es-le-before``  (-1)
  THEN  (InstLemma  `es-before-no\_repeats`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (HypSubst'  (-4)  (-1)  THENA  Auto)
  THEN  (HypSubst'  (-4)  (-2)  THENA  Auto)
  THEN  FLemma  `list-decomp-no\_repeats`  [-2]
  THEN  Auto)

---

Home Index