Nuprl - Proof: factorial tail via iter wf 1 1

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

1. m :

2. k :

3. k-m<0

(

i:{k-m..k

}. i+1)

By:	Guarding ( i:{k-m..k}. i+1) Analyze ...

Generated subgoal:

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

About:

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