/* * Definition of divisibility and greatest common divisor. * * Note: these definitions assume that their arguments are natural numbers. */ DEFINITIONS Divides (d, n) == (#kk . (kk : NATURAL & (n) = kk*(d))) ; /* * CD (p, x, y) means that p is a common divisor of x and y. */ CD (p, x, y) == (Divides((p), (x)) & Divides((p), (y))) ; /* * GCD (p, x, y) means that p is the greatest common divisor of x and y. */ GCD (p, x, y) == (CD((p), (x), (y)) & !qq . (qq : NATURAL & CD(qq, (x), (y)) => qq <= (p)))