In the precondition positive list, I am not sure whether b!=x is the best way to represent the condition. IsNot(b, x) can be used instead.