(9steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc alternate zero beyond 1 1 1 1 1
1. f : 
2. g : 
3. b : 
4. f zero beyond b
5. a : 
6. g zero beyond a
7. y : 
8. max(a;b)<y
9. y even
  f(y) = 0  
By: BackThru: f zero beyond b

Generated subgoal:

1   b<y
1 step

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

(9steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc