% Axioms for the natural numbers

set name nat

declare sort Nat
declare variables x, y, z: Nat
declare operators
  0, 1, 2      :          -> Nat
  s            : Nat      -> Nat
  __+__, __*__ : Nat, Nat -> Nat
  ..


% Ordering hints

register height * > + > 2 > 1 > s > 0		% for noeq-dsmpos ordering
register polynomial 0     2             2	% for polynomial 2 ordering
register polynomial 1     5             5
register polynomial 2     8             8
register polynomial +     x + y + 1     x*y
register polynomial s     x + 2         x + 2
register polynomial *     x*y           x*y


% Axioms

assert 
  ac +;
  ac *;
  sort Nat generated by 0, s;
  x + 0 = x;
  x + s(y) = s(x + y);
  x * 0 = 0;
  x * s(y) = (x * y) + x;
  x * (y + z) = (x * y) + (x * z);
  1 = s(0);
  2 = s(1);
  0 ~= s(x);
  s(x) = s(y) <=> x = y
  ..