---

Step * 2 1 1 1 of Lemma fin_spr_is_spr


1. B :  List  @i
2. a :  List@i
3. 1 > 0@i
4. s : @i
5. ||a @ [s]||  0
6. (a  fspr(B))
 ((firstn(||a @ [s]|| - 1;a @ [s])  fspr(B))  last(a @ [s]) z B firstn(||a @ [s]|| - 1;a @ [s]))
BY
{ ((RWO "firstn_append_front_singleton" 0 THEN Auto) THEN RWO "last_append_singleton_sq" 0 THEN Auto) }



1.  B  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
2.  a  :  \mBbbN{}  List@i
3.  1  >  0@i
4.  s  :  \mBbbN{}@i
5.  ||a  @  [s]||  \mneq{}  0
6.  \mneg{}\muparrow{}(a  \mmember{}  fspr(B))
\mvdash{}  \mneg{}\muparrow{}((firstn(||a  @  [s]||  -  1;a  @  [s])  \mmember{}  fspr(B))
\mwedge{}\msubb{}  last(a  @  [s])  \mleq{}z  B  firstn(||a  @  [s]||  -  1;a  @  [s]))


By

((RWO  "firstn\_append\_front\_singleton"  0  THEN  Auto)  THEN  RWO  "last\_append\_singleton\_sq"  0  THEN  Auto)\mcdot{}
\mcdot{}



Home Index