Nuprl - Proof: gcd p shift

(12steps 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 shift

a,b,y,k:

. GCD(a;b;y)

GCD(a;b+k

a;y)

By:	Unfold `gcd_p` 0

Generated subgoals:

1 1. a :
2. b :
3. y :
4. k :
5. y | a
6. y | b
7. z:. z | a & z | b  z | y
  y | b+ka
4 steps

2 1. a :
2. b :
3. y :
4. k :
5. y | a
6. y | b
7. z:. z | a & z | b  z | y
8. z :
9. z | a
10. z | b+ka
  z | y
7 steps

About:

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

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

1	1. a : 2. b : 3. y : 4. k : 5. y \| a 6. y \| b 7. z:. z \| a & z \| b z \| y y \| b+ka	4 steps
2	1. a : 2. b : 3. y : 4. k : 5. y \| a 6. y \| b 7. z:. z \| a & z \| b z \| y 8. z : 9. z \| a 10. z \| b+ka z \| y	7 steps