---

Step * of Lemma fin_spr_as_list

f:  . B: List  .  ((x:. (if (mklist(x;f)  fspr(B)) then 0 else 1 fi  = 0))  (f  fin_spr(B)))
BY
{ Auto }

1
1. f :   @i
2. B :  List  @i
3. x:. (if (mklist(x;f)  fspr(B)) then 0 else 1 fi  = 0)@i
 f  fin_spr(B)


\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}B:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.
    ((\mforall{}x:\mBbbN{}.  (if  (mklist(x;f)  \mmember{}  fspr(B))  then  0  else  1  fi    =  0))  {}\mRightarrow{}  (f  \mmember{}  fin\_spr(B)))


By

Auto



Home Index