Nuprl - Proof: factorial tail via iter step 1 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

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) = (

i:{k'-m'..k'

}. i+1)

By:	Rewrite by k' = k-1 ... THEN Rewrite by m' = m-1 ...

Generated subgoals:

None

About:

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