Theorem: Finite adaptive composition

A finite sequence or finite adaptive tree of the declared instruments, finite allocations, allowed unitaries, and compatible report transports defines a complete instrument.

If $h$ ranges over its complete histories, there are path maps $K_h$ such that

These formulas hold with arbitrary untouched references. Every failure history is retained. Each new clock use requires a fresh or separately returned clock encoding; a consumed name is not reused as a quantum input.

Proof. Compose the isometries, gates, transport maps, and destructive measurement bras along each history. They give $K_h$.

Backward induction on the finite instruction tree proves completeness. A unitary or allocation is isometric. At a readout, summing the complete outcome family gives the identity; the same is true of every complete continuation by induction. Thus (eq:pathmaps) holds. Tensoring each path map with $I_E$ proves the reference statement. The declared input/output names enforce consumption.