this precondition is here to check whether protection of constraints is compatible with termination of the refinement step