---

Step * 1 2 1 1 1 of Lemma es-before-decomp

.....subterm..... T:t
2:n
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)
7. firstn(||l1||;before(e')) ~ before(before(e')[||l1||])
8. firstn(||l1||;before(e')) = l1 ∈ (E List)
⊢ before(e')[||l1||] = e ∈ E
BY
{ (Subst ⌈before(e') = (l1 @ [e] @ l2) ∈ {l:E List| ||l1|| < ||l||} ⌉ 0⋅ THEN Auto') }

1
.....equality..... 
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)
7. firstn(||l1||;before(e')) ~ before(before(e')[||l1||])
8. firstn(||l1||;before(e')) = l1 ∈ (E List)
⊢ before(e') = (l1 @ [e] @ l2) ∈ {l:E List| ||l1|| < ||l||} 

2
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)
7. firstn(||l1||;before(e')) ~ before(before(e')[||l1||])
8. firstn(||l1||;before(e')) = l1 ∈ (E List)
⊢ l1 @ [e] @ l2[||l1||] = e ∈ E

---

Latex:


.....subterm.....  T:t
2:n
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)
7.  firstn(||l1||;before(e'))  \msim{}  before(before(e')[||l1||])
8.  firstn(||l1||;before(e'))  =  l1
\mvdash{}  before(e')[||l1||]  =  e


By

(Subst  \mkleeneopen{}before(e')  =  (l1  @  [e]  @  l2)\mkleeneclose{}  0\mcdot{}  THEN  Auto')

---

Home Index