(21steps total) PrintForm Definitions mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: search property
  k:, P:(k).
  ((i:k. P(i))  0<search(k;P))
  & (0<search(k;P)  P(search(k;P)-1) & (j:k. j<search(k;P)-1  P(j)))
By: Analyze 0 THEN NatInd 1

Generated subgoals:

1   P:(0). 
  ((i:0. P(i))  0<search(0;P))
  & (0<search(0;P)  P(search(0;P)-1) & (j:0. j<search(0;P)-1  P(j)))
1 step
2 1. k : 
2. 0<k
3. P:((k-1)). 
3. ((i:(k-1). P(i))  0<search(k-1;P))
3. & (0<search(k-1;P)
3. & (
3. & (P(search(k-1;P)-1) & (j:(k-1). j<search(k-1;P)-1  P(j)))
  P:(k). 
  ((i:k. P(i))  0<search(k;P))
  & (0<search(k;P)  P(search(k;P)-1) & (j:k. j<search(k;P)-1  P(j)))
19 steps

About:
boolassertnatural_numbersubtractless_thanapplyfunctionimpliesandallexists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(21steps total) PrintForm Definitions mb nat Sections MarkB generic Doc