---

Step * 1 1 1 1 1 of Lemma spr_down_closed


1. g :  List  @i
2. a: List. ((((g a) = 0)  (s:. ((g (a @ [s])) = 0)))  (((g a) > 0)  (s:. ((g (a @ [s])) > 0))))@i
3. a :  List@i
4. s : @i
5. (g (a @ [s])) = 0@i
6. ((g a) = 0)  (s:. ((g (a @ [s])) = 0))
7. ((g a) > 0)  (s:. ((g (a @ [s])) > 0))
8. s:. ((g (a @ [s])) > 0)@i
 False
BY
{ (InstHyp [s] (-1)  THEN Auto) }



1.  g  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
2.  \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
3.  a  :  \mBbbN{}  List@i
4.  s  :  \mBbbN{}@i
5.  (g  (a  @  [s]))  =  0@i
6.  ((g  a)  =  0)  {}\mRightarrow{}  (\mexists{}s:\mBbbN{}.  ((g  (a  @  [s]))  =  0))
7.  ((g  a)  >  0)  {}\mRightarrow{}  (\mforall{}s:\mBbbN{}.  ((g  (a  @  [s]))  >  0))
8.  \mforall{}s:\mBbbN{}.  ((g  (a  @  [s]))  >  0)@i
\mvdash{}  False


By

(InstHyp  [\mkleeneopen{}s\mkleeneclose{}]  (-1)  \mcdot{}  THEN  Auto)\mcdot{}



Home Index