---

Step * 1 of Lemma spr_choice_fun


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))
BY
{ (InstConcl [a.if (g a = 0) then fst(((fst((f a))) )) else 0 fi ] THEN Auto) }

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
3. a :  List@i
4. (g a) = 0@i
 (g (a @ [(a.if (g a = 0) then fst(((fst((f a))) )) else 0 fi ) a])) = 0



1.  g  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
2.  f  :  \mforall{}a:\mBbbN{}  List
                  ((((g  a)  =  0)  {}\mRightarrow{}  (\mexists{}s:\mBbbN{}.  ((g  (a  @  [s]))  =  0)))
                  \mwedge{}  (((g  a)  >  0)  {}\mRightarrow{}  (\mforall{}s:\mBbbN{}.  ((g  (a  @  [s]))  >  0))))@i
\mvdash{}  \mexists{}h:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.  \mforall{}a:\mBbbN{}  List.  (((g  a)  =  0)  {}\mRightarrow{}  ((g  (a  @  [h  a]))  =  0))


By

(InstConcl  [\mkleeneopen{}\mlambda{}a.if  (g  a  =\msubz{}  0)  then  fst(((fst((f  a)))  \mcdot{}))  else  0  fi  \mkleeneclose{}]\mcdot{}  THEN  Auto)



Home Index