Nuprl - Proof: nsub inj factorial tail 1 1 2 1 1 1 1

(17steps total) Remark PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

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

1. a :

2.

a1:

. a1<a

(

b:

. (

a1 inj

b) ~

(b!a1))
3. b :

4. a

b
5.

a = 0

(

b

((-1+b)!(-1+a))) ~

(b

(-1+b)!(-1+a))

By:	Rewrite by Thm* a,b:. (ab) ~ (ab)

Generated subgoals:

None

About:

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

(17steps total) Remark PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc