products/sources/formale Sprachen/Cobol/Test-Suite/SQL M/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: dml126.cob   Sprache: Unknown

%------------------------------------------------------------------------------
% Abelian Groups
%
%     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
%------------------------------------------------------------------------------

abelian_group[T:Type+,*:[T,T->T],one:T]: THEORY

BEGIN

   ASSUMING IMPORTING group_def[T,*,one]

       fullset_is_abelian_group: ASSUMPTION abelian_group?(fullset[T])

   ENDASSUMING

   IMPORTING monoid_def, group_def,
             group[T,*,one]

   abelian_group: NONEMPTY_TYPE = (abelian_group?) CONTAINING fullset[T]

   A:   VAR abelian_group
   S:   VAR set[T]

   abelian_group_is_group: JUDGEMENT abelian_group SUBTYPE_OF group

   abelian_group_is_commutative_monoid:
                          JUDGEMENT abelian_group SUBTYPE_OF commutative_monoid

   abelian_subgroups:     LEMMA subgroup?(S,A) IMPLIES abelian_group?(S)

   finite_abelian_group: TYPE+ = (finite_abelian_group?) 

   G: VAR finite_abelian_group
 
   finite_abelian_group_is_abelian_group:
       JUDGEMENT finite_abelian_group SUBTYPE_OF abelian_group

   finite_abelian_group_is_finite_group:
       JUDGEMENT finite_abelian_group SUBTYPE_OF finite_group

   finite_abelian_subgroups:
                    LEMMA subgroup?(S,G) IMPLIES finite_abelian_group?(S)



END abelian_group

[ Verzeichnis aufwärts0.53unsichere Verbindung  Übersetzung europäischer Sprachen durch Browser  ]