|
%------------------------------------------------------------------------------
% Commutative groupoids
%
% 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
%------------------------------------------------------------------------------
commutative_groupoid[T:Type+,*:[T,T->T]]: THEORY
BEGIN
ASSUMING IMPORTING groupoid_def[T,*]
fullset_is_commutative_groupoid: ASSUMPTION
commutative_groupoid?(fullset[T])
ENDASSUMING
IMPORTING groupoid_def, groupoid[T,*]
commutative_groupoid: TYPE+ = (commutative_groupoid?) CONTAINING fullset[T]
G: VAR commutative_groupoid
x,y: VAR T
commutative: LEMMA x * y = y * x
commutative_groupoid_is_groupoid:
JUDGEMENT commutative_groupoid SUBTYPE_OF groupoid
END commutative_groupoid
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.18Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
