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