Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: vect2_fun_ops.pvs Sprache: PVS

Original von: PVS^©

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

BEGIN

   ASSUMING IMPORTING cyclic_monoid_def[T,*,one]

       fullset_is_cyclic_monoid: ASSUMPTION cyclic_monoid?(fullset[T])

   ENDASSUMING

   IMPORTING monoid[T,*,one]

   cyclic_monoid: TYPE+ = (cyclic_monoid?) CONTAINING fullset[T]

   M: VAR cyclic_monoid
   a: VAR T
   n: VAR nat

   cyclic_monoid_is: LEMMA cyclic_monoid?(M)

   cyclic_monoid_is_monoid: JUDGEMENT cyclic_monoid SUBTYPE_OF monoid

   cyclic_monoid_is_commutative_monoid:
                        JUDGEMENT cyclic_monoid SUBTYPE_OF commutative_monoid

END cyclic_monoid

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.