Nuprl - Proof: factorial tail via iter step 1 1 1

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

1. m :

2. k :

3. 1

m
4. m

k
5. k' :

6. m' :

7. k' = k-1
8. m' = m-1

(

i:{k-m..k-1

}. i+1) = k'!m'

By:	Def of <nat>!<nat>

Generated subgoal:

1 ( i:{k-m..k-1}. i+1) = ( i:{k'-m'..k'}. i+1)
1 step

About:

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