---

Step * 1 2 1 1 1 1 2 1 of Lemma FIM26_5


1. B :     @i'
2. s,z,w:.  ((B s z)  (w  z )  (B s w))@i
3. b : 
4. 0 < b
5. s:. ((s  b)  (z:. (B s z)))@i
6. z : 
7. B b z
8. z1 : 
9. s:. ((s  (b - 1))  (B s z1))
10. B b imax(z1;z)
11. s:. ((s  (b - 1))  (B s imax(z1;z)))
12. s : @i
13. s  b@i
 B s imax(z1;z)
BY
{ (Assert (s = b)  (s < b) BY
         MaAuto) }

1
1. B :     @i'
2. s,z,w:.  ((B s z)  (w  z )  (B s w))@i
3. b : 
4. 0 < b
5. s:. ((s  b)  (z:. (B s z)))@i
6. z : 
7. B b z
8. z1 : 
9. s:. ((s  (b - 1))  (B s z1))
10. B b imax(z1;z)
11. s:. ((s  (b - 1))  (B s imax(z1;z)))
12. s : @i
13. s  b@i
14. (s = b)  (s < b)
 B s imax(z1;z)



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.  b  :  \mBbbZ{}
4.  0  <  b
5.  \mforall{}s:\mBbbN{}.  ((s  \mleq{}  b)  {}\mRightarrow{}  (\mexists{}z:\mBbbN{}.  (B  s  z)))@i
6.  z  :  \mBbbN{}
7.  B  b  z
8.  z1  :  \mBbbN{}
9.  \mforall{}s:\mBbbN{}.  ((s  \mleq{}  (b  -  1))  {}\mRightarrow{}  (B  s  z1))
10.  B  b  imax(z1;z)
11.  \mforall{}s:\mBbbN{}.  ((s  \mleq{}  (b  -  1))  {}\mRightarrow{}  (B  s  imax(z1;z)))
12.  s  :  \mBbbN{}@i
13.  s  \mleq{}  b@i
\mvdash{}  B  s  imax(z1;z)


By

(Assert  (s  =  b)  \mvee{}  (s  <  b)  BY
              MaAuto)



Home Index