Quellcode-Bibliothek sets_lemmas_aux.pvs
Sprache: unbekannt
|
|
% 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
[ 0.6Quellennavigators
Projekt
]
|
2026-03-28
|
