---

Step * 2 of Lemma fin_spr_is_spr


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
BY
{ (SplitOnHypITE (-2) THEN Auto) }

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



1.  B  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
2.  a  :  \mBbbN{}  List@i
3.  if  (a  \mmember{}  fspr(B))  then  0  else  1  fi    >  0@i
4.  s  :  \mBbbN{}@i
\mvdash{}  if  (a  @  [s]  \mmember{}  fspr(B))  then  0  else  1  fi    >  0


By

(SplitOnHypITE  (-2)  THEN  Auto)\mcdot{}



Home Index