YES

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

linear polynomial interpretations on N:

  admit_A(x1,x2) = x2 + 1
  admit#_A(x1,x2) = x2 + 1
  nil_A = 1
  nil#_A = 0
  ._A(x1,x2) = x1 + x2
  .#_A(x1,x2) = 1
  w_A = 1
  w#_A = 0
  cond_A(x1,x2) = x2
  cond#_A(x1,x2) = 0
  =_A(x1,x2) = x1
  =#_A(x1,x2) = x2
  sum_A(x1,x2,x3) = x1 + x2 + x3 + 1
  sum#_A(x1,x2,x3) = 0
  carry_A(x1,x2,x3) = x2 + x3 + 1
  carry#_A(x1,x2,x3) = 0
  true_A = 1
  true#_A = 0

precedence:

  admit = cond = = > nil = . = sum = carry = true > w