MATH.2:5.2 - A location class loses availability

Let V0 and V1 be states at location V, without and with permission. A partial transition r is defined at V1 and returns T; it is undefined at V0.

The proposed location-only relation identifies V0~V1. Output comparison alone would find no conflicting pair of returned values, because one value does not exist. The domain test detects the failure: V1∈D_r and V0∉D_r.

Refine the relation to retain permission. The two states are now in different classes, and the inherited transition is available only on the class containing V1. In MATH.1’s route case, this retains the permitted q;r of cost 6 and excludes the apparent p;r of cost 3.

A convention that declares a class enabled whenever any representative is enabled would answer a different question: a transition is possible from some member. To execute it from the actual state, that convention still needs a suitable member or an enabling step. The present construction preserves the availability of the given operation at the represented state.