---

Step * 1 of Lemma firstn-le-before


1. the_es : EO
2. e : E
3. n : ℕ
4. n < ||before(e)||
5. firstn(n;before(e)) ~ before(before(e)[n])
⊢ firstn(n + 1;≤loc(e)) ~ ≤loc(before(e)[n])
BY
{ (Unfold `es-le-before` 0 THEN (RevHypSubst (-1) 0 THENA Auto)) }

1
1. the_es : EO
2. e : E
3. n : ℕ
4. n < ||before(e)||
5. firstn(n;before(e)) ~ before(before(e)[n])
⊢ firstn(n + 1;before(e) @ [e]) ~ firstn(n;before(e)) @ [before(e)[n]]

---

Latex:



1.  the$_{es}$  :  EO
2.  e  :  E
3.  n  :  \mBbbN{}
4.  n  <  ||before(e)||
5.  firstn(n;before(e))  \msim{}  before(before(e)[n])
\mvdash{}  firstn(n  +  1;\mleq{}loc(e))  \msim{}  \mleq{}loc(before(e)[n])


By

(Unfold  `es-le-before`  0  THEN  (RevHypSubst  (-1)  0  THENA  Auto))

---

Home Index