|
%------------------------------------------------------------------------------
% Enumerations of finite sets
%
% MODIFICATIONS:
%
% Author: David Lester, Manchester University 12/12/07
%
%------------------------------------------------------------------------------
finite_enumeration[T:TYPE]: THEORY
BEGIN
finite_enumeration(X:finite_set[T]): [below[card(X)]->(X)]
= choose({f:[below[card(X)]->(X)] | bijective?[below[card(X)],(X)](f)})
X: VAR finite_set[T]
finite_enumeration_bij: LEMMA
bijective?[below[card(X)],(X)](finite_enumeration(X))
finite_enumeration_image: LEMMA
image(finite_enumeration(X),fullset[below[card(X)]]) = X
END finite_enumeration
¤ Dauer der Verarbeitung: 0.70 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
