---

Step * of Lemma in_fspr_iff_in_spr_of_fin_spr

B: List  . f:  .  ((f  spr(a.if (a  fspr(B)) then 0 else 1 fi ))  (f  fspr(B)))
BY
{ Auto }

1
1. B :  List  @i
2. f :   @i
3. (f  spr(a.if (a  fspr(B)) then 0 else 1 fi ))@i
 (f  fspr(B))

2
1. B :  List  @i
2. f :   @i
3. (f  fspr(B))@i
 (f  spr(a.if (a  fspr(B)) then 0 else 1 fi ))


\mforall{}B:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    ((f  \mmember{}  spr(\mlambda{}a.if  (a  \mmember{}  fspr(B))  then  0  else  1  fi  ))  \mLeftarrow{}{}\mRightarrow{}  (f  \mmember{}  fspr(B)))


By

Auto



Home Index