doubletons[T: TYPE]: THEORY BEGIN x,y,z: VAR T dbl(x,y): set[T] = {t: T | t = x OR t = y} S: VAR set[T] doubleton?(S): bool = (EXISTS x,y: x /= y AND S = dbl(x,y)) doubleton: TYPE = {S | EXISTS x,y: x /= y AND S = dbl(x,y)} Dbl: TYPE = doubleton dbl_comm: LEMMA dbl(x,y) = dbl(y,x) D: VAR doubleton doubleton_irreflexive : LEMMA NOT doubleton?(dbl(x,x)) doubleton_nonempty : LEMMA nonempty?(D) doubleton_rest_nonempty: LEMMA nonempty?(rest(D)) dbl_choose : LEMMA choose(dbl(x,y)) = x or choose(dbl(x,y)) = y dbl_rest_choose : LEMMA x /= y IMPLIES (choose(dbl(x,y)) /= choose(rest(dbl(x,y)))) AND (choose(rest(dbl(x,y))) = x OR choose(rest(dbl(x,y))) = y) dbl_to_pair(D) : {(x,y) | D = dbl(x,y)} dbl_def : LEMMA dbl(PROJ_1(dbl_to_pair(D)), PROJ_2(dbl_to_pair(D))) = D dbl_in : LEMMA D = dbl(x,y) IMPLIES D(x) AND D(y) dbl_not_in : LEMMA D = dbl(x,y) AND z /= x AND z /= y IMPLIES NOT D(z) dbl_to_pair_lem : LEMMA x /= y IMPLIES dbl_to_pair(dbl(x,y)) = (x,y) OR dbl_to_pair(dbl(x,y)) = (y,x) dbl_to_pair_inverse_l : LEMMA dbl(dbl_to_pair(D)) = D dbl_proj : LEMMA D(PROJ_1(dbl_to_pair(D))) AND D(PROJ_2(dbl_to_pair(D))) v: VAR T proj_dbl: LEMMA (PROJ_1(dbl_to_pair(D)) = v OR PROJ_2(dbl_to_pair(D)) = v) IMPLIES D(v) dbl_eq: LEMMA dbl(x,y) = dbl(v,z) IMPLIES (x = v AND y = z) OR (x = z AND y = v) IMPORTING finite_sets@finite_sets finite_dbl: LEMMA is_finite(dbl(x,y)) END doubletons