[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 nat-pot
enrich
   nat-div
with
   

   
   
   functions  . ^ . : nat × nat → nat prio 12 right;
              log : nat × nat → nat;
             comment: first arg basis, i.e. log(m, m ^ n) = n;
              2^ . : nat → nat;
              log2 . : nat → nat;
   
   
   
   
   

   

   axioms Pot-zero :  ⊦ n ^ 0 = 1;
          used for: s, ls;
          Pot-succ :  ⊦ n ^ m +1 = n ^ m * n;
          used for: ls;
          Logdef :  ⊦ m ^ n0 ≤ n ∧ n < m ^ n0 +1 → log(m, n) = n0;
          used for: nokodkodax;
          Pot2-zero :  ⊦ 2^ 0 = 1;
          used for: s, ls;
          Pot2-succ :  ⊦ 2^ n +1 = 2 * 2^ n;
          used for: ls;
          Log2def :  ⊦ 2^ m ≤ n ∧ n < 2^ m +1 → log2 n = m;
          used for: nokodkodax;

   

   
end enrich