---

Step * 1 of Lemma fin_spr_as_list


1. f :   @i
2. B :  List  @i
3. x:. (if (mklist(x;f)  fspr(B)) then 0 else 1 fi  = 0)@i
 f  fin_spr(B)
BY
{ (Unfold `fin_spr` 0 THEN MaAuto) }

1
1. f :   @i
2. B :  List  @i
3. x:. (if (mklist(x;f)  fspr(B)) then 0 else 1 fi  = 0)@i
4. n : @i
 (f n)  (B mklist(n;f))



1.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}@i
2.  B  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
3.  \mforall{}x:\mBbbN{}.  (if  (mklist(x;f)  \mmember{}  fspr(B))  then  0  else  1  fi    =  0)@i
\mvdash{}  f  \mmember{}  fin\_spr(B)


By

(Unfold  `fin\_spr`  0  THEN  MaAuto)\mcdot{}



Home Index