Lemma: Complete path maps for the displayed finite programs

For a finite program built from allocation, unitaries, destructive readout, and finite classical control, each complete history $h$ determines a linear path map $K_h$. For a pure input $\psi$,

If the reported output is $o$, its selective map is

These identities also hold with an untouched reference.

Proof. A complete history fixes the later classical controls. Compose allocation isometries, gate matrices, and destructive readout bras along that history. Conditional normalization factors cancel against the corresponding branch probabilities.

Completeness follows by backwards induction on the finite outcome tree. An allocation is isometric, a gate is unitary, and a readout satisfies

Grouping histories gives the selective maps. Tensor every path map with the identity on the reference.