---

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

.....assertion..... 
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. ((e1, e2)[n - 1] <loc pred((e1, e2)[n]))
⊢ False
BY
{ ((Assert ⌈¬↑first((e1, e2)[n])⌉⋅
    THENA ((D 0 THEN Auto)
           THEN (RWO "assert-es-first" (-1) THENA Auto)
           THEN InstHyp [⌈(e1, e2)[n - 1]⌉] (-1)⋅
           THEN Auto)
    )
   THEN (InstLemma `member-es-open-interval` [⌈es⌉;⌈e1⌉;⌈e2⌉;⌈(e1, e2)[n]⌉]⋅ THENA Auto)
   THEN (InstLemma `member-es-open-interval` [⌈es⌉;⌈e1⌉;⌈e2⌉;⌈(e1, e2)[n - 1]⌉]⋅ THENA Auto)
   THEN (((D (-1) THEN Thin (-1)) THEN (D (-1) THENA (With ⌈n - 1⌉ (D 0)⋅ THEN Auto)))
         THEN ((D (-2) THEN Thin (-2)) THEN (D (-2) THENA (With ⌈n⌉ (D 0)⋅ THEN Auto)))
         THEN RepD
         THEN (Assert ⌈(pred((e1, e2)[n]) ∈ (e1, e2))⌉⋅ THENA (BLemma `member-es-open-interval` THEN Auto))
         THEN Unfold `l_member` (-1)
         THEN ExRepD
         THEN RepeatFor 2 (MoveToHyp 0 (-10))
         THEN (HypSubst' (-3) (-2) THENA Auto)
         THEN (HypSubst' (-3) (-1) THENA Auto))⋅) }

1
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. ¬↑first((e1, e2)[n])
9. (e1 <loc (e1, e2)[n - 1])
10. ((e1, e2)[n - 1] <loc e2)
11. (e1 <loc (e1, e2)[n])
12. ((e1, e2)[n] <loc e2)
13. i : ℕ
14. i < ||(e1, e2)||
15. pred((e1, e2)[n]) = (e1, e2)[i] ∈ E
16. ((e1, e2)[i] <loc (e1, e2)[n])
17. ((e1, e2)[n - 1] <loc (e1, e2)[i])
⊢ False

---

Latex:


.....assertion..... 
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.  ((e1,  e2)[n  -  1]  <loc  pred((e1,  e2)[n]))
\mvdash{}  False


By

((Assert  \mkleeneopen{}\mneg{}\muparrow{}first((e1,  e2)[n])\mkleeneclose{}\mcdot{}
    THENA  ((D  0  THEN  Auto)
                  THEN  (RWO  "assert-es-first"  (-1)  THENA  Auto)
                  THEN  InstHyp  [\mkleeneopen{}(e1,  e2)[n  -  1]\mkleeneclose{}]  (-1)\mcdot{}
                  THEN  Auto)
    )
  THEN  (InstLemma  `member-es-open-interval`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}(e1,  e2)[n]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `member-es-open-interval`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}(e1,  e2)[n  -  1]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (((D  (-1)  THEN  Thin  (-1))  THEN  (D  (-1)  THENA  (With  \mkleeneopen{}n  -  1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)))
              THEN  ((D  (-2)  THEN  Thin  (-2))  THEN  (D  (-2)  THENA  (With  \mkleeneopen{}n\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)))
              THEN  RepD
              THEN  (Assert  \mkleeneopen{}(pred((e1,  e2)[n])  \mmember{}  (e1,  e2))\mkleeneclose{}\mcdot{}
                          THENA  (BLemma  `member-es-open-interval`  THEN  Auto)
                          )
              THEN  Unfold  `l\_member`  (-1)
              THEN  ExRepD
              THEN  RepeatFor  2  (MoveToHyp  0  (-10))
              THEN  (HypSubst'  (-3)  (-2)  THENA  Auto)
              THEN  (HypSubst'  (-3)  (-1)  THENA  Auto))\mcdot{})

---

Home Index