Transitivity of many-one reductions

For every three languages $A,B_0,C_0\subseteq B^*$, if $A\preceq B_0$ and $B_0\preceq C_0$, then $A\preceq C_0$. Thus existence of a polynomial-time membership-preserving map for each of the first two ordered pairs implies existence of such a map from $A$ to $C_0$; no complexity-class membership is assumed for any of the three languages. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. For languages $A,B_0\subseteq B^*$, write $A\preceq B_0$ to mean that there exists $f:B^*\to B^*$ satisfying $F(f)$ and $\forall w\in B^*,\ w\in A\ \Longleftrightarrow\ f(w)\in B_0$. Write $F(f)$ for existence of such a machine and a polynomial $p\in\mathbb N[X]$ that, for every $w\in B^*$, compute output list $f(w)$ from input list $w$ in at most $p(|w|)$ steps. Different existential computation witnesses may use different machines and polynomials. A machine in these assertions is a Mathlib TM2 stack machine with finitely many stack indices, instruction labels, and control states, a finite input-stack alphabet, designated input and output stacks, a program, and initial label and control state; its other stack alphabets need not be finite. Input and output alphabet bijections transport the specified encoded lists to the corresponding stack alphabets. Computation starts with only the input stack populated, and reaches a halted configuration with the specified output on the output stack, all other stacks empty, and the control state reset to its initial value. Time counts executions of whole TM2 statements, each of which may contain several stack operations. The supplied body is admitted with sorry; no proof of this assertion is supplied there.