| 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 |
|
Quellcode-Bibliothek abelian_group.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Abelian Groups % % 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 %------------------------------------------------------------------------------ abelian_group[T:Type+,*:[T,T->T],one:T]: THEORY BEGIN ASSUMING IMPORTING group_def[T,*,one] fullset_is_abelian_group: ASSUMPTION abelian_group?(fullset[T]) ENDASSUMING IMPORTING monoid_def, group_def, group[T,*,one] abelian_group: NONEMPTY_TYPE = (abelian_group?) CONTAINING fullset[T] A: VAR abelian_group S: VAR set[T] abelian_group_is_group: JUDGEMENT abelian_group SUBTYPE_OF group abelian_group_is_commutative_monoid: JUDGEMENT abelian_group SUBTYPE_OF commutative_monoid abelian_subgroups: LEMMA subgroup?(S,A) IMPLIES abelian_group?(S) finite_abelian_group: TYPE+ = (finite_abelian_group?) G: VAR finite_abelian_group finite_abelian_group_is_abelian_group: JUDGEMENT finite_abelian_group SUBTYPE_OF abelian_group finite_abelian_group_is_finite_group: JUDGEMENT finite_abelian_group SUBTYPE_OF finite_group finite_abelian_subgroups: LEMMA subgroup?(S,G) IMPLIES finite_abelian_group?(S) END abelian_group ¤ 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.2Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28