MAYBE

Problem:
 app(nil(),xs) -> nil()
 app(cons(x,xs),ys) -> cons(x,app(xs,ys))
 rev(nil()) -> nil()
 rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))

Proof:
 DP Processor:
  DPs:
   app#(cons(x,xs),ys) -> app#(xs,ys)
   rev#(cons(x,xs)) -> rev#(cons(x,nil()))
  TRS:
   app(nil(),xs) -> nil()
   app(cons(x,xs),ys) -> cons(x,app(xs,ys))
   rev(nil()) -> nil()
   rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
  Open