---

Step * 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
{ (Subst a = ([] @ a) 0 THEN Auto) }

1
1. g :  List  @i
2. spr(g)@i
3. (g []) > 0@i
4. a :  List@i
 (g ([] @ a)) > 0



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

(Subst  \mkleeneopen{}a  =  ([]  @  a)\mkleeneclose{}  0\mcdot{}  THEN  Auto)



Home Index