---

Step * 1 of Lemma es-hist-partition

.....subterm..... T:t
2:n
1. Info : Type
2. es : EO+(Info)
3. e1 : E
4. e2 : E
5. e : E
6. (e1 <loc e)
7. e ≤loc e2 
⊢ [e1, e2] = ([e1, pred(e)] @ [e, e2]) ∈ (E List)
BY
{ ((InstLemma `es-interval-partition` [⌈es⌉; ⌈e2⌉; ⌈e1⌉; ⌈e⌉])⋅ THENA Auto) }

1
1. Info : Type
2. es : EO+(Info)
3. e1 : E
4. e2 : E
5. e : E
6. (e1 <loc e)
7. e ≤loc e2 
8. [e1, e2] = ([e1, pred(e)] @ [e, e2]) ∈ (E List)
⊢ [e1, e2] = ([e1, pred(e)] @ [e, e2]) ∈ (E List)

---

Latex:


.....subterm.....  T:t
2:n
1.  Info  :  Type
2.  es  :  EO+(Info)
3.  e1  :  E
4.  e2  :  E
5.  e  :  E
6.  (e1  <loc  e)
7.  e  \mleq{}loc  e2 
\mvdash{}  [e1,  e2]  =  ([e1,  pred(e)]  @  [e,  e2])


By

((InstLemma  `es-interval-partition`  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}e2\mkleeneclose{};  \mkleeneopen{}e1\mkleeneclose{};  \mkleeneopen{}e\mkleeneclose{}])\mcdot{}  THENA  Auto)

---

Home Index