---

Step * 1 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. 0 < ||(e1, e2)||@i
6. (e1 <loc e2)
7. e : E
8. ¬↑first(e)
9. e1 = pred(e) ∈ E
10. (e1, e2) = [e;e2) ∈ (E List)
⊢ tl((e1, e2)) = ((e1, e2)[0], e2) ∈ (E List)
BY
{ ((Assert ⌈¬↑first(e2)⌉⋅ THENA Auto)
   THEN UseLoclTri ⌈es⌉⌈e⌉⌈e2⌉⋅
   THEN Try (Complete (((InstLemma `es-closed-open-interval-decomp` [⌈es⌉;⌈e⌉;⌈e2⌉]⋅ THENA Auto)
                        THEN HypSubst' (-1) (-4)
                        THEN HypSubst' (-4) 0
                        THEN Reduce 0
                        THEN Auto)))
   THEN (Assert ⌈False⌉⋅ THEN Auto)
   THEN Try (Complete (((Assert ⌈pred(e2) ≤loc e1 ⌉⋅ THENA Auto)
                        THEN (InstLemma `es-open-interval-nil` [⌈es⌉;⌈e1⌉;⌈e2⌉]⋅ THENA (Auto THEN OrRight THEN Auto))
                        THEN HypSubst' (-1) (-10)
                        THEN Reduce (-10)
                        THEN Auto)))
   THEN Try (Complete (((InstLemma `es-pred_property` [⌈es⌉;⌈e⌉]⋅ THEN Auto)
                        THEN (InstHyp [⌈e2⌉] (-1)⋅ THENA Auto)
                        THEN D (-1)
                        THEN Auto)))) }

---

Latex:



1.  es  :  EO
2.  e1  :  E
3.  e2  :  E
4.  loc(e1)  =  loc(e2)
5.  0  <  ||(e1,  e2)||@i
6.  (e1  <loc  e2)
7.  e  :  E
8.  \mneg{}\muparrow{}first(e)
9.  e1  =  pred(e)
10.  (e1,  e2)  =  [e;e2)
\mvdash{}  tl((e1,  e2))  =  ((e1,  e2)[0],  e2)


By

((Assert  \mkleeneopen{}\mneg{}\muparrow{}first(e2)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  UseLoclTri  \mkleeneopen{}es\mkleeneclose{}\mkleeneopen{}e\mkleeneclose{}\mkleeneopen{}e2\mkleeneclose{}\mcdot{}
  THEN  Try  (Complete  (((InstLemma  `es-closed-open-interval-decomp`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                            THEN  HypSubst'  (-1)  (-4)
                                            THEN  HypSubst'  (-4)  0
                                            THEN  Reduce  0
                                            THEN  Auto)))
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  Try  (Complete  (((Assert  \mkleeneopen{}pred(e2)  \mleq{}loc  e1  \mkleeneclose{}\mcdot{}  THENA  Auto)
                                            THEN  (InstLemma  `es-open-interval-nil`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}
                                                        THENA  (Auto  THEN  OrRight  THEN  Auto)
                                                        )
                                            THEN  HypSubst'  (-1)  (-10)
                                            THEN  Reduce  (-10)
                                            THEN  Auto)))
  THEN  Try  (Complete  (((InstLemma  `es-pred\_property`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THEN  Auto)
                                            THEN  (InstHyp  [\mkleeneopen{}e2\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
                                            THEN  D  (-1)
                                            THEN  Auto))))

---

Home Index