MAYBE

Problem:
 isEmpty(nil()) -> true()
 isEmpty(cons(x,xs)) -> false()
 last(cons(x,nil())) -> x
 last(cons(x,cons(y,ys))) -> last(cons(y,ys))
 dropLast(nil()) -> nil()
 dropLast(cons(x,nil())) -> nil()
 dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
 append(nil(),ys) -> ys
 append(cons(x,xs),ys) -> cons(x,append(xs,ys))
 reverse(xs) -> rev(xs,nil())
 rev(xs,ys) -> if(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
 if(true(),xs,ys,zs) -> zs
 if(false(),xs,ys,zs) -> rev(xs,ys)

Proof:
 DP Processor:
  DPs:
   last#(cons(x,cons(y,ys))) -> last#(cons(y,ys))
   dropLast#(cons(x,cons(y,ys))) -> dropLast#(cons(y,ys))
   append#(cons(x,xs),ys) -> append#(xs,ys)
   reverse#(xs) -> rev#(xs,nil())
   rev#(xs,ys) -> last#(xs)
   rev#(xs,ys) -> append#(ys,last(xs))
   rev#(xs,ys) -> dropLast#(xs)
   rev#(xs,ys) -> isEmpty#(xs)
   rev#(xs,ys) -> if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
   if#(false(),xs,ys,zs) -> rev#(xs,ys)
  TRS:
   isEmpty(nil()) -> true()
   isEmpty(cons(x,xs)) -> false()
   last(cons(x,nil())) -> x
   last(cons(x,cons(y,ys))) -> last(cons(y,ys))
   dropLast(nil()) -> nil()
   dropLast(cons(x,nil())) -> nil()
   dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
   append(nil(),ys) -> ys
   append(cons(x,xs),ys) -> cons(x,append(xs,ys))
   reverse(xs) -> rev(xs,nil())
   rev(xs,ys) -> if(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
   if(true(),xs,ys,zs) -> zs
   if(false(),xs,ys,zs) -> rev(xs,ys)
  Usable Rule Processor:
   DPs:
    last#(cons(x,cons(y,ys))) -> last#(cons(y,ys))
    dropLast#(cons(x,cons(y,ys))) -> dropLast#(cons(y,ys))
    append#(cons(x,xs),ys) -> append#(xs,ys)
    reverse#(xs) -> rev#(xs,nil())
    rev#(xs,ys) -> last#(xs)
    rev#(xs,ys) -> append#(ys,last(xs))
    rev#(xs,ys) -> dropLast#(xs)
    rev#(xs,ys) -> isEmpty#(xs)
    rev#(xs,ys) -> if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
    if#(false(),xs,ys,zs) -> rev#(xs,ys)
   TRS:
    last(cons(x,nil())) -> x
    last(cons(x,cons(y,ys))) -> last(cons(y,ys))
    append(nil(),ys) -> ys
    append(cons(x,xs),ys) -> cons(x,append(xs,ys))
    dropLast(nil()) -> nil()
    dropLast(cons(x,nil())) -> nil()
    dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
    isEmpty(nil()) -> true()
    isEmpty(cons(x,xs)) -> false()
   Open