MACHINE SetAsserts DEFINITIONS Divides (d, n) == (#kk . (kk : NATURAL & (n) = kk*(d))) SETS UNIVERSE ASSERTIONS /* Exercise 9 */ !ss . (ss : FIN(INTEGER) => #tt . (tt : FIN(INTEGER) & ss <<: tt)) & /* Exercise 10 */ !ss . (ss : FIN(INTEGER) => #(aa, bb) . (aa : INTEGER & bb : INTEGER & ss <: (aa..bb))) & /* Exercise 11 */ !nn . (nn : NATURAL1 => {dd | dd : NATURAL & Divides (dd, nn)} : FIN(NATURAL)) & /* Exercise 12 */ /* * The original statement is invalid. A counterexample is the function * mapping each natural number n to n+1, which is in (NATURAL >-> NATURAL) * but not in (NATURAL >->> NATURAL). * * We fix the statement by expressing that every total injective function * from a finite subset of integers to itself is bijective. */ !ss . (ss : FIN(UNIVERSE) => (ss >-> ss) <: (ss >->> ss)) & /* Exercise 14 */ !(ss, tt) . (ss : FIN(UNIVERSE) & tt : FIN(UNIVERSE) => (ss <: tt => card(ss) <= card(tt))) & /* Exercise 17 */ !(xx, yy, zz) . (xx <: UNIVERSE & yy <: UNIVERSE & zz <: UNIVERSE => (xx <: xx) & (xx <: yy & yy <: zz => xx <: zz) & (xx <: yy & yy <: xx => xx = yy)) & /* Exercise 18 */ !ff . (ff : POW(UNIVERSE) --> POW(UNIVERSE) & (!(xx, yy) . (xx <: UNIVERSE & yy <: UNIVERSE & xx <: yy => ff(xx) <: ff(yy))) => #zz . (zz <: UNIVERSE & ff(zz) = zz)) END