---

Step * 1 1 1 1 of Lemma fin_spr_is_spr


1. B :  List  @i
2. a :  List@i
3. 0 = 0@i
4. (a  fspr(B))
 if (||a @ [0]|| = 0)
then tt
else (firstn(||a @ [0]|| - 1;a @ [0])  fspr(B))  last(a @ [0]) z B firstn(||a @ [0]|| - 1;a @ [0])
fi 
BY
{ AutoSplit }

1
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]))



1.  B  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
2.  a  :  \mBbbN{}  List@i
3.  0  =  0@i
4.  \muparrow{}(a  \mmember{}  fspr(B))
\mvdash{}  \muparrow{}if  (||a  @  [0]||  =\msubz{}  0)
then  tt
else  (firstn(||a  @  [0]||  -  1;a  @  [0])  \mmember{}  fspr(B))
          \mwedge{}\msubb{}  last(a  @  [0])  \mleq{}z  B  firstn(||a  @  [0]||  -  1;a  @  [0])
fi 


By

AutoSplit



Home Index