TRS:
 {             is_empty(nil()) -> true(),
          is_empty(cons(x, l)) -> false(),
                hd(cons(x, l)) -> x,
                tl(cons(x, l)) -> l,
                append(l1, l2) -> ifappend(l1, l2, l1),
       ifappend(l1, l2, nil()) -> l2,
  ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2))}
 Cdiprover:
  Interpretation class: pizerosimplemixed
  Complexity bound: POLYTIME COMPUTABLE
  append(X9, X8) = + 1*X9^2 + 2*X8^2 + 3*X9 + 3 + 1*X8 + 0*X8*X9
  ifappend(X7, X6, X5) = + 0*X7^2 + 2*X6^2 + 1*X5^2 + 0*X6*X7 + 1*X6 + 0 + 2*X7 + 0*X5*X7 + 1*X5 + 0*X5*X6 + 0*X5*X6*X7
  tl(X4) = + 0*X4^2 + 1 + 2*X4
  hd(X3) = + 0*X3^2 + 0 + 2*X3
  cons(X2, X1) = + 1*X1 + 1*X2 + 2
  false = + 1
  nil = + 1
  is_empty(X0) = + 2*X0^2 + 0 + 1*X0
  true = + 2
  
  Qed