| products/Sources/formale Sprachen/Coq/kernel/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: root.pvs Sprache: PVSUntersuchung PVS© |
|
||||||
|
zn[N: posnat]: THEORY
%------------------------------------------------------------------------ % Integer Groups % % Author: Rick Butler, NASA Langley Research Center % % Goal: show that Z_n is isomorphic to Z/nZ % % Version 1.0 12/14/07 %------------------------------------------------------------------------ BEGIN IMPORTING group, group_rew ++(a,b: below(N)): below(N) = mod(a+b,N) floor_help: LEMMA FORALL (x: below(N)): floor(x / N) = 0 AUTO_REWRITE+ floor_help Z_group: LEMMA group?[int, +, 0](fullset[int]); Z: group[int,+,0] = fullset[int] Z_prep: LEMMA group?[below(N), ++, 0](fullset[below(N)]); Z_: group[below(N),++,0] = fullset[below(N)] %% IMPORTING ints@primes %% zn_prime_field: LEMMA prime?(N) IMPLIES field?[below(N),++,0] = fullset[below(N)] nZ_TYPE: TYPE = {x: int | EXISTS (k: int): x = k*N} nZ_plus(x,y: nZ_TYPE): nZ_TYPE = x + y nZ_prep: LEMMA group?[nZ_TYPE, nZ_plus, 0](fullset[(nZ_TYPE)]); nZ: group[nZ_TYPE, +, 0] = fullset[nZ_TYPE] IMPORTING factor_groups nZ_normal: LEMMA normal_subgroup?(nZ,Z) %% THE FOLLOWING currently breaks PVS 4.1 with %% Break: set-type-for-application-parameters % Z_fact_test: LEMMA FORALL (G: factor_type(Z,nZ)): group?[factor_type(Z,nZ),mult(Z,nZ Z_fact_test: LEMMA group?[factor_type(Z,nZ),mult(Z,nZ),nZ](Z/nZ) END zn ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.0Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Entwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
