---

Step * 2 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 - 1 < ||(e1, e2)|| ⇒ (nth_tl((n - 1) + 1;(e1, e2)) = ((e1, e2)[n - 1], e2) ∈ (E List))
8. n < ||(e1, e2)||@i
⊢ nth_tl(n + 1;(e1, e2)) = ((e1, e2)[n], e2) ∈ (E List)
BY
{ ((D (-2) THENA Auto)
   THEN (Subst ⌈(n - 1) + 1 ~ n⌉ (-1)⋅ THENA Auto)
   THEN RWO "nth_tl_decomp" (-1)
   THEN Auto
   THEN (Assert ⌈((e1, e2)[n - 1], e2) = [(e1, e2)[n] / ((e1, e2)[n], e2)] ∈ (E List)⌉⋅
   THENM (HypSubst' (-1) (-2) THEN Auto)
   )
   THEN Thin (-1)
   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 RepD
   THEN (Assert ⌈¬↑first((e1, e2)[n - 1])⌉⋅ THENA Auto)
   THEN (Assert ⌈(e1 <loc e2)⌉⋅
         THENA (UseLoclTri ⌈es⌉⌈e1⌉⌈e2⌉⋅
                THEN (InstLemma `es-open-interval-nil` [⌈es⌉;⌈e1⌉;⌈e2⌉]⋅
                THENM (HypSubst' (-1) (-3) THEN Reduce (-3) THEN Auto)
                )
                THEN Auto
                THEN (Decide ↑first(e2) THENA Auto)
                THEN Try (Complete ((OrLeft THEN Auto)))
                THEN (OrRight THENA Auto)
                THEN Auto
                THEN Try (Complete ((HypSubst' (-2) 0 THEN Auto)))
                THEN 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)
⊢ ((e1, e2)[n - 1], 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  -  1  <  ||(e1,  e2)||  {}\mRightarrow{}  (nth\_tl((n  -  1)  +  1;(e1,  e2))  =  ((e1,  e2)[n  -  1],  e2))
8.  n  <  ||(e1,  e2)||@i
\mvdash{}  nth\_tl(n  +  1;(e1,  e2))  =  ((e1,  e2)[n],  e2)


By

((D  (-2)  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}(n  -  1)  +  1  \msim{}  n\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  RWO  "nth\_tl\_decomp"  (-1)
  THEN  Auto
  THEN  (Assert  \mkleeneopen{}((e1,  e2)[n  -  1],  e2)  =  [(e1,  e2)[n]  /  ((e1,  e2)[n],  e2)]\mkleeneclose{}\mcdot{}
  THENM  (HypSubst'  (-1)  (-2)  THEN  Auto)
  )
  THEN  Thin  (-1)
  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  RepD
  THEN  (Assert  \mkleeneopen{}\mneg{}\muparrow{}first((e1,  e2)[n  -  1])\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}(e1  <loc  e2)\mkleeneclose{}\mcdot{}
              THENA  (UseLoclTri  \mkleeneopen{}es\mkleeneclose{}\mkleeneopen{}e1\mkleeneclose{}\mkleeneopen{}e2\mkleeneclose{}\mcdot{}
                            THEN  (InstLemma  `es-open-interval-nil`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}
                            THENM  (HypSubst'  (-1)  (-3)  THEN  Reduce  (-3)  THEN  Auto)
                            )
                            THEN  Auto
                            THEN  (Decide  \muparrow{}first(e2)  THENA  Auto)
                            THEN  Try  (Complete  ((OrLeft  THEN  Auto)))
                            THEN  (OrRight  THENA  Auto)
                            THEN  Auto
                            THEN  Try  (Complete  ((HypSubst'  (-2)  0  THEN  Auto)))
                            THEN  Auto)
              ))

---

Home Index