---

Step * 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 < ||(e1, e2)||@i
⊢ nth_tl(0 + 1;(e1, e2)) = ((e1, e2)[0], e2) ∈ (E List)
BY
{ (RecUnfold `nth_tl` 0
   THEN Reduce 0
   THEN Thin (-2)
   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
                THEN (Assert (pred(e2) <loc e2) BY
                            Auto)
                THEN Auto)
         )
   THEN (InstLemma `es-pred-exists-between` [⌜es⌝;⌜e1⌝;⌜e2⌝]⋅ THENA Auto)
   THEN ExRepD) }

1
1. es : EO
2. e1 : E
3. e2 : E
4. loc(e1) = loc(e2) ∈ Id
5. 0 < ||(e1, e2)||@i
6. (e1 <loc e2)
7. e : {e:E| ¬↑first(e)} 
8. e1 = pred(e) ∈ E
⊢ tl((e1, e2)) = ((e1, e2)[0], e2) ∈ (E List)

---

Latex:

---

Latex:

1.  es  :  EO
2.  e1  :  E
3.  e2  :  E
4.  loc(e1)  =  loc(e2)
5.  n  :  \mBbbZ{}
6.  0  <  ||(e1,  e2)||@i
\mvdash{}  nth\_tl(0  +  1;(e1,  e2))  =  ((e1,  e2)[0],  e2)


By

---

Latex:
(RecUnfold  `nth\_tl`  0
  THEN  Reduce  0
  THEN  Thin  (-2)
  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
                            THEN  (Assert  (pred(e2)  <loc  e2)  BY
                                                    Auto)
                            THEN  Auto)
              )
  THEN  (InstLemma  `es-pred-exists-between`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD)

---

Home Index