| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ints/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 kB |
|
Quelle tmod.pvs Sprache: PVS |
|||||||||
|
tmod: THEORY
%------------------------------------------------------------------------ % % mod function for number theory % % This has been defined using "tdiv" % % AUTHOR % ------ % % Ricky W. Butler email: r.w.butler@larc.nasa.gov % Mail Stop 130 fax: (804) 864-4234 % NASA Langley Research Center phone: (804) 864-6198 % Hampton, Virginia 23681-0001 % % %------------------------------------------------------------------------ BEGIN IMPORTING tdiv i,k,cc: VAR int m: VAR posnat n,a,b,c: VAR nat j: VAR nonzero_integer ml3: LEMMA abs(i - m * floor(i/m)) < m ml4: LEMMA abs(i + m * floor(-i/m)) < m mod(i,j): {k| abs(k) < abs(j)} = i-j*tdiv(i,j) mod_even: LEMMA integer?(i/j) IMPLIES mod(i,j) = 0 mod_neg: LEMMA mod(-i,j) = IF integer?(i/j) THEN 0 ELSE j - mod(i,j) ENDIF mod_neg_d: LEMMA mod(i,-j) = IF integer?(i/j) THEN 0 ELSE mod(i,j) - j ENDIF mod_eq_arg: LEMMA mod(j,j) = 0 mod_lt: LEMMA abs(i) < abs(j) IMPLIES mod(i,j) = IF sgn(i) = sgn(j) OR i = 0 THEN i ELSE i + j ENDIF mod_lt_nat: LEMMA n < m IMPLIES mod(n,m) = n mod_sum_pos: LEMMA mod(i+k*m,m) = mod(i,m) mod_sum: LEMMA mod(i+k*j,j) = mod(i,j) mod_it_is: LEMMA a = b + m*c AND b < m IMPLIES b = mod(a,m) mod_zero: LEMMA mod(0,j) = 0 mod_0 : LEMMA mod(0,j) = 0 mod_one: LEMMA mod(1,j) = IF abs(j) = 1 THEN 0 ELSIF j > 0 THEN 1 ELSE j + 1 ENDIF mod_of_mod: LEMMA mod(i + mod(k,m), m) = mod(i+k, m) mod_pos: LEMMA mod(i,m) >= 0 AND mod(i,m) < m JUDGEMENT mod(i,m) HAS_TYPE below(m) % ------- connection with prelude rem -------------- mod_to_rem: LEMMA mod(i,m) = rem(m)(i) mod_0_divides: LEMMA mod(i,j) = 0 IFF divides(j,i) AUTO_REWRITE+ mod_pos AUTO_REWRITE+ mod_0 AUTO_REWRITE+ mod_eq_arg AUTO_REWRITE+ mod_sum_pos AUTO_REWRITE+ mod_of_mod AUTO_REWRITE+ mod_sum END tmod ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28