Nuprl - Proof: gcd p neg arg

(4steps 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 neg arg

a,b,y:

. GCD(a;b;y)

GCD(a;-b;y)

By:	Unfold `gcd_p` 0

Generated subgoals:

1 1. a :
2. b :
3. y :
4. y | a
5. y | b
6. z:. z | a & z | b  z | y
  y | -b
1 step

2 1. a :
2. b :
3. y :
4. y | a
5. y | b
6. z:. z | a & z | b  z | y
7. z :
8. z | a
9. z | -b
  z | y
2 steps

About:

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

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

1	1. a : 2. b : 3. y : 4. y \| a 5. y \| b 6. z:. z \| a & z \| b z \| y y \| -b	1 step
2	1. a : 2. b : 3. y : 4. y \| a 5. y \| b 6. z:. z \| a & z \| b z \| y 7. z : 8. z \| a 9. z \| -b z \| y	2 steps