Quellcode-Bibliothek cyclic_monoid.pvs Sprache: 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

quality95%

¤ 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.0.5Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.