---

Step * 1 2 of Lemma es-before-decomp


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||])
⊢ l1 = before(e) ∈ (E List)
BY
{ ((((((ApFunToHypEquands `z' ⌈firstn(||l1||;z)⌉ ⌈E List⌉ (-2))⋅ THENA Auto) THEN (RWO "firstn_append" (-1)))
     THENA Auto'
     )
    THEN (RWO "firstn_length" (-1))
    )
   THENA Auto'
   ) }

1
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 = before(e) ∈ (E List)

---

Latex:



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||])
\mvdash{}  l1  =  before(e)


By

((((((ApFunToHypEquands  `z'  \mkleeneopen{}firstn(||l1||;z)\mkleeneclose{}  \mkleeneopen{}E  List\mkleeneclose{}  (-2))\mcdot{}  THENA  Auto)
        THEN  (RWO  "firstn\_append"  (-1))
        )
      THENA  Auto'
      )
    THEN  (RWO  "firstn\_length"  (-1))
    )
  THENA  Auto'
  )

---

Home Index