|
% various extras for the standard prelude
sets_lemmas_aux[T:TYPE]: THEORY
BEGIN
x, y: VAR T
a, b, c: VAR set[T]
A, B : Var setofsets[T]
IMPORTING sets_lemmas[T]
union_complement: LEMMA union(a,complement(a)) = fullset
intersection_complement: LEMMA intersection(a,complement(a)) = emptyset
disjoint_complement: LEMMA disjoint?(a,complement(a))
disjoint_commutative: LEMMA disjoint?(a,b) = disjoint?(b,a)
disjoint_empty: LEMMA disjoint?(a,emptyset)
powerset_fullset: LEMMA member(a, powerset(a))
union_diff_inter: LEMMA union(difference(a,b),intersection(a,b)) = a
disjoint_diff_inter: LEMMA disjoint?(difference(a,b),intersection(a,b))
disjoint_member: LEMMA disjoint?(a,b) AND member(x,a) IMPLIES
NOT member(x,b)
END sets_lemmas_aux
¤ Dauer der Verarbeitung: 0.0 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.
|
