---

Step * 1 1 of Lemma es-before-decomp

.....antecedent..... 
1. the_es : EO@i'
2. e' : E@i
3. e : E@i
4. l1 : E List
5. l2 : E List
6. before(e') = (l1 @ [e] @ l2) ∈ (E List)
⊢ ||l1|| < ||before(e')||
BY
{ (((HypSubst (-1) 0) THENM RWW "length_append" 0) THEN Auto') }

---

Latex:


.....antecedent..... 
1.  the$_{es}$  :  EO@i'
2.  e'  :  E@i
3.  e  :  E@i
4.  l1  :  E  List
5.  l2  :  E  List
6.  before(e')  =  (l1  @  [e]  @  l2)
\mvdash{}  ||l1||  <  ||before(e')||


By

(((HypSubst  (-1)  0)  THENM  RWW  "length\_append"  0)  THEN  Auto')

---

Home Index