Nuprl - Proof: card pi vs nsub pi 2 1 1 1

(11steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card pi vs nsub pi 2 1 1 1

1. a :

2. 0<a
3.

b:(

(a-1)

). (i:

(a-1)

b(i)) ~

(

i:

(a-1). b(i))
4. b :

a

(

(

i:

(a-1). b(i))

b(a-1)) ~

((

i:

(a-1). b(i))

b(a-1))

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

Generated subgoal:

1 5. x :
6. y :
xy
1 step

About:

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

(11steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc