| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/ints/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle divides_lems.pvs Sprache: PVS |
|||||||||
|
divides_lems: THEORY
%---------------------------------------------------------------------------- % % Divisibility % % Author: Rick Butler % % NOTE. This theory joins the old divisibility theory with the prelude % definitions. If you hate the fact that the prelude definition of divides % using x as an integer, you can use divides_rew instead. % %---------------------------------------------------------------------------- BEGIN n,n1,n2: VAR nat m,m1,m2: VAR posnat i,j,k,ip,jp: VAR int nn,mm,ii,jj,kk: VAR nzint divides_rew: LEMMA divides(mm,i) = (EXISTS (k: int): i = mm*k) divides_lt: LEMMA i /= 0 IMPLIES divides(mm,i) IMPLIES mm <= abs(i) divides_lt_abs: LEMMA divides(mm,ii) IMPLIES abs(mm) <= abs(ii) divides_mod: LEMMA divides(m,i) = (mod(i,m) = 0) divides_sym: LEMMA divides(mm,ii) = divides(mm,-ii) divides_plus : LEMMA divides(mm,i) AND divides(mm,j) IMPLIES divides(mm,i+j) divides_plus_1: LEMMA mm > 1 IMPLIES divides(mm,ii) IMPLIES NOT divides(mm,ii+1) IMPORTING min_posnat lcm(m1,m2): int = min({k: posnat | divides(m1,k) AND divides(m2,k)}) IMPORTING max_bounded_posnat gcd_noem: LEMMA nonempty?({k: posnat | divides(k, i) AND divides(k, j)}) gcd_prep: LEMMA FORALL (i: int, j: {jj: int | i = 0 => jj /= 0}): EXISTS (UB: posnat): FORALL (y: ({k: posnat | divides(k, i) AND divides(k, j)})): y <= UB END divides_lems ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28