---

Step * 1 1 1 of Lemma iseg-es-le-before


1. es : EO@i'
2. e' : E@i
3. e : E@i
4. (e' <loc e)@i
5. l : E List
6. before(e) = (before(e') @ [e'] @ l) ∈ (E List)
⊢ (before(e) @ [e]) = ((before(e') @ [e']) @ l @ [e]) ∈ (E List)
BY
{ (HypSubst' (-1) 0 THEN Auto) }

1
1. es : EO@i'
2. e' : E@i
3. e : E@i
4. (e' <loc e)@i
5. l : E List
6. before(e) = (before(e') @ [e'] @ l) ∈ (E List)
⊢ ((before(e') @ [e'] @ l) @ [e]) = ((before(e') @ [e']) @ l @ [e]) ∈ (E List)

---

Latex:



1.  es  :  EO@i'
2.  e'  :  E@i
3.  e  :  E@i
4.  (e'  <loc  e)@i
5.  l  :  E  List
6.  before(e)  =  (before(e')  @  [e']  @  l)
\mvdash{}  (before(e)  @  [e])  =  ((before(e')  @  [e'])  @  l  @  [e])


By

(HypSubst'  (-1)  0  THEN  Auto)

---

Home Index