a,b:
. GCD(a;b;gcd(a;b))a:. GCD(a;0;a)a:, b:
. |a rem b|<|b|a,b,y,k:. GCD(a;b;y) 
GCD(a;b+k
a;y)a:, n:. (a rem n) = a-(a 
n)na,b,y:. GCD(a;b;y) GCD(b;a;y)| Rank | Theorem | Name |
| 2 | a,b:. GCD(a;b;gcd(a;b)) | [gcd_sat_pred] |
| cites the following: | ||
| 1 | a:. GCD(a;0;a) | [gcd_p_zero] |
| 0 | a:, b:. |a rem b|<|b| | [rem_bounds_z] |
| 1 | a,b,y,k:. GCD(a;b;y) GCD(a;b+ka;y) | [gcd_p_shift] |
| 1 | a:, n:. (a rem n) = a-(a n)n | [rem_to_div] |
| 0 | a,b,y:. GCD(a;b;y) GCD(b;a;y) | [gcd_p_sym] |