---

Step * of Lemma FIM26_5

B:    
  ((s,z,w:.  ((B s z)  (w  z )  (B s w)))
   (b:. ((s:. ((s  b)  (z:. (B s z))))  (z:. s:. ((s  b)  (B s z))))))
BY
{ Auto }

1
1. B :     @i'
2. s,z,w:.  ((B s z)  (w  z )  (B s w))@i
3. b : @i
4. s:. ((s  b)  (z:. (B s z)))@i
 z:. s:. ((s  b)  (B s z))


\mforall{}B:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
    ((\mforall{}s,z,w:\mBbbN{}.    ((B  s  z)  {}\mRightarrow{}  (w  \mgeq{}  z  )  {}\mRightarrow{}  (B  s  w)))
    {}\mRightarrow{}  (\mforall{}b:\mBbbN{}.  ((\mforall{}s:\mBbbN{}.  ((s  \mleq{}  b)  {}\mRightarrow{}  (\mexists{}z:\mBbbN{}.  (B  s  z))))  {}\mRightarrow{}  (\mexists{}z:\mBbbN{}.  \mforall{}s:\mBbbN{}.  ((s  \mleq{}  b)  {}\mRightarrow{}  (B  s  z))))))


By

Auto



Home Index