(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. f : 
2. g : 
3. b : 
4. f zero beyond b
5. a : 
6. g zero beyond a
7. y : 
8. max(a;b)<y
  if y even f(y) else g(y) fi = 0
By: SplitOnConclITE

Generated subgoals:

1 9. y even
  f(y) = 0  
2 steps
2 9. y even
  g(y) = 0  
2 steps

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

(9steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc