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