---

Step * 2 2 of Lemma iseg-es-hist


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. L : Info List@i
7. loc(e1) = loc(j) ∈ Id
8. ¬(L = [] ∈ (Info List))
9. L ≤ es-hist(es;e1;j)@i
10. e1 = j ∈ E
⊢ ∃e∈[e1,j].L = es-hist(es;e1;e) ∈ (Info List)
BY
{ (UnfoldTopAb 0 THEN (InstConcl [⌈j⌉])⋅ THEN Auto⋅)⋅ }

1
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. L : Info List@i
7. loc(e1) = loc(j) ∈ Id
8. ¬(L = [] ∈ (Info List))
9. L ≤ es-hist(es;e1;j)@i
10. e1 = j ∈ E
11. e1 ≤loc j 
12. j ≤loc j 
⊢ L = es-hist(es;e1;j) ∈ (Info List)

---

Latex:



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.  L  :  Info  List@i
7.  loc(e1)  =  loc(j)
8.  \mneg{}(L  =  [])
9.  L  \mleq{}  es-hist(es;e1;j)@i
10.  e1  =  j
\mvdash{}  \mexists{}e\mmember{}[e1,j].L  =  es-hist(es;e1;e)


By

(UnfoldTopAb  0  THEN  (InstConcl  [\mkleeneopen{}j\mkleeneclose{}])\mcdot{}  THEN  Auto\mcdot{})\mcdot{}

---

Home Index