Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Delphi/Elbe 1.0/Sources/   (Columbo Version 0.7©)  Datei vom 4.1.2008 mit Größe 52 B image not shown  

Impressum groupoid.pvs   Sprache: unbekannt

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

groupoid[T:Type+,*:[T,T->T]]: THEORY

BEGIN

   IMPORTING groupoid_def[T,*]

   fullset_is_groupoid: LEMMA groupoid?(fullset[T])

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

   G: VAR groupoid

   closed         : LEMMA FORALL (x,y:(G)): member(x*y,G)

   star_closed    : LEMMA FORALL (x,y:(G)): G(x*y)

   groupoid_is_set: JUDGEMENT groupoid SUBTYPE_OF set[T]


END groupoid

98%


[ Seitenstruktur0.3Drucken  etwas mehr zur Ethik  ]