| products/sources/formale sprachen/Coq/doc/changelog/04-tactics/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: sdl005.mco Sprache: PVSUntersuchung PVS© |
|
||||||
|
factor_groups[T:Type+,*:[T,T->T],one:T]: THEORY
%----------------------------------------------------------------------------- % Experimental theory working towards factor groups % % Author: Rick Butler % %----------------------------------------------------------------------------- BEGIN ASSUMING IMPORTING group_def[T,*,one] fullset_is_group: ASSUMPTION group?(fullset[T]) ENDASSUMING IMPORTING normal_subgroups[T,*,one] AUTO_REWRITE+ member H,G: VAR group[T,*,one] a,b,h: VAR T p0: LEMMA FORALL (G: group, H: normal_subgroup(G), A,B: left_cosets(G, H)): nonempty?[set[T]]({S: set[T] | EXISTS (a, b: (G)): A = a*H AND B = b*H AND S = (a * b)*H }) prep: LEMMA FORALL (a1,a2,b1,b2: (G)): FORALL (H: normal_subgroup(G)): a1*H = a2*H AND b1*H = b2*H IMPLIES (a1*b1)*H = (a2*b2)*H mult_prep: LEMMA FORALL (G: group, H: normal_subgroup(G), A,B: left_cosets(G, H)): singleton?[set[T]] ({S: set[T] | EXISTS (a, b: (G)): A = a*H AND B = b*H AND S = (a * b)*H }) AUTO_REWRITE+ left_coset mult(G:group,H:normal_subgroup(G))(A,B: left_cosets(G,H)): left_cosets(G,H) = lc_gen(G,H,A)*lc_gen(G,H,B)*H mult_lem : LEMMA FORALL (G: group, H: normal_subgroup(G), a,b: (G)): mult(G,H)(a*H,b*H) = (a*b)*H mult_in : LEMMA FORALL (G: group, H: normal_subgroup(G)),(A,B: left_cosets(G,H)): mult(G, H)(A,B)(a) IMPLIES G(a) mult_is_coset: LEMMA FORALL (G: group, H: normal_subgroup(G)),(A,B: left_cosets(G,H)): EXISTS (a: (G)): mult(G, H)(A,B) = a*H N_is_identity: LEMMA FORALL (G: group, N: normal_subgroup(G)), (A: left_cosets(G,N)): mult(G,N)(N,A) = A AND mult(G,N)(A,N) = A IMPORTING group left_cosets_group: THEOREM FORALL (G: group, N: normal_subgroup(G)): group?[left_cosets(G, N), mult(G, N), N](fullset[left_cosets(G, N)]) ; %% ----- define G/N as set of all left_cosets /(G: group[T,*,one], N: normal_subgroup(G)): group[left_cosets(G,N),mult(G,N),N] = fullset[left_cosets(G, N)] over(G: group[T,*,one], N: normal_subgroup(G)): group[left_cosets(G,N),mult(G,N),N] = fullset[left_cosets(G, N)] factor_type(G:group,N:normal_subgroup(G)): TYPE+ = left_cosets(G,N) END factor_groups ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.29Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
ZieleEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
