TRS:
 {f(s(X), X) -> f(X, a(X)),
  f(X, c(X)) -> f(s(X), X),
     f(X, X) -> c(X)}
 Cdiprover:
  Interpretation class: pizerosimplemixed
  Complexity bound: POLYTIME COMPUTABLE
  c(X4) = + 1*X4 + 2
  s(X3) = + 1*X3 + 1
  a(X2) = + 1*X2 + 1
  f(X1, X0) = + 1*X1^2 + 1*X0^2 + 2*X1 + 3 + 1*X0 + 0*X0*X1
  
  Qed