---

Step * 1 1 1 1 of Lemma FIM26_5


1. B :     @i'
2. s,z,w:.  ((B s z)  (w  z )  (B s w))@i
3. s:. ((s  0)  (z:. (B s z)))@i
4. z : 
5. B 0 z
6. s : @i
7. s  0@i
 B s z
BY
{ ((Assert s = 0 BY Auto) THEN Auto) }



1.  B  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}@i'
2.  \mforall{}s,z,w:\mBbbN{}.    ((B  s  z)  {}\mRightarrow{}  (w  \mgeq{}  z  )  {}\mRightarrow{}  (B  s  w))@i
3.  \mforall{}s:\mBbbN{}.  ((s  \mleq{}  0)  {}\mRightarrow{}  (\mexists{}z:\mBbbN{}.  (B  s  z)))@i
4.  z  :  \mBbbN{}
5.  B  0  z
6.  s  :  \mBbbN{}@i
7.  s  \mleq{}  0@i
\mvdash{}  B  s  z


By

((Assert  s  =  0  BY  Auto)  THEN  Auto)



Home Index