---

Step * of Lemma negated_spr_append_back_closed

g: List  . (spr(g)  (a: List. (((g a) > 0)  (b: List. ((g (a @ b)) > 0)))))
BY
{ (Auto THEN RepUR ``spr`` 2) }

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 @ b)) > 0


\mforall{}g:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.  (spr(g)  {}\mRightarrow{}  (\mforall{}a:\mBbbN{}  List.  (((g  a)  >  0)  {}\mRightarrow{}  (\mforall{}b:\mBbbN{}  List.  ((g  (a  @  b))  >  0)))))


By

(Auto  THEN  RepUR  ``spr``  2)



Home Index