---

Step * 1 2 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 - 1))  (z:. (B s z))))  (z:. s:. ((s  (b - 1))  (B s z)))
6. s:. ((s  b)  (z:. (B s z)))@i
 z:. s:. ((s  b)  (B s z))
BY
{ ((InstHyp [b] (-1) THENA Auto) THEN skip{(InstHyp [b - 1] (-2) THENA Auto)}) }

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 - 1))  (z:. (B s z))))  (z:. s:. ((s  (b - 1))  (B s z)))
6. s:. ((s  b)  (z:. (B s z)))@i
7. z:. (B b z)
 z:. s:. ((s  b)  (B s 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  -  1))  {}\mRightarrow{}  (\mexists{}z:\mBbbN{}.  (B  s  z))))  {}\mRightarrow{}  (\mexists{}z:\mBbbN{}.  \mforall{}s:\mBbbN{}.  ((s  \mleq{}  (b  -  1))  {}\mRightarrow{}  (B  s  z)))
6.  \mforall{}s:\mBbbN{}.  ((s  \mleq{}  b)  {}\mRightarrow{}  (\mexists{}z:\mBbbN{}.  (B  s  z)))@i
\mvdash{}  \mexists{}z:\mBbbN{}.  \mforall{}s:\mBbbN{}.  ((s  \mleq{}  b)  {}\mRightarrow{}  (B  s  z))


By

((InstHyp  [\mkleeneopen{}b\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  skip\{(InstHyp  [\mkleeneopen{}b  -  1\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)\}\mcdot{})\mcdot{}



Home Index