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
  Usable Rule 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:
    f11(x,y) -> x
    f11(x,y) -> y
    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)))))
   ADG 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:
     f11(x,y) -> x
     f11(x,y) -> y
     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)))))
    graph:
     admit#(x,.(u,.(v,.(w(),z)))) -> 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) ->
     admit#(x,.(u,.(v,.(w(),z)))) ->
     cond#(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z)))))
    Restore Modifier:
     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
     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
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [admit#](x0, x1) = x1,
        
        [true] = 0,
        
        [cond](x0, x1) = x1,
        
        [carry](x0, x1, x2) = 0,
        
        [=](x0, x1) = 0,
        
        [sum](x0, x1, x2) = 0,
        
        [.](x0, x1) = x1 + 1,
        
        [w] = 0,
        
        [admit](x0, x1) = x0 + x1,
        
        [nil] = 0
       orientation:
        admit#(x,.(u,.(v,.(w(),z)))) = z + 3 >= z = admit#(carry(x,u,v),z)
        
        admit(x,nil()) = x >= 0 = nil()
        
        admit(x,.(u,.(v,.(w(),z)))) = x + z + 3 >= z + 3 = cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z)))))
        
        cond(true(),y) = y >= y = y
       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