TRS:
 {a(b(x)) -> b(b(a(x)))}
 Cdiprover:
  Interpretation class: pizerosimplemixed
  Complexity bound: POLYTIME COMPUTABLE
  a(X1) = + 0*X1^2 + 0 + 3*X1
  b(X0) = + 1*X0 + 1
  
  Qed