b:
, a:
. 
y:. GCD(a;b;y)a:. GCD(a;0;a)a:, b:
. q:, r:b. a = q
b+ra,b,y:. GCD(a;b;y) 
GCD(b;a;y)a,b:. ab = baa,b:. a+b = b+aa,b,y,k:. GCD(a;b;y) GCD(a;b+ka;y)| Rank | Theorem | Name |
| 2 | b:, a:. y:. GCD(a;b;y) | [gcd_exists_n] |
| cites the following: | ||
| 1 | a:. GCD(a;0;a) | [gcd_p_zero] |
| 1 | a:, b:. q:, r:b. a = qb+r | [quot_rem_exists] |
| 0 | a,b,y:. GCD(a;b;y) GCD(b;a;y) | [gcd_p_sym] |
| 0 | a,b:. ab = ba | [mul_com] |
| 0 | a,b:. a+b = b+a | [add_com] |
| 1 | a,b,y,k:. GCD(a;b;y) GCD(a;b+ka;y) | [gcd_p_shift] |