MATH.17:4.3 - Establish the composition that the work needs

Try to construct:

Adm(B,C) x Adm(A,B) -> Adm(A,C), (g,f) -> g∘f.

The formula already defines a function composite. To obtain the displayed operation, establish that the composite satisfies the selected admissibility condition. Establish identity membership when doing nothing must be an allowable operation. Associativity then follows from function composition.

For example, fix a subset P of X and admit every f:X -> X with f(P) contained in P. If f and g are admitted and x lies in P, then f(x) lies in P and g(f(x)) lies in P. Thus their composite is admitted, as is the identity. These operations form a monoid: a set with associative composition and an identity. Several object types with identities and compatible associative composition form a category. These names make the established structure reusable.

If closure fails, use the failing input or pair to choose the repair. You might restrict the operations, enlarge the permitted result class, or keep a sequence of operations whose total admissibility is checked separately. For a cumulative resource bound, for example, retain the sequence and accumulated cost needed to assess the whole. Calling each step allowable leaves that total unresolved.

An interchange of steps is another claim. Establish g∘f=f∘g when a proposed reordering needs it; associativity by itself only changes the grouping of a fixed order.