---

Step * 2 1 of Lemma in_fspr_iff_in_spr_of_fin_spr


1. B :  List  @i
2. f :   @i
3. n:. ((f n)  (B mklist(n;f)))@i
4. x : @i
 if (mklist(x;f)  fspr(B)) then 0 else 1 fi  = 0
BY
{ (RWO "boolean_as_01" 0 THEN Auto) }

1
1. B :  List  @i
2. f :   @i
3. n:. ((f n)  (B mklist(n;f)))@i
4. x : @i
 (mklist(x;f)  fspr(B))



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


By

(RWO  "boolean\_as\_01"  0  THEN  Auto)



Home Index