---

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

∀[es:EO]. ∀[e,x:E]. ∀[L:E List].  L = before(x) ∈ (E List) supposing L @ [x] ≤ ≤loc(e)
BY
{ (Auto
   THEN D (-1)
   THEN (Assert ⌈x ≤loc e ⌉⋅
         THENA ((Assert ⌈(x ∈ ≤loc(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-le-before-partition` [⌈es⌉;⌈e⌉;⌈x⌉]⋅ THENA Auto)
   THEN (Assert ⌈∃l':E List. (((L @ [x]) @ l) = (before(x) @ [x] @ l') ∈ (E List))⌉⋅
         THENA ((RevHypSubst' (-3) 0 THENA Auto)
                THEN HypSubst' (-1) 0
                THEN (RWO "es-interval-open-interval" 0 THENA Auto)
                THEN AutoSplit
                THEN Try (Complete ((InstConcl [⌈(x, e) @ [e]⌉]⋅ THEN Auto)))
                THEN UseLoclTri ⌈es⌉⌈x⌉⌈e⌉⋅
                THEN Try (Complete ((Assert ⌈False⌉⋅ THEN Auto)))
                THEN (HypSubst' (-1) 0 THENA Auto)
                THEN (RWO "es-open-interval-nil" 0 THENA Auto)
                THEN Try (Complete (((Decide ⌈↑first(e)⌉⋅ THENA Auto)
                                     THEN Try (Complete ((OrLeft THEN Auto)))
                                     THEN Try (Complete ((OrRight THEN Auto))))))
                THEN Reduce 0
                THEN InstConcl [⌈[]⌉]⋅
                THEN Auto)
         )
   THEN D (-1)
   THEN (RWO "append_assoc<" (-1) THENA Auto)
   THEN (InstLemma `es-le-before-no_repeats` [⌈es⌉;⌈e⌉]⋅ THENA Auto)
   THEN (HypSubst' (-6) (-1) THENA Auto)
   THEN FLemma `list-decomp-no_repeats` [-2]
   THEN Auto) }

---

Latex:


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


By

(Auto
  THEN  D  (-1)
  THEN  (Assert  \mkleeneopen{}x  \mleq{}loc  e  \mkleeneclose{}\mcdot{}
              THENA  ((Assert  \mkleeneopen{}(x  \mmember{}  \mleq{}loc(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-le-before-partition`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\mexists{}l':E  List.  (((L  @  [x])  @  l)  =  (before(x)  @  [x]  @  l'))\mkleeneclose{}\mcdot{}
              THENA  ((RevHypSubst'  (-3)  0  THENA  Auto)
                            THEN  HypSubst'  (-1)  0
                            THEN  (RWO  "es-interval-open-interval"  0  THENA  Auto)
                            THEN  AutoSplit
                            THEN  Try  (Complete  ((InstConcl  [\mkleeneopen{}(x,  e)  @  [e]\mkleeneclose{}]\mcdot{}  THEN  Auto)))
                            THEN  UseLoclTri  \mkleeneopen{}es\mkleeneclose{}\mkleeneopen{}x\mkleeneclose{}\mkleeneopen{}e\mkleeneclose{}\mcdot{}
                            THEN  Try  (Complete  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)))
                            THEN  (HypSubst'  (-1)  0  THENA  Auto)
                            THEN  (RWO  "es-open-interval-nil"  0  THENA  Auto)
                            THEN  Try  (Complete  (((Decide  \mkleeneopen{}\muparrow{}first(e)\mkleeneclose{}\mcdot{}  THENA  Auto)
                                                                      THEN  Try  (Complete  ((OrLeft  THEN  Auto)))
                                                                      THEN  Try  (Complete  ((OrRight  THEN  Auto))))))
                            THEN  Reduce  0
                            THEN  InstConcl  [\mkleeneopen{}[]\mkleeneclose{}]\mcdot{}
                            THEN  Auto)
              )
  THEN  D  (-1)
  THEN  (RWO  "append\_assoc<"  (-1)  THENA  Auto)
  THEN  (InstLemma  `es-le-before-no\_repeats`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (HypSubst'  (-6)  (-1)  THENA  Auto)
  THEN  FLemma  `list-decomp-no\_repeats`  [-2]
  THEN  Auto)

---

Home Index