---

Step * 2 of Lemma in_fspr_iff_in_spr_of_fin_spr


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

1
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



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


By

(Unfold  `in\_fin\_spr`  (-1)  THEN  Unfold  `in\_spr`  (0)  THEN  All  Reduce    THEN  Auto)



Home Index