mod_lems: THEORY %------------------------------------------------------------------------ % Develops useful lemmas about mod % % % 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 mod i,j,k: VAR int m: VAR posnat n,a,b,c,x: VAR nat % The following rule characterizes the property that incrementing % modulo m wraps around the zero point. mod_wrap_around: LEMMA n < m & (c <= m & c >= m-n) => mod(n+c, m) = n - (m-c) mod_wrap2: LEMMA c < m IMPLIES mod(m+c, m) = c % Injection-like properties for mod for limited ranges mod_inj1: LEMMA x < m AND n < m AND c < m AND mod(x + n, m) = mod(x + c, m) IMPLIES n = c mod_inj2: LEMMA x < m AND n < m AND c < m AND mod(x - n, m) = mod(x - c, m) IMPLIES n = c mod_wrap_inj: LEMMA x < m AND a < m AND b < m AND a > 0 IMPLIES (mod(x + a, m) = mod(x - b, m)) = (a + b = m) kk, vv: VAR nat mod_neg_limited: LEMMA 0 <= kk AND kk < m AND vv < m AND vv - kk < 0 IMPLIES mod(vv - kk,m) = m + vv - kk END mod_lems