%------------------------------------------------------------------------------
% Cyclic monoid definition file
%
%     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_def[T:Type+,*:[T,T->T],one:T]: THEORY

BEGIN

   IMPORTING monoid_def[T,*,one]

   S: VAR set[T]
   a: VAR T

   cyclic_monoid?(S):bool = monoid?(S) AND EXISTS (a:(S)): S = generated_set(a)

   finite_cyclic_monoid?(S): bool          = cyclic_monoid?(S) AND is_finite(S)

   commutative_cyclic_monoid?(S): bool        = cyclic_monoid?(S)

   finite_commutative_cyclic_monoid?(S): bool = finite_cyclic_monoid?(S)

END cyclic_monoid_def