---

Step * 1 1 1 2 of Lemma es-subinterval


1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. ∀k:E
     ((k <loc j)
     ⇒ (∀e1:E. (e1 ≤loc k  ⇒ (∀n:ℕ. (∃e∈(e1,k].||[e1, pred(e)]|| = n ∈ ℤ) supposing (n < ||[e1, k]|| and 0 < n)))))@i
5. e1 : E@i
6. ¬↑first(j)
7. e1 ≤loc pred(j) 
8. n : ℕ@i
9. 0 < n
10. n < ||[e1, j]||
11. ∀n:ℕ. (∃e∈(e1,pred(j)].||[e1, pred(e)]|| = n ∈ ℤ) supposing (n < ||[e1, pred(j)]|| and 0 < n)
12. ¬n < ||[e1, pred(j)]||
⊢ ∃e∈(e1,j].||[e1, pred(e)]|| = n ∈ ℤ
BY
{ (((((RWO "es-interval-less" (-3)) THENA Auto)
     THEN Try (((RWO "es-le-pred" (-6)) THEN Auto))
     THEN (RWO "length-append" (-3)))
    THENA Auto
    )
   THEN (Reduce (-3))
   ) }

1
1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. ∀k:E
     ((k <loc j)
     ⇒ (∀e1:E. (e1 ≤loc k  ⇒ (∀n:ℕ. (∃e∈(e1,k].||[e1, pred(e)]|| = n ∈ ℤ) supposing (n < ||[e1, k]|| and 0 < n)))))@i
5. e1 : E@i
6. ¬↑first(j)
7. (e1 <loc j)
8. n : ℕ@i
9. 0 < n
10. n < ||[e1, pred(j)]|| + 1
11. ∀n:ℕ. (∃e∈(e1,pred(j)].||[e1, pred(e)]|| = n ∈ ℤ) supposing (n < ||[e1, pred(j)]|| and 0 < n)
12. ¬n < ||[e1, pred(j)]||
⊢ ∃e∈(e1,j].||[e1, pred(e)]|| = n ∈ ℤ

---

Latex:



1.  es  :  EO@i'
2.  WellFnd\{i\}(E;x,y.(x  <loc  y))
3.  j  :  E@i
4.  \mforall{}k:E
          ((k  <loc  j)
          {}\mRightarrow{}  (\mforall{}e1:E
                      (e1  \mleq{}loc  k 
                      {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  (\mexists{}e\mmember{}(e1,k].||[e1,  pred(e)]||  =  n)  supposing  (n  <  ||[e1,  k]||  and  0  <  n)))))@i
5.  e1  :  E@i
6.  \mneg{}\muparrow{}first(j)
7.  e1  \mleq{}loc  pred(j) 
8.  n  :  \mBbbN{}@i
9.  0  <  n
10.  n  <  ||[e1,  j]||
11.  \mforall{}n:\mBbbN{}.  (\mexists{}e\mmember{}(e1,pred(j)].||[e1,  pred(e)]||  =  n)  supposing  (n  <  ||[e1,  pred(j)]||  and  0  <  n)
12.  \mneg{}n  <  ||[e1,  pred(j)]||
\mvdash{}  \mexists{}e\mmember{}(e1,j].||[e1,  pred(e)]||  =  n


By

(((((RWO  "es-interval-less"  (-3))  THENA  Auto)
      THEN  Try  (((RWO  "es-le-pred"  (-6))  THEN  Auto))
      THEN  (RWO  "length-append"  (-3)))
    THENA  Auto
    )
  THEN  (Reduce  (-3))
  )

---

Home Index