---

Step * of Lemma fin_spr_is_spr

B: List  . spr(a.if (a  fspr(B)) then 0 else 1 fi )
BY
{ (Unfold `spr` 0 THEN Reduce 0 THEN Auto) }

1
1. B :  List  @i
2. a :  List@i
3. if (a  fspr(B)) then 0 else 1 fi  = 0@i
 s:. (if (a @ [s]  fspr(B)) then 0 else 1 fi  = 0)

2
1. B :  List  @i
2. a :  List@i
3. if (a  fspr(B)) then 0 else 1 fi  > 0@i
4. s : @i
 if (a @ [s]  fspr(B)) then 0 else 1 fi  > 0


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


By

(Unfold  `spr`  0  THEN  Reduce  0  THEN  Auto)



Home Index