Proving operational termination of membership equational programs