|
%------------------------------------------------------------------------------
% Indexed Set properties
%
% Author: David Lester, Manchester University
%
% Version 1.0 14/06/09 Initial Version
%------------------------------------------------------------------------------
indexed_sets_aux[index, T: TYPE]: THEORY
BEGIN
i,j: VAR index
x: VAR T
A,B: VAR [index -> set[T]]
S: VAR set[T]
disjoint?(A):bool = FORALL i,j: i /= j IMPLIES disjoint?(A(i),A(j))
disjoint_indexed_set: TYPE+ = (disjoint?) CONTAINING (LAMBDA i: emptyset[T])
IComplement(A)(i): set[T] = complement(A(i))
IComplement_IComplement: LEMMA IComplement(IComplement(A)) = A
IDemorgan1: LEMMA complement(IUnion(A)) = IIntersection(IComplement(A))
IDemorgan2: LEMMA complement(IIntersection(A)) = IUnion(IComplement(A))
END indexed_sets_aux
¤ Dauer der Verarbeitung: 0.16 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.
|
