Quelle  chinese_remainder.pvs

chinese_remainder: THEORY

% The Chinese Remainder Theorem
% Author(s): Anthony Narkawicz
%
% Date: March 2012

BEGIN

IMPORTING ints@gcd,reals@product_nat

N: VAR posnat

m1,m2: VAR posnat

a1,a2: VAR nat


chinese_remainder_base : LEMMA
  rel_prime(m1,m2) IMPLIES
  EXISTS (k:below(m1*m2)): mod(a1,m1)=mod(k,m1) AND mod(a2,m2) = mod(k,m2)

mseq : VAR [nat->posnat]
aseq : VAR [nat->nat]

chinese_remainder : LEMMA
  (FORALL (i,j:below(N)): i/=j IMPLIES rel_prime(mseq(i),mseq(j)))
  IMPLIES
  (EXISTS (k:nat): FORALL (i:below(N)): mod(aseq(i),mseq(i)) = mod(k,mseq(i)))







END chinese_remainder