Theorem: Finite-program soundness

Consider a finite acyclic instruction tree built from:

• allocation of specified pure ancillas;

• specified unitary operations;

• destructive Enter;

• classical control and classical discard;

• return of a fixed declared hybrid output type.

Every quantum name is either returned or explicitly consumed. The tree denotes a CPTP channel. After refining all histories, there are path maps $K_h$ satisfying

Its reported output block $y$ is the sum

The denotation retains every reference, and each evaluation branch terminates.

Proof. Pure allocation is an isometry. A specified unitary is trace preserving. Enter has complete measurement bras by ${\sum }_z{M}_z^{†}{M}_z=I$. Classical discard adds blocks, and classical control chooses a complete continuation on each block.

Compose the linear path maps from the root to every leaf. Backward induction on the tree, using completeness at each branch, proves (eq:path-completeness). Grouping leaf histories by their reported output proves (eq:path-channel). These are completely positive maps whose traces sum to the input trace. No normalized postselection is substituted for their sum.

The same path maps tensored with $I_Q$ prove the reference statement. A finite acyclic tree has finite maximum branch length, which proves termination.