|
%------------------------------------------------------------------------------
% Cyclic monoids
%
% 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
%------------------------------------------------------------------------------
cyclic_monoid[T:Type+,*:[T,T->T],one:T]: THEORY
BEGIN
ASSUMING IMPORTING cyclic_monoid_def[T,*,one]
fullset_is_cyclic_monoid: ASSUMPTION cyclic_monoid?(fullset[T])
ENDASSUMING
IMPORTING monoid[T,*,one]
cyclic_monoid: TYPE+ = (cyclic_monoid?) CONTAINING fullset[T]
M: VAR cyclic_monoid
a: VAR T
n: VAR nat
cyclic_monoid_is: LEMMA cyclic_monoid?(M)
cyclic_monoid_is_monoid: JUDGEMENT cyclic_monoid SUBTYPE_OF monoid
cyclic_monoid_is_commutative_monoid:
JUDGEMENT cyclic_monoid SUBTYPE_OF commutative_monoid
END cyclic_monoid
¤ 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.
|
