Nuprl Basics - Proof: sfa doc factorial2 wf 1 1 2 1 1 2 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc factorial2 wf 1 1 2 1 1 2 2

1. x :

x1:

. x1<x

x1!

(given (x1 rem 2) = 0)
3. x

0
4. (x rem 2) = 0
5. (x rem 2) = 0
6. 2

(x-2)!

By:	FwdThru: Hyp:2 on [ x-2<x ]

Generated subgoals:

1   x-2
1 step

2 7. (x-2)!  (given ((x-2) rem 2) = 0)
  (x-2)!
3 steps

About:

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

1	x-2	1 step
2	7. (x-2)! (given ((x-2) rem 2) = 0) (x-2)!	3 steps