MMP.10:4.3 - Derive structural conditions and translate requirements
Ask what must hold for a variable assignment to describe one candidate of the intended kind. With Boolean entries r_ij describing the graph of a total function, require sum_j r_ij = 1 for every input i. For a partial function, replace this with sum_j r_ij <= 1; an all-zero row then means undefined at that input. For an injective function, additional conditions on columns express the extra requirement.
These conditions have different reasons. One value per input comes from choosing a total function. Injectivity comes from the particular problem, if it requires injectivity. Keep their reasons recoverable so that a later change from total to partial or from injective to unrestricted has a local repair.
Express the original requirements using the represented objects. Conjoin conditions that must hold for the same assignment. Use disjunction for allowed alternatives and implication when choosing an option imposes a condition. An implication alone supplies no timing; use time quantities or an explicit sequence when order matters. Preserve a coupled condition such as x+y=1 rather than replacing it by separate bounds on x and y.
When a bijection between representations is established, MATH.7 supplies transport of operations, relations and compound expressions. For a representation with several records per object, C.29.1 supplies the more general correspondence. Use the decoding of a record to express the requirement on its object. If a condition is rewritten to fit the receiving notation, derive that expression from the original relation and the structural conditions. This is where a missing index, an undefined value or a lost alternative can change the formulation.
Additional constraints can expose consequences and help the obtaining method. Derive them from the retained requirements, and preserve that dependence. Fewer variables or more constraints do not alone establish a faster method; compare the actual resulting work when efficiency matters.