|
% 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
[ Original von:0.1Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen.
Man kann per Verzeichnistruktur darin navigieren.
Der Code wird farblich markiert angezeigt.
Datei übertragen
]
|
