functions
  0 : Nat
  S : Nat -> Nat
  mul : Nat * Nat -> Nat
  plus : Nat * Nat -> Nat
  axioms
  [1] plus(x,0) = x
  [2] plus(x,Sy) = S(plus(x,y))
  [3] mul(x,0) = 0
  [4] mul(x,Sy) = plus(mul(x,y),x)
  end