Step
*
1
1
1
1
1
of Lemma
fin_spr_is_spr
1. B : 
 List 
 
@i
2. a : 
 List@i
3. ||a @ [0]|| 
 0
4. 0 = 0@i
5. 
(a 
 fspr(B))
 
((firstn(||a @ [0]|| - 1;a @ [0]) 
 fspr(B)) 
 last(a @ [0]) 
z B firstn(||a @ [0]|| - 1;a @ [0]))
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.  ||a  @  [0]||  \mneq{}  0
4.  0  =  0@i
5.  \muparrow{}(a  \mmember{}  fspr(B))
\mvdash{}  \muparrow{}((firstn(||a  @  [0]||  -  1;a  @  [0])  \mmember{}  fspr(B))
\mwedge{}\msubb{}  last(a  @  [0])  \mleq{}z  B  firstn(||a  @  [0]||  -  1;a  @  [0]))
By
((RWO  "firstn\_append\_front\_singleton"  0  THEN  Auto)  THEN  RWO  "last\_append\_singleton\_sq"  0  THEN  Auto)
Home
Index