---

Step * 1 of Lemma es-interval-partition


∀es:EO. ∀e',e,a:E.  (((e <loc a) ∧ a ≤loc e' ) ⇒ ([e, e'] = ([e, pred(a)] @ [a, e']) ∈ (E List)))
BY
{ (((((((D 0 THENA Auto) THEN LocLessInd) THENA Auto)
      THEN Auto
      THEN (InstLemma `es-interval-less` [es; e; j])⋅
      THEN Auto)
     THENA ((Using [`b',a] (BLemma `es-le-trans3`))⋅ THEN Auto)
     )
    THEN (HypSubst (-1) 0)
    )
   THENA Auto
   ) }

1
1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. ∀k:E. ((k <loc j) ⇒ (∀e,a:E.  (((e <loc a) ∧ a ≤loc k ) ⇒ ([e, k] = ([e, pred(a)] @ [a, k]) ∈ (E List)))))@i
5. e : E@i
6. a : E@i
7. (e <loc a)@i
8. a ≤loc j @i
9. [e, j] = ([e, pred(j)] @ [j]) ∈ (E List)
⊢ ([e, pred(j)] @ [j]) = ([e, pred(a)] @ [a, j]) ∈ (E List)

---

Latex:



\mforall{}es:EO.  \mforall{}e',e,a:E.    (((e  <loc  a)  \mwedge{}  a  \mleq{}loc  e'  )  {}\mRightarrow{}  ([e,  e']  =  ([e,  pred(a)]  @  [a,  e'])))


By

(((((((D  0  THENA  Auto)  THEN  LocLessInd)  THENA  Auto)
        THEN  Auto
        THEN  (InstLemma  `es-interval-less`  [es;  e;  j])\mcdot{}
        THEN  Auto)
      THENA  ((Using  [`b',a]  (BLemma  `es-le-trans3`))\mcdot{}  THEN  Auto)
      )
    THEN  (HypSubst  (-1)  0)
    )
  THENA  Auto
  )

---

Home Index