TRS:
 {                admit(x, nil()) -> nil(),
  admit(x, .(u, .(v, .(w(), z)))) -> cond(=(sum(x, u, v), w()), .(u, .(v, .(w(), admit(carry(x, u, v), z))))),
                  cond(true(), y) -> y}
 Cdiprover:
  Interpretation class: pizerosimplemixed
  Complexity bound: POLYTIME COMPUTABLE
  true = + 1
  carry(X13, X12, X11) = + 1*X11 + 1*X12 + 1*X13 + 1
  .(X10, X9) = + 1*X9 + 1*X10 + 1
  w = + 1
  sum(X8, X7, X6) = + 1*X6 + 1*X7 + 1*X8 + 1
  =(X5, X4) = + 1*X4 + 1*X5 + 1
  cond(X3, X2) = + 0*X3^2 + 0*X2^2 + 3*X3 + 0 + 1*X2 + 0*X2*X3
  admit(X1, X0) = + 0*X1^2 + 2*X0^2 + 3*X1 + 0 + 1*X0 + 2*X0*X1
  nil = + 1
  
  Qed