TRS:
 {     del(.(x, .(y, z))) -> f(=(x, y), x, y, z),
       f(true(), x, y, z) -> del(.(y, z)),
      f(false(), x, y, z) -> .(x, del(.(y, z))),
          =(nil(), nil()) -> true(),
        =(.(x, y), nil()) -> false(),
        =(nil(), .(y, z)) -> false(),
  =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v()))}
 Cdiprover:
  Interpretation class: pizerosimplemixed
  Complexity bound: POLYTIME COMPUTABLE
  v = + 1
  u = + 1
  and(X10, X9) = + 1*X9 + 1*X10 + 1
  nil = + 1
  false = + 4
  true = + 3
  .(X8, X7) = + 1*X7 + 1*X8 + 1
  del(X6) = + 1*X6^2 + 1 + 1*X6
  =(X5, X4) = + 0*X5^2 + 0*X4^2 + 1*X5 + 0 + 2*X4 + 2*X4*X5
  f(X3, X2, X1, X0) = + 0*X3^2 + 0*X2^2 + 1*X1^2 + 1*X0^2 + 0*X1*X2*X3 + 0*X1*X2 + 3*X1 + 0*X1*X3 + 1*X3 + 1 + 2*X2 + 0*X2*X3 + 0*X0*X2*X3 + 0*X0*X2 + 3*X0 + 0*X0*X3 + 0*X0*X1*X3 + 2*X0*X1 + 0*X0*X1*X2 + 0*X0*X1*X2*X3
  
  Qed