|
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
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
