| 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 |
|
SSL group_def.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Groups definition file % % Author: Rick Butler % 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 %------------------------------------------------------------------------------ group_def[T:Type+,*:[T,T->T],one:T]: THEORY BEGIN IMPORTING monoid_def[T,*,one] S: VAR set[T] inv_exists?(S): bool = FORALL (x:(S)): EXISTS (y:(S)): x*y = one AND y*x = one group?(S): bool = monoid?(S) AND inv_exists?(S) finite_group?(S): bool = group?(S) AND is_finite(S) abelian_group?(S): bool = group?(S) AND commutative?[(S)](*) finite_abelian_group?(S): bool = finite_group?(S) AND commutative?[(S)](*) subgroup?(S:set[T],G:(group?)): bool = subset?(S,G) AND group?(S) finite_group_surj: LEMMA group?(S) AND (EXISTS (N: nat), (f: [below[N] -> (S)]): surjective?(f)) IMPLIES finite_group?(S) END group_def ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28