---

Step * 2 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)
⊢ ((e1, e2)[n - 1], e2) = [(e1, e2)[n] / ((e1, e2)[n], e2)] ∈ (E List)
BY
{ ((InstLemma `es-pred-exists-between` [⌈es⌉;⌈(e1, e2)[n - 1]⌉;⌈e2⌉]⋅ THENA Auto)
   THEN ExRepD
   THEN D (-2)
   THEN (InstLemma `es-open-interval-closed` [⌈es⌉;⌈e⌉;⌈e2⌉]⋅ THENA Auto)
   THEN (RevHypSubst' (-2) (-1) THENA Auto)
   THEN HypSubst' (-1) 0
   THEN (InstLemma `pred-member-es-open-interval` [⌈es⌉;⌈e1⌉;⌈e2⌉;⌈n⌉]⋅ THENA Auto)
   THEN (Assert ⌈pred((e1, e2)[n]) = pred(e) ∈ E⌉⋅ THENA Auto)
   THEN (InstLemma `es-open-interval-ordered-inst` [⌈es⌉;⌈e1⌉;⌈e2⌉;⌈n - 1⌉;⌈n⌉]⋅ THENA Auto)
   THEN (FLemma `es-pred-one-one` [-2] THENA Auto)
   THEN (RevHypSubst' (-1) 0 THENA Auto)) }

1
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)

---

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)
\mvdash{}  ((e1,  e2)[n  -  1],  e2)  =  [(e1,  e2)[n]  /  ((e1,  e2)[n],  e2)]


By

((InstLemma  `es-pred-exists-between`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}(e1,  e2)[n  -  1]\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  D  (-2)
  THEN  (InstLemma  `es-open-interval-closed`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RevHypSubst'  (-2)  (-1)  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  (InstLemma  `pred-member-es-open-interval`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}pred((e1,  e2)[n])  =  pred(e)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `es-open-interval-ordered-inst`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}n  -  1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (FLemma  `es-pred-one-one`  [-2]  THENA  Auto)
  THEN  (RevHypSubst'  (-1)  0  THENA  Auto))

---

Home Index