---

Step * 1 of Lemma negated_spr_append_back_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. (g a) > 0@i
5. b :  List@i
 (g (a @ b)) > 0
BY
{ (InstLemma `last_induction` [;b.((g (a @ b)) > 0)] THEN Auto THEN All (RepUR ``so_apply``) THEN Auto) }

1
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. (g a) > 0@i
5. b :  List@i
 (g (a @ [])) > 0

2
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. (g a) > 0@i
5. b :  List@i
6. ys :  List@i
7. y : @i
8. (g (a @ ys)) > 0@i
 (g (a @ ys @ [y])) > 0



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.  (g  a)  >  0@i
5.  b  :  \mBbbN{}  List@i
\mvdash{}  (g  (a  @  b))  >  0


By

(InstLemma  `last\_induction`  [\mkleeneopen{}\mBbbN{}\mkleeneclose{};\mkleeneopen{}\mlambda{}b.((g  (a  @  b))  >  0)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  All  (RepUR  ``so\_apply``)
  THEN  Auto)



Home Index