---

Step * of Lemma spr_choice_fun

g: List  . (spr(g)  (h: List  . a: List. (((g a) = 0)  ((g (a @ [h a])) = 0))))
BY
{ (Auto THEN Unfold `spr` (-1) THEN RenameVar `f' (-1) ) }

1
1. g :  List  @i
2. f : a: List. ((((g a) = 0)  (s:. ((g (a @ [s])) = 0)))  (((g a) > 0)  (s:. ((g (a @ [s])) > 0))))@i
 h: List  . a: List. (((g a) = 0)  ((g (a @ [h a])) = 0))


\mforall{}g:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.  (spr(g)  {}\mRightarrow{}  (\mexists{}h:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.  \mforall{}a:\mBbbN{}  List.  (((g  a)  =  0)  {}\mRightarrow{}  ((g  (a  @  [h  a]))  =  0))))


By

(Auto  THEN  Unfold  `spr`  (-1)  THEN  RenameVar  `f'  (-1)  )



Home Index