---

Step * of Lemma iseg-es-hist

∀[Info:Type]
  ∀es:EO+(Info). ∀e1,e2:E. ∀L:Info List.
    (L ≤ es-hist(es;e1;e2) ⇒ ∃e∈[e1,e2].L = es-hist(es;e1;e) ∈ (Info List)) supposing 
       ((¬(L = [] ∈ (Info List))) and 
       (loc(e1) = loc(e2) ∈ Id))
BY
{ (RepeatFor 3 ((D 0 THENA Auto)) THEN LocLessInd THEN Auto⋅ THEN Assert ⌈e1 ≤loc j ⌉⋅) }

1
.....assertion..... 
1. [Info] : Type
2. es : EO+(Info)@i'
3. e1 : E@i
4. WellFnd{i}(E;x,y.(x <loc y))
5. j : E@i
6. ∀k:E
     ((k <loc j)
     ⇒ (∀L:Info List
           (L ≤ es-hist(es;e1;k) ⇒ ∃e∈[e1,k].L = es-hist(es;e1;e) ∈ (Info List)) supposing 
              ((¬(L = [] ∈ (Info List))) and 
              (loc(e1) = loc(k) ∈ Id))))@i
7. L : Info List@i
8. loc(e1) = loc(j) ∈ Id
9. ¬(L = [] ∈ (Info List))
10. L ≤ es-hist(es;e1;j)@i
⊢ e1 ≤loc j 

2
1. [Info] : Type
2. es : EO+(Info)@i'
3. e1 : E@i
4. WellFnd{i}(E;x,y.(x <loc y))
5. j : E@i
6. ∀k:E
     ((k <loc j)
     ⇒ (∀L:Info List
           (L ≤ es-hist(es;e1;k) ⇒ ∃e∈[e1,k].L = es-hist(es;e1;e) ∈ (Info List)) supposing 
              ((¬(L = [] ∈ (Info List))) and 
              (loc(e1) = loc(k) ∈ Id))))@i
7. L : Info List@i
8. loc(e1) = loc(j) ∈ Id
9. ¬(L = [] ∈ (Info List))
10. L ≤ es-hist(es;e1;j)@i
11. e1 ≤loc j 
⊢ ∃e∈[e1,j].L = es-hist(es;e1;e) ∈ (Info List)

---

Latex:


\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}e1,e2:E.  \mforall{}L:Info  List.
        (L  \mleq{}  es-hist(es;e1;e2)  {}\mRightarrow{}  \mexists{}e\mmember{}[e1,e2].L  =  es-hist(es;e1;e))  supposing 
              ((\mneg{}(L  =  []))  and 
              (loc(e1)  =  loc(e2)))


By

(RepeatFor  3  ((D  0  THENA  Auto))  THEN  LocLessInd  THEN  Auto\mcdot{}  THEN  Assert  \mkleeneopen{}e1  \mleq{}loc  j  \mkleeneclose{}\mcdot{})

---

Home Index