---

Step * of Lemma spr_down_closed

g: List  . (spr(g)  (a: List. s:.  (((g (a @ [s])) = 0)  ((g a) = 0))))
BY
{ (Auto THEN Unfold `spr` 2 THEN (InstHyp [a] 2  THENA 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. s : @i
5. (g (a @ [s])) = 0@i
6. (((g a) = 0)  (s:. ((g (a @ [s])) = 0)))  (((g a) > 0)  (s:. ((g (a @ [s])) > 0)))
 (g a) = 0


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


By

(Auto  THEN  Unfold  `spr`  2  THEN  (InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  2  \mcdot{}  THENA  Auto))



Home Index