MAYBE

Problem:
 rev(nil()) -> nil()
 rev(++(x,y)) -> ++(rev1(x,y),rev2(x,y))
 rev1(x,nil()) -> x
 rev1(x,++(y,z)) -> rev1(y,z)
 rev2(x,nil()) -> nil()
 rev2(x,++(y,z)) -> rev(++(x,rev(rev2(y,z))))

Proof:
 DP Processor:
  DPs:
   rev#(++(x,y)) -> rev2#(x,y)
   rev#(++(x,y)) -> rev1#(x,y)
   rev1#(x,++(y,z)) -> rev1#(y,z)
   rev2#(x,++(y,z)) -> rev2#(y,z)
   rev2#(x,++(y,z)) -> rev#(rev2(y,z))
   rev2#(x,++(y,z)) -> rev#(++(x,rev(rev2(y,z))))
  TRS:
   rev(nil()) -> nil()
   rev(++(x,y)) -> ++(rev1(x,y),rev2(x,y))
   rev1(x,nil()) -> x
   rev1(x,++(y,z)) -> rev1(y,z)
   rev2(x,nil()) -> nil()
   rev2(x,++(y,z)) -> rev(++(x,rev(rev2(y,z))))
  Open