Nuprl - Proof: factorial via iter wf 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: factorial via iter wf 1 1 1 1

1. k :

(

i:{(k-k)..k

}. i+1 = 0)

By:	Analyze ...w

Generated subgoal:

1 2. i:{(k-k)..k}. i+1 = 0
False
2 steps

About:

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