Theorem: Complete finite composition

Any finite adaptive tree of the specified instruments, allowed finite gates, allocations, and compatible transports has complete path maps $K_h$ satisfying

The identities hold with every untouched reference, and every failure history is included.

Each destructive use consumes its input names. A later quantum use requires a separately supplied factor, including a new clock when needed.

Proof. Compose the allocation isometries, unitaries, and destructive Kraus maps along each history. Backward induction on the finite tree proves completeness: each terminal identity is pulled back through a complete instrument or an isometry. Tensoring the path identities with the reference identity proves the complete statement. Input and output names enforce consumption.