---

Step * of Lemma es-before-decomp

∀the_es:EO. ∀e',e:E.  ((e ∈ before(e')) ⇒ (∃l:E List. (before(e') = (before(e) @ [e] @ l) ∈ (E List))))
BY
{ (((((Auto THEN (RWO "l_member_decomp" (-1))) THENA Auto) THEN ExRepD THEN (HypSubst (-1) 0)) THENA Auto)
   THEN (InstConcl [⌈l2⌉])⋅
   THEN Auto
   THEN EqCD
   THEN Auto) }

1
.....subterm..... T:t
1: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)
⊢ l1 = before(e) ∈ (E List)

---

Latex:


\mforall{}the$_{es}$:EO.  \mforall{}e',e:E.    ((e  \mmember{}  before(e'))  {}\mRightarrow{}  (\mexists{}l:E  List.  (before(e')  =  (before\000C(e)  @  [e]  @  l))))


By

(((((Auto  THEN  (RWO  "l\_member\_decomp"  (-1)))  THENA  Auto)  THEN  ExRepD  THEN  (HypSubst  (-1)  0))
    THENA  Auto
    )
  THEN  (InstConcl  [\mkleeneopen{}l2\mkleeneclose{}])\mcdot{}
  THEN  Auto
  THEN  EqCD
  THEN  Auto)

---

Home Index