Nuprl Basics - Proof: sfa doc alternate zero beyond 1 1 1 1 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc alternate zero beyond 1 1 1 1 2 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

a<y

By:	(8) Def of max(a;b) THEN SplitITE Hyp:-2

Generated subgoals:

None

About:

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