Theorem: Preservation and progress

Every deterministic or positive-probability Born transition preserves the type of a well-typed configuration. Every nonvalue well-typed configuration has an enabled transition.

Proof. Administrative preservation follows from substitution. Conditional selection retains the shared alternative resources by Lemma lem:branchwise. Allocation adds one name and one factor. A gate changes neither ownership nor type. Readout removes precisely its argument names and returns a bit tuple of the required type.

For progress, follow the call-by-value typing decomposition until a root operation is reached. Canonical forms supply the required value shape. Gate and readout arguments are tuples of distinct runtime names, or $\ast$ at arity zero. Finally,

provides at least one positive measurement branch.