---

Step * 2 1 1 of Lemma nth_tl-es-open-interval


1. es : EO
2. e1 : E
3. e2 : E
4. loc(e1) = loc(e2) ∈ Id
5. n : ℤ
6. 0 < n
7. n < ||(e1, e2)||@i
8. (e1 <loc (e1, e2)[n - 1])
9. ((e1, e2)[n - 1] <loc e2)
10. ¬↑first((e1, e2)[n - 1])
11. (e1 <loc e2)
12. e : E
13. ¬↑first(e)
14. (e1, e2)[n - 1] = pred(e) ∈ E
15. ((e1, e2)[n - 1], e2) = [e;e2) ∈ (E List)
16. pred((e1, e2)[n]) = (e1, e2)[n - 1] ∈ E
17. pred((e1, e2)[n]) = pred(e) ∈ E
18. ((e1, e2)[n - 1] <loc (e1, e2)[n])
19. (e1, e2)[n] = e ∈ E
⊢ [(e1, e2)[n];e2) = [(e1, e2)[n] / ((e1, e2)[n], e2)] ∈ (E List)
BY
{ (UseLoclTri ⌈es⌉⌈(e1, e2)[n]⌉⌈e2⌉⋅
   THEN Try (Complete ((BLemma `es-closed-open-interval-decomp` THEN Auto)))
   THEN (InstLemma `member-es-open-interval` [⌈es⌉;⌈e1⌉;⌈e2⌉;⌈(e1, e2)[n]⌉]⋅ THENA Auto)
   THEN (D (-1) THEN Thin (-1))
   THEN D (-1)
   THEN Auto) }

---

Latex:



1.  es  :  EO
2.  e1  :  E
3.  e2  :  E
4.  loc(e1)  =  loc(e2)
5.  n  :  \mBbbZ{}
6.  0  <  n
7.  n  <  ||(e1,  e2)||@i
8.  (e1  <loc  (e1,  e2)[n  -  1])
9.  ((e1,  e2)[n  -  1]  <loc  e2)
10.  \mneg{}\muparrow{}first((e1,  e2)[n  -  1])
11.  (e1  <loc  e2)
12.  e  :  E
13.  \mneg{}\muparrow{}first(e)
14.  (e1,  e2)[n  -  1]  =  pred(e)
15.  ((e1,  e2)[n  -  1],  e2)  =  [e;e2)
16.  pred((e1,  e2)[n])  =  (e1,  e2)[n  -  1]
17.  pred((e1,  e2)[n])  =  pred(e)
18.  ((e1,  e2)[n  -  1]  <loc  (e1,  e2)[n])
19.  (e1,  e2)[n]  =  e
\mvdash{}  [(e1,  e2)[n];e2)  =  [(e1,  e2)[n]  /  ((e1,  e2)[n],  e2)]


By

(UseLoclTri  \mkleeneopen{}es\mkleeneclose{}\mkleeneopen{}(e1,  e2)[n]\mkleeneclose{}\mkleeneopen{}e2\mkleeneclose{}\mcdot{}
  THEN  Try  (Complete  ((BLemma  `es-closed-open-interval-decomp`  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  (D  (-1)  THEN  Thin  (-1))
  THEN  D  (-1)
  THEN  Auto)

---

Home Index