---

Step * 1 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
 s:. (if (a @ [s]  fspr(B)) then 0 else 1 fi  = 0)
BY
{ (SplitOnHypITE (-1) THEN Auto) }

1
.....truecase..... 
1. B :  List  @i
2. a :  List@i
3. 0 = 0@i
4. (a  fspr(B))
 s:. (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
\mvdash{}  \mexists{}s:\mBbbN{}.  (if  (a  @  [s]  \mmember{}  fspr(B))  then  0  else  1  fi    =  0)


By

(SplitOnHypITE  (-1)  THEN  Auto)



Home Index