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 */ (NATURAL >-> NATURAL) <: (NATURAL >->> NATURAL) & /* Exercise 13 */ !(ss, xx) . (ss : FIN(NATURAL) & xx : ss => (xx <= SIGMA(zz) . (zz : ss | zz))) & /* Exercise 14 */ !(ss, tt) . (ss : FIN(UNIVERSE) & tt : FIN(UNIVERSE) => (ss <: tt => card(ss) <= card(tt))) & /* Exercise 15 */ !(ss, tt) . (ss : FIN(UNIVERSE) & tt : FIN(UNIVERSE) => (card(ss) <= card(tt) <=> (ss >-> tt) /= {})) & /* Exercise 16 */ !(ss, tt) . (ss : FIN(UNIVERSE) & tt : FIN(UNIVERSE) => (card(ss) >= card(tt) <=> (ss -->> 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