---

Step * 1 1 of Lemma fin_spr_is_spr

.....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)
BY
{ (InstConcl [0] THEN Auto) }

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


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


By

(InstConcl  [\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THEN  Auto)



Home Index