MACHINE NatAsserts DEFINITIONS Divides (d, n) == (#kk . (kk : NATURAL & (n) = kk*(d))) ASSERTIONS /* Exercise 1 */ #nn . (nn : NATURAL & !mm . (mm : NATURAL => nn <= mm)) & /* Exercise 2 */ !nn . (nn : NATURAL => #mm . (mm : NATURAL & mm > nn)) & /* Exercise 3 */ !(nn, mm) . (nn : NATURAL & mm : NATURAL & nn /= mm => (nn < mm or nn > mm)) & /* Exercise 4 */ !nn . (nn : NATURAL => ((nn mod 2 = 0) or (nn mod 2 = 1))) & /* Exercise 5 */ !nn . (nn : NATURAL => Divides(nn, nn) & Divides(nn, 0)) & /* Exercise 6 */ #nn . (nn : NATURAL & !mm . (mm : NATURAL => Divides(nn, mm))) & /* Exercise 7 */ !(dd, nn) . (dd : NATURAL1 & nn : NATURAL => (Divides(dd, nn) <=> (nn mod dd = 0))) & /* Exercise 8 */ !(xx, yy, zz) . (xx : NATURAL & yy : NATURAL & zz : NATURAL => (Divides(xx, xx)) & (Divides(xx, yy) & Divides(yy, zz) => Divides(xx, zz)) & (Divides(xx, yy) & Divides(yy, xx) => xx = yy)) END