(COMMENT
  O(n^2), works with POP* and polyomial interpretation:

  [0]()          = 1
  [add](x1, x2)  = 1 + 3*x1 + x2
  [s](x1)        = 1 + x1
  [mult](x1, x2) = 1 + 2*x1 + 2*x1^2

)

(VAR x y)

(DATATYPES
  Nat = µX.< 0, s(X) >
)

(SIGNATURES
  add :: Nat x Nat -> Nat
  mult :: Nat x Nat -> Nat
)

(RULES
  add(0,y) -> y
  add(s(x),y) -> s(add(x,y))
  mult(0,y) -> 0
  mult(s(x),y) -> add(x,mult(x,y))
)