YES

Problem:
 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

Proof:
 DP Processor:
  DPs:
   admit#(x,.(u,.(v,.(w(),z)))) -> admit#(carry(x,u,v),z)
   admit#(x,.(u,.(v,.(w(),z)))) -> cond#(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z)))))
  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
  TDG Processor:
   DPs:
    admit#(x,.(u,.(v,.(w(),z)))) -> admit#(carry(x,u,v),z)
    admit#(x,.(u,.(v,.(w(),z)))) -> cond#(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z)))))
   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
   graph:
    admit#(x,.(u,.(v,.(w(),z)))) -> admit#(carry(x,u,v),z) ->
    admit#(x,.(u,.(v,.(w(),z)))) -> cond#(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z)))))
    admit#(x,.(u,.(v,.(w(),z)))) -> admit#(carry(x,u,v),z) ->
    admit#(x,.(u,.(v,.(w(),z)))) -> admit#(carry(x,u,v),z)
   SCC Processor:
    #sccs: 1
    #rules: 1
    #arcs: 2/4
    DPs:
     admit#(x,.(u,.(v,.(w(),z)))) -> admit#(carry(x,u,v),z)
    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
    KBO Processor:
     argument filtering:
      pi(nil) = []
      pi(admit) = 1
      pi(w) = []
      pi(.) = [1]
      pi(sum) = [0,2]
      pi(=) = []
      pi(carry) = 2
      pi(cond) = 1
      pi(true) = []
      pi(admit#) = 1
     weight function:
      w0 = 1
      w(admit#) = w(true) = w(cond) = w(=) = w(w) = w(nil) = 1
      w(carry) = w(sum) = w(.) = w(admit) = 0
     precedence:
      admit# ~ true ~ cond ~ carry ~ = ~ sum ~ . ~ w ~ admit ~ nil
     problem:
      DPs:
       
      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
     Qed