---

Step * of Lemma empty_spr

g: List  . (spr(g)  ((g []) > 0)  (a: List. ((g a) > 0)))
BY
{ Auto }

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


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


By

Auto



Home Index