MAYBE

Problem:
 empty(nil()) -> true()
 empty(cons(x,l)) -> false()
 head(cons(x,l)) -> x
 tail(nil()) -> nil()
 tail(cons(x,l)) -> l
 rev(nil()) -> nil()
 rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
 last(x,l) -> if(empty(l),x,l)
 if(true(),x,l) -> x
 if(false(),x,l) -> last(head(l),tail(l))
 rev2(x,nil()) -> nil()
 rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))

Proof:
 DP Processor:
  DPs:
   rev#(cons(x,l)) -> rev2#(x,l)
   last#(x,l) -> empty#(l)
   last#(x,l) -> if#(empty(l),x,l)
   if#(false(),x,l) -> tail#(l)
   if#(false(),x,l) -> head#(l)
   if#(false(),x,l) -> last#(head(l),tail(l))
   rev2#(x,cons(y,l)) -> rev2#(y,l)
   rev2#(x,cons(y,l)) -> rev#(cons(x,rev2(y,l)))
  TRS:
   empty(nil()) -> true()
   empty(cons(x,l)) -> false()
   head(cons(x,l)) -> x
   tail(nil()) -> nil()
   tail(cons(x,l)) -> l
   rev(nil()) -> nil()
   rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
   last(x,l) -> if(empty(l),x,l)
   if(true(),x,l) -> x
   if(false(),x,l) -> last(head(l),tail(l))
   rev2(x,nil()) -> nil()
   rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))
  Open