---

Step * 1 1 1 1 of Lemma pred-hd-es-open-interval


1. es : EO
2. e1 : E
3. e2 : E
4. ||(e1, e2)|| > 0
5. (e1 <loc hd((e1, e2)))
6. (hd((e1, e2)) <loc e2)
7. loc(pred(hd((e1, e2)))) = loc(hd((e1, e2))) ∈ Id
8. (pred(hd((e1, e2))) < hd((e1, e2)))
9. ∀e':E
     (e' < hd((e1, e2))) ⇒ ((e' = pred(hd((e1, e2))) ∈ E) ∨ (e' < pred(hd((e1, e2))))) 
     supposing loc(e') = loc(hd((e1, e2))) ∈ Id
10. (e1 < pred(hd((e1, e2))))
11. i : ℕ
12. i < ||(e1, e2)||
13. ¬(i = 0 ∈ ℤ)
14. l-ordered(E;e1,e2.(e1 <loc e2);(e1, e2))
⊢ (e1, e2)[0] ≤loc (e1, e2)[i] 
BY
{ (Unfold `l-ordered` (-1)
   THEN ((InstHyp [⌜(e1, e2)[0]⌝;⌜(e1, e2)[i]⌝] (-1)⋅ THENM Auto) THENA Auto)
   THEN RepUR ``l_before sublist`` 0
   THEN InstConcl [⌜λx.if (x =z 0) then 0 else i fi ⌝]⋅
   THEN Auto
   THEN Try (Complete ((IntSegCases (-1) THEN Reduce 0 THEN Auto')))
   THEN Unfold `increasing` 0
   THEN Reduce 0
   THEN Auto
   THEN IntSegCases (-1)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  es  :  EO
2.  e1  :  E
3.  e2  :  E
4.  ||(e1,  e2)||  >  0
5.  (e1  <loc  hd((e1,  e2)))
6.  (hd((e1,  e2))  <loc  e2)
7.  loc(pred(hd((e1,  e2))))  =  loc(hd((e1,  e2)))
8.  (pred(hd((e1,  e2)))  <  hd((e1,  e2)))
9.  \mforall{}e':E
          (e'  <  hd((e1,  e2)))  {}\mRightarrow{}  ((e'  =  pred(hd((e1,  e2))))  \mvee{}  (e'  <  pred(hd((e1,  e2))))) 
          supposing  loc(e')  =  loc(hd((e1,  e2)))
10.  (e1  <  pred(hd((e1,  e2))))
11.  i  :  \mBbbN{}
12.  i  <  ||(e1,  e2)||
13.  \mneg{}(i  =  0)
14.  l-ordered(E;e1,e2.(e1  <loc  e2);(e1,  e2))
\mvdash{}  (e1,  e2)[0]  \mleq{}loc  (e1,  e2)[i] 


By

---

Latex:
(Unfold  `l-ordered`  (-1)
  THEN  ((InstHyp  [\mkleeneopen{}(e1,  e2)[0]\mkleeneclose{};\mkleeneopen{}(e1,  e2)[i]\mkleeneclose{}]  (-1)\mcdot{}  THENM  Auto)  THENA  Auto)
  THEN  RepUR  ``l\_before  sublist``  0
  THEN  InstConcl  [\mkleeneopen{}\mlambda{}x.if  (x  =\msubz{}  0)  then  0  else  i  fi  \mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  ((IntSegCases  (-1)  THEN  Reduce  0  THEN  Auto')))
  THEN  Unfold  `increasing`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  IntSegCases  (-1)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index