MAYBE

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))
  SCC Processor:
   #sccs: 1
   #rules: 3
   #arcs: 9/9
   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))
   Open