---

Step * 2 1 of Lemma fin_spr_is_spr

.....falsecase..... 
1. B :  List  @i
2. a :  List@i
3. 1 > 0@i
4. s : @i
5. (a  fspr(B))
 if (a @ [s]  fspr(B)) then 0 else 1 fi  > 0
BY
{ ((Assert (a @ [s]  fspr(B)) BY RWO "list-in-fin_spr_unfold" 0) THEN Auto THEN Reduce 0) }

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


.....falsecase..... 
1.  B  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
2.  a  :  \mBbbN{}  List@i
3.  1  >  0@i
4.  s  :  \mBbbN{}@i
5.  \mneg{}\muparrow{}(a  \mmember{}  fspr(B))
\mvdash{}  if  (a  @  [s]  \mmember{}  fspr(B))  then  0  else  1  fi    >  0


By

((Assert  \mneg{}\muparrow{}(a  @  [s]  \mmember{}  fspr(B))  BY  RWO  "list-in-fin\_spr\_unfold"  0)  THEN  Auto  THEN  Reduce  0)\mcdot{}



Home Index