[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,

Specification align
enrich
   nat-div

with
   

   
   
   functions  align↑ : nat × nat → nat;
              align↓ : nat × nat → nat;
   predicates  is-aligned : nat × nat;
   
   
   
   

   

   axioms alignup-def : 0 ≠ m ⊦ align↑(n, m) = (n % m = 0 ⊃ n;(n / m)+1 * m);
          used for: ls;
          aligndown-def : 0 ≠ m ⊦ align↓(n, m) = (n % m = 0 ⊃ n;n / m * m);
          used for: ls;
          is-aligned-def :  ⊦ is-aligned(n, m) ↔ n % m = 0;
          used for: ls;

   

   
end enrich