YES
Time: 6.720351
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}
 DP:
  DP:
   {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}
  UR:
   {                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))))),
                            a(w, t) -> w,
                            a(w, t) -> t}
   EDG:
    {(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))))))}
    STATUS:
     arrows: 0.500000
     SCCS (1):
      Scc:
       {admit#(x, .(u, .(v, .(w(), z)))) -> admit#(carry(x, u, v), z)}
      
      SCC (1):
       Strict:
        {admit#(x, .(u, .(v, .(w(), z)))) -> admit#(carry(x, u, v), z)}
       Weak:
       {                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}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [sum](x0, x1, x2) = 1,
         
         [carry](x0, x1, x2) = x0,
         
         [admit](x0, x1) = 0,
         
         [cond](x0, x1) = x0,
         
         [=](x0, x1) = x0,
         
         [.](x0, x1) = x0 + x1,
         
         [nil] = 0,
         
         [w] = 1,
         
         [true] = 0,
         
         [admit#](x0, x1) = x0 + x1
        Strict:
         admit#(x, .(u, .(v, .(w(), z)))) -> admit#(carry(x, u, v), z)
         1 + 1x + 1u + 1v + 1z >= 0 + 0x + 1u + 0v + 1z
        Weak:
         cond(true(), y) -> y
         0 + 1y >= 1y
         admit(x, .(u, .(v, .(w(), z)))) -> cond(=(sum(x, u, v), w()), .(u, .(v, .(w(), admit(carry(x, u, v), z)))))
         0 + 0x + 0u + 0v + 0z >= 1 + 0x + 1u + 1v + 0z
         admit(x, nil()) -> nil()
         0 + 0x >= 0
       Qed