---

Step * 1 1 1 of Lemma pred-member-es-open-interval


1. es : EO
2. e1 : E
3. e2 : E
4. n : ℤ
5. 1 ≤ n
6. n < ||(e1, e2)||
7. ((e1, e2)[n - 1] <loc (e1, e2)[n])
8. (pred((e1, e2)[n]) <loc (e1, e2)[n])
9. (pred((e1, e2)[n]) <loc (e1, e2)[n - 1])
10. loc(pred((e1, e2)[n])) = loc((e1, e2)[n]) ∈ Id
11. (pred((e1, e2)[n]) < (e1, e2)[n])
12. ∀e':E
      (e' < (e1, e2)[n]) ⇒ ((e' = pred((e1, e2)[n]) ∈ E) ∨ (e' < pred((e1, e2)[n]))) 
      supposing loc(e') = loc((e1, e2)[n]) ∈ Id
13. ((e1, e2)[n - 1] = pred((e1, e2)[n]) ∈ E) ∨ ((e1, e2)[n - 1] < pred((e1, e2)[n]))
⊢ False
BY
{ (D -1 THEN Auto) }

---

Latex:



1.  es  :  EO
2.  e1  :  E
3.  e2  :  E
4.  n  :  \mBbbZ{}
5.  1  \mleq{}  n
6.  n  <  ||(e1,  e2)||
7.  ((e1,  e2)[n  -  1]  <loc  (e1,  e2)[n])
8.  (pred((e1,  e2)[n])  <loc  (e1,  e2)[n])
9.  (pred((e1,  e2)[n])  <loc  (e1,  e2)[n  -  1])
10.  loc(pred((e1,  e2)[n]))  =  loc((e1,  e2)[n])
11.  (pred((e1,  e2)[n])  <  (e1,  e2)[n])
12.  \mforall{}e':E
            (e'  <  (e1,  e2)[n])  {}\mRightarrow{}  ((e'  =  pred((e1,  e2)[n]))  \mvee{}  (e'  <  pred((e1,  e2)[n]))) 
            supposing  loc(e')  =  loc((e1,  e2)[n])
13.  ((e1,  e2)[n  -  1]  =  pred((e1,  e2)[n]))  \mvee{}  ((e1,  e2)[n  -  1]  <  pred((e1,  e2)[n]))
\mvdash{}  False


By

(D  -1  THEN  Auto)

---

Home Index