Nuprl - Proof: factorial tail via iter step 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. 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-1+1) = k

k'!m'

By:	BackThru: Thm* a,b,c,d:. a = b c = d ac = db ...

Generated subgoal:

1 ( i:{k-m..k-1}. i+1) = k'!m'
2 steps

About:

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