TRS:
 {U11(tt(), M, N) -> U12(tt(), activate(M), activate(N)),
  U12(tt(), M, N) -> s(plus(activate(N), activate(M))),
     plus(N, 0()) -> N,
    plus(N, s(M)) -> U11(tt(), M, N),
      activate(X) -> X}
 Cdiprover:
  Interpretation class: pizerosimplemixed
  Complexity bound: POLYTIME COMPUTABLE
  0 = + 1
  plus(X9, X8) = + 0*X9^2 + 2*X8^2 + 3*X9 + 1 + 1*X8 + 0*X8*X9
  s(X7) = + 1*X7 + 4
  U11(X6, X5, X4) = + 3*X6^2 + 2*X5^2 + 0*X4^2 + 2*X5*X6 + 3*X5 + 3 + 2*X6 + 0*X4*X6 + 3*X4 + 0*X4*X5 + 0*X4*X5*X6
  activate(X3) = + 0*X3^2 + 1 + 1*X3
  tt = + 3
  U12(X2, X1, X0) = + 2*X2^2 + 2*X1^2 + 0*X0^2 + 1*X1*X2 + 2*X1 + 0 + 1*X2 + 0*X0*X2 + 3*X0 + 0*X0*X1 + 0*X0*X1*X2
  
  Qed