2. i :
3. p(i)
(least i:. p(i)) 
{i:| p(i) & (
j:. j<i 
p(j)) }
(least i:. p(i)) {i:| p(i) & (j:. j<i p(j)) }| By: |
Thm* k:, p:{p:(k)|  i:k. p(i) }.
Thm* (least i: . p(i)) {i:k| p(i) & (j:i. p(j)) }
on [i+1 | p] |
| 1 |
p {p:((i+1))| i:(i+1). p(i) } | 2 steps |
| 2 |
. p(i)) {i:(i+1)| p(i) & (j:i. p(j)) }
(least i:. p(i)) {i:| p(i) & (j:. j<i p(j)) } | 5 steps |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |