---

Step * 1 1 of Lemma in_fspr_iff_in_spr_of_fin_spr


1. B :  List  @i
2. f :   @i
3. x:. (if (mklist(x;f)  fspr(B)) then 0 else 1 fi  = 0)@i
 n:. ((f n)  (B mklist(n;f)))
BY
{ ((FLemma `fin_spr_as_list` [3] THEN Auto)
   THEN (Unfold `fin_spr` 4 THEN MaAuto)
   THEN (MemTypeHD 4 THEN Auto)
   THEN Unhide
   THEN Auto) }



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


By

((FLemma  `fin\_spr\_as\_list`  [3]  THEN  Auto)\mcdot{}
  THEN  (Unfold  `fin\_spr`  4  THEN  MaAuto)
  THEN  (MemTypeHD  4  THEN  Auto)
  THEN  Unhide
  THEN  Auto)



Home Index