| products/sources/formale Sprachen/PVS/algebra/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: A_group.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
A_group[T: TYPE]: THEORY
%----------------------------------------------------------------------------- % Experimental theory : % % In Chapter 2 Herstein introduces A(S) the group that consists of all % 1-1 mappings of a nonempty set onto itself. % % Author: Rick Butler % % the identity function is the identity element % * is function composition % inv is the inv function which exists because maps are 1-1 % %----------------------------------------------------------------------------- BEGIN AUTO_REWRITE+ member S: VAR (nonempty?[T]) %% nonempty set[T] maps(S: set[T]): TYPE = (bijective?[(S),(S)]) %% 1-1 maps A(S): set[maps(S)] = fullset[maps(S)] id(S): maps(S) = identity[(S)] op(S): [maps(S),maps(S) -> maps(S)] = function_props[(S),(S),(S)].o IMPORTING group_def A_is_group: LEMMA group?[maps(S),op(S),id(S)](fullset[maps(S)]) END A_group ¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
