Quelle products_subgroups.pvs Sprache: PVS

%%-------------------** Product of Subgroups **-------------------
%%
%% Author          : André Luiz Galdino
%%                   Universidade Federal de Goiás - Brasil
%%
%% Last Modified On: November 28, 2011
%%
%%----------------------------------------------------------------

products_subgroups[T: TYPE, *: [T,T -> T], one: T]: THEORY

BEGIN

     ASSUMING IMPORTING algebra@group_def[T,*,one]

       fullset_is_group: ASSUMPTION group?(fullset[T])

   ENDASSUMING

   IMPORTING  algebra@normal_subgroups[T,*,one], groups_scaf

       G: VAR group[T,*,one]
   H,K,N: VAR set[T]

%%% Definitions %%%%%%

prod(H,K): set[T] = {t:T | EXISTS (h:(H), k:(K)): t = h*k}

HK_subgroup: LEMMA FORALL (H, N: subgroup(G)): normal_subgroup?(N,G)
                      IMPLIES subgroup?(prod(H,N),G)

HK_subgroup_permute: LEMMA FORALL (H, K: subgroup(G)):
                                 subgroup?(prod(H,K),G) IFF prod(H,K) = prod(K,H) ;

H_K_are_subgroups: LEMMA FORALL (H, K: subgroup(G)):
                   group?(prod(H,K)) IMPLIES
                        subgroup?(H, prod(H,K)) AND
                        subgroup?(K, prod(H,K))

END products_subgroups

quality94%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Bemerkung:

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Anfrage:

Dauer der Verarbeitung:

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.