(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 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)))
By: Unfold `search` 0 THEN Reduce 0 THEN ExRepD

Generated subgoals:

None

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