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:
 Matrix Interpretation Processor: dim=1
  
  interpretation:
   [append](x0, x1) = x0 + x1,
   
   [rev](x0) = x0 + 2,
   
   [cons](x0, x1) = x0 + x1 + 5,
   
   [app](x0, x1) = 4x0 + x1 + 4,
   
   [nil] = 0
  orientation:
   app(nil(),xs) = xs + 4 >= 0 = nil()
   
   app(cons(x,xs),ys) = 4x + 4xs + ys + 24 >= x + 4xs + ys + 9 = cons(x,app(xs,ys))
   
   rev(nil()) = 2 >= 0 = nil()
   
   rev(cons(x,xs)) = x + xs + 7 >= x + xs + 7 = append(xs,rev(cons(x,nil())))
  problem:
   rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
  DP Processor:
   DPs:
    rev#(cons(x,xs)) -> rev#(cons(x,nil()))
   TRS:
    rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
   Open