| products/sources/formale Sprachen/PVS/algebra/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: PVSOriginal von: PVS© |
|
|
cyclic_group[T:Type+,*:[T,T->T],one:T]: THEORY
BEGIN %------------------------------------------------------------------------ % The imported type T with * and one must be a group. % From this foundation other groups are created. These are just subgroups of the % underlying imported type. %------------------------------------------------------------------------ ASSUMING IMPORTING group_def[T,*,one] fullset_is_group: ASSUMPTION group?(fullset[T]) ENDASSUMING IMPORTING group[T,*,one] a: VAR T S: VAR set[T] H,G: VAR group i: VAR int % generated_by(a): group = {t: T | EXISTS (i: int): t = a^i} % cyclic?(G): boolean = EXISTS (a:(G)): G = generated_by(a) generated_by_lem : LEMMA generated_by(a)(a^i) generated_is_subgroup: LEMMA member(a,G) IMPLIES subgroup?(generated_by(a),G) generated_by_is_finite: LEMMA S = generated_by(a) AND (EXISTS (k: posnat): a^k = one) IMPLIES finite_group?(S) cyclic_abelian: THEOREM cyclic?(G) IMPLIES abelian_group?(G) %% TRICKY %% cyclic_subgroup: LEMMA subgroup?(H,G) AND cyclic?(G) IMPLIES cyclic?(H) is_cyclic : LEMMA (EXISTS (a:(G)): FORALL (x: (G)): EXISTS (n: nat): x = a^n) IMPLIES cyclic?(G) END cyclic_group ¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤ |
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchenDie farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
