(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
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)
Q is empty.