Specification int-mod

[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

enrich
   int-fac
with
   comment: we should also define the multiplicative modulo inverse: 
         z = x ^-1 mod n ⇔ z * x ≡ 1 mod n, i.e. ≡mod(z * x, 1, n).
         Exists, if gcd(x, n) = 1.
         Computed by the extended Euclidean algorithm (see ?/exercises/math-examples, RSA).
         modinverse is not unique. EEA computes a and b such that gcd(x, n) = a * x + b * n.
         a is the modinverse. a can be negative, but abs(a) < n. To obtain a positive
         modinverse add n to a if a < 0.
         ;

   
   
   functions  . |%| . : int × int → int prio 11 right;
             comment: i mod j, always > 0, otherwise like %.;
              . |/| . : int × int → int prio 11 right;
             comment: i / j with mod positive.;
   predicates  ≡mod : int × int × int;
              comment: i = j mod n, congruent modulo.;
   
   
   
   

   

   axioms mod-pos-def :  ⊦ 0 ≤ i % j → i |%| j = i % j;
          mod-neg-def :  ⊦ i % j < 0 → i |%| j = i % j + j;
          div-pos-def :  ⊦ 0 ≤ i % j → i |/| j = i / j;
          div-neg-def :  ⊦ i % j < 0 → i |/| j = i / j - 1;
          congmod-def :  ⊦ ≡mod(i, i0, j) ↔ j | abs(i - i0);

   

   
end enrich