| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/algebra/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle monoid_def.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Monoids definition file % % Author: Rick Butler, NASA Langley % David Lester, Manchester University & NIA % % 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 %------------------------------------------------------------------------------ monoid_def[T:Type+,*:[T,T->T],one:T]: THEORY BEGIN IMPORTING monad_def[T,*,one] S: VAR set[T] a: VAR T n,m: VAR nat power(a,n):RECURSIVE T = IF n=0 THEN one ELSE a*power(a,n-1) ENDIF MEASURE n generated_set(a):set[T] = {t: T | EXISTS n: t = power(a,n)} generated_set_lem : LEMMA generated_set(a)(power(a,n)) monoid?(S): bool = monad?(S) AND associative?[(S)](*) finite_monoid?(S): bool = monoid?(S) AND is_finite(S) commutative_monoid?(S): bool = monoid?(S) AND commutative?[(S)](*) finite_commutative_monoid?(S): bool = finite_monoid?(S) AND commutative?[(S)](*) infinite_order?(a):bool = (FORALL (n:posnat): power(a,n) /= one) finite_order?(a) :bool = NOT infinite_order?(a) END monoid_def ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28