---

Step * 1 2 of Lemma select_append_back


1. T : Type
2. bs : T List
3. u : T
4. v : T List
5. ∀i:{||v||..||v|| + ||bs||-}. (v @ bs[i] = bs[i - ||v||] ∈ T)
6. i : {||v|| + 1..(||v|| + 1) + ||bs||-}
⊢ [u / (v @ bs)][i] = bs[i - ||v|| + 1] ∈ T
BY
{ (RWW "select_cons_tl 5" 0 THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  bs  :  T  List
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}i:\{||v||..||v||  +  ||bs||\msupminus{}\}.  (v  @  bs[i]  =  bs[i  -  ||v||])
6.  i  :  \{||v||  +  1..(||v||  +  1)  +  ||bs||\msupminus{}\}
\mvdash{}  [u  /  (v  @  bs)][i]  =  bs[i  -  ||v||  +  1]


By

---

Latex:
(RWW  "select\_cons\_tl  5"  0  THEN  Auto')

---

Home Index