---

Step * 1 of Lemma in_fspr_iff_in_spr_of_fin_spr


1. B :  List  @i
2. f :   @i
3. (f  spr(a.if (a  fspr(B)) then 0 else 1 fi ))@i
 (f  fspr(B))
BY
{ (Unfold `in_fin_spr` 0 THEN Unfold `in_spr` (-1) THEN Reduce (-1)) }

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



1.  B  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
2.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}@i
3.  (f  \mmember{}  spr(\mlambda{}a.if  (a  \mmember{}  fspr(B))  then  0  else  1  fi  ))@i
\mvdash{}  (f  \mmember{}  fspr(B))


By

(Unfold  `in\_fin\_spr`  0  THEN  Unfold  `in\_spr`  (-1)  THEN  Reduce  (-1))\mcdot{}



Home Index