| 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 |
|
Quelle zn.pvs Sprache: 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 ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28