---

Step * 1 1 of Lemma empty_spr


1. g :  List  @i
2. spr(g)@i
3. (g []) > 0@i
4. a :  List@i
 (g ([] @ a)) > 0
BY
{ (BLemma `negated_spr_append_back_closed` THEN Auto) }



1.  g  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
2.  spr(g)@i
3.  (g  [])  >  0@i
4.  a  :  \mBbbN{}  List@i
\mvdash{}  (g  ([]  @  a))  >  0


By

(BLemma  `negated\_spr\_append\_back\_closed`  THEN  Auto)



Home Index