|
%------------------------------------------------------------------------------
% Semigroups
%
% Author: David Lester, Manchester University & NIA
% Rick Butler
%
% Version 1.0 3/1/02
% Version 1.1 12/3/03 New library structure
% Version 1.2 5/5/04 Reworked for definition files DRL
%------------------------------------------------------------------------------
semigroup[T:Type+,*:[T,T->T]]: THEORY
BEGIN
ASSUMING IMPORTING semigroup_def[T,*]
fullset_is_semigroup: ASSUMPTION semigroup?(fullset[T])
ENDASSUMING
IMPORTING semigroup_def, groupoid[T,*]
semigroup: TYPE+ = (semigroup?) CONTAINING fullset[T]
x,y,z: VAR T
associative: LEMMA (x * y) * z = x * (y * z)
semigroup_is_groupoid: JUDGEMENT semigroup SUBTYPE_OF groupoid
END semigroup
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
