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: Open