Nuprl - Proof: gcd of triple

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

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

a,b,c,x,y:

GCD(a;b;x)

GCD(x;c;y)

y | a & y | b & y | c & (

. z | a

z | b

z | c

z | y)

By:	(Unfold `gcd_p` 0 THEN UnivCD) THEN (Analyze 0)

Generated subgoals:

1 1. a :
2. b :
3. c :
4. x :
5. y :
6. x | a & x | b & (z:. z | a & z | b  z | x)
7. y | x & y | c & (z:. z | x & z | c  z | y)
  y | a & y | b & y | c
1 step

2 1. a :
2. b :
3. c :
4. x :
5. y :
6. x | a & x | b & (z:. z | a & z | b  z | x)
7. y | x & y | c & (z:. z | x & z | c  z | y)
  z:. z | a  z | b  z | c  z | y
1 step

About:

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

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

1	1. a : 2. b : 3. c : 4. x : 5. y : 6. x \| a & x \| b & (z:. z \| a & z \| b z \| x) 7. y \| x & y \| c & (z:. z \| x & z \| c z \| y) y \| a & y \| b & y \| c	1 step
2	1. a : 2. b : 3. c : 4. x : 5. y : 6. x \| a & x \| b & (z:. z \| a & z \| b z \| x) 7. y \| x & y \| c & (z:. z \| x & z \| c z \| y) z:. z \| a z \| b z \| c z \| y	1 step