---

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

∀[es:EO]. ∀[e1,e2:E].  pred(hd((e1, e2))) = e1 ∈ E supposing ||(e1, e2)|| > 0
BY
{ (Auto
   THEN (InstLemma `member-es-open-interval` [⌈es⌉;⌈e1⌉;⌈e2⌉;⌈hd((e1, e2))⌉]⋅ THENA Auto)
   THEN (D (-1) THEN Thin (-1)⋅)
   THEN (D (-1) THENA (Auto THEN With ⌈0⌉ (D 0)⋅ THEN Auto THEN RWO "select0" 0 THEN Auto))
   THEN InstLemma `es-pred_property` [⌈es⌉;⌈hd((e1, e2))⌉]⋅
   THEN Auto
   THEN (InstHyp [⌈e1⌉] (-1)⋅ THENA Auto)
   THEN D (-1)
   THEN Auto
   THEN Assert ⌈False⌉⋅
   THEN Auto) }

1
.....assertion..... 
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))))
⊢ False

---

Latex:


\mforall{}[es:EO].  \mforall{}[e1,e2:E].    pred(hd((e1,  e2)))  =  e1  supposing  ||(e1,  e2)||  >  0


By

(Auto
  THEN  (InstLemma  `member-es-open-interval`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}hd((e1,  e2))\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  (-1)  THEN  Thin  (-1)\mcdot{})
  THEN  (D  (-1)  THENA  (Auto  THEN  With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  RWO  "select0"  0  THEN  Auto))
  THEN  InstLemma  `es-pred\_property`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}hd((e1,  e2))\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}e1\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Auto
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index