Nuprl - Proof: nsub inj factorial tail 1 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub inj factorial tail 1 1 2

1. a :

a1:

. a1<a

(

. (

a1 inj

b) ~

(b!a1))
3. b :

4. a

b
5.

a = 0

(

a inj

b) ~

(b!a)

By:	Rewrite by Thm* m,k:. 1 m k k!m = k(k-1)!(m-1)

Generated subgoal:

1 (a inj b) ~ (b(b-1)!(a-1))
4 steps

About:

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