Details About PVS Algebra Library

 

   top_group:
             groupoid,              finite_groupoid,
             commutative_groupoid,  finite_commutative_groupoid,
             monad,                 finite_monad,
             commutative_monad,     finite_commutative_monad,
             semigroup,             finite_semigroup,
             commutative_semigroup, finite_commutative_semigroup,
             monoid,                finite_monoid,
             commutative_monoid,    finite_commutative_monoid,
             cyclic_monoid,
             group,                 finite_group,
             abelian_group,         finite_abelian_group,
             symmetric_groups,
             group_test,

             cyclic_groups,          %% RWB experimental
             factor_groups,          %% RWB experimental
             A_group,                %% RWB experimental
             homomorphisms          %% RWB experimental
%            cayleys                 %% RWB experimental


   top_field:                    % Ring/Field-like Mathematical Structures with signatures:
                                 %     [T:Type+,+,*:[T,T->T],zero:T]  or   [T:Type+,+,*:[T,T->T],zero,one:T]

             ring,                      % semigroup[T,*]
             commutative_ring,          % commutative_semigroup[T,*]
             ring_nz_closed,            % semigroup[T,*], semigroup[nz_T,*]
             ring_with_one,             % monoid[T,*,one]
             commutative_ring_with_one, % commutative_monoid[T,*,one]
             integral_domain,           % commutative_semigroup[T,*]
                                        % commutative_semigroup[nz_T,*]
             division_ring,             % monoid[T,*,one], group[nz_T,*,one]
             field                      % commutative_monoid[T,*,one]
                                        % abelian_group[nz_T,*,one]
%            field_test