NO 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()))) shuffle(nil()) -> nil() shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs))) Proof: Containment Processor: loop length: 1 terms: rev(cons(x,xs)) context: append(xs,[]) substitution: x -> x xs -> nil() Qed