Nuprl - Proof: gcd p mul

(7steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: gcd p mul

a,b,y,n:

. GCD(a;b;y)

GCD(n

a;n

b;n

y)

By:	RWN 2 (UnfoldTopC `gcd_p`) 0 THEN GenUnivCD

Generated subgoals:

1 1. a :
2. b :
3. y :
4. n :
5. GCD(a;b;y)
  ny | na
1 step

2 1. a :
2. b :
3. y :
4. n :
5. GCD(a;b;y)
  ny | nb
1 step

3 1. a :
2. b :
3. y :
4. n :
5. GCD(a;b;y)
6. z :
7. z | na & z | nb
  z | ny
4 steps

About:

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

(7steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc