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}
 DP:
  Strict:
   {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)))))}
  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}
  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))))))}
   SCCS:
    Scc:
     {admit#(x, .(u, .(v, .(w(), z)))) -> admit#(carry(x, u, v), z)}
    SCC:
     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}
     SPSC:
      Simple Projection:
       pi(admit#) = 1
      Strict:
       {}
      Qed