---

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

.....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
BY
{ (Assert ⌈(pred(hd((e1, e2))) ∈ (e1, e2))⌉⋅
   THENA (UnfoldAtAddr [2] 0
          THEN GenListD 0
          THEN (RW assert_pushdownC 0 THENA Auto)
          THEN Auto
          THEN GenListD 0
          THEN (Assert ⌈(pred(hd((e1, e2))) <loc hd((e1, e2)))⌉⋅ THEN Auto)
          THEN (FLemma `es-locl_transitivity` [-1;-6] THEN Auto)
          THEN (D 0 THEN Auto)
          THEN (RWO "assert-es-first" (-1) THEN Auto)
          THEN (InstHyp [⌈e1⌉] (-1)⋅ THEN Auto)
          THEN D (-1)
          THEN Auto)
   )⋅ }

1
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. (pred(hd((e1, e2))) ∈ (e1, e2))
⊢ False

---

Latex:


.....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)))
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))))
\mvdash{}  False


By

(Assert  \mkleeneopen{}(pred(hd((e1,  e2)))  \mmember{}  (e1,  e2))\mkleeneclose{}\mcdot{}
  THENA  (UnfoldAtAddr  [2]  0
                THEN  GenListD  0
                THEN  (RW  assert\_pushdownC  0  THENA  Auto)
                THEN  Auto
                THEN  GenListD  0
                THEN  (Assert  \mkleeneopen{}(pred(hd((e1,  e2)))  <loc  hd((e1,  e2)))\mkleeneclose{}\mcdot{}  THEN  Auto)
                THEN  (FLemma  `es-locl\_transitivity`  [-1;-6]  THEN  Auto)
                THEN  (D  0  THEN  Auto)
                THEN  (RWO  "assert-es-first"  (-1)  THEN  Auto)
                THEN  (InstHyp  [\mkleeneopen{}e1\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
                THEN  D  (-1)
                THEN  Auto)
  )\mcdot{}

---

Home Index