YES

Problem:
 ++(nil(),y) -> y
 ++(x,nil()) -> x
 ++(.(x,y),z) -> .(x,++(y,z))
 ++(++(x,y),z) -> ++(x,++(y,z))

Proof:
 DP Processor:
  DPs:
   ++#(.(x,y),z) -> ++#(y,z)
   ++#(++(x,y),z) -> ++#(y,z)
   ++#(++(x,y),z) -> ++#(x,++(y,z))
  TRS:
   ++(nil(),y) -> y
   ++(x,nil()) -> x
   ++(.(x,y),z) -> .(x,++(y,z))
   ++(++(x,y),z) -> ++(x,++(y,z))
  CDG Processor:
   DPs:
    ++#(.(x,y),z) -> ++#(y,z)
    ++#(++(x,y),z) -> ++#(y,z)
    ++#(++(x,y),z) -> ++#(x,++(y,z))
   TRS:
    ++(nil(),y) -> y
    ++(x,nil()) -> x
    ++(.(x,y),z) -> .(x,++(y,z))
    ++(++(x,y),z) -> ++(x,++(y,z))
   graph:
    
   Qed