Nuprl - Proof: factorial tail via iter wf 1

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

1. m :

2. k :

(

i:{k-m..k

}. i+1)

By:	Decide: k-m<0

Generated subgoals:

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

2 3. k-m<0
( i:{k-m..k}. i+1)
Auto

About:

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

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