Definition: Legal finite programme

A programme is a finite acyclic decision tree. Each node applies a declared operation to named live registers:

1. a unitary from a frozen finite library;

2. preparation of a fixed fresh ancilla, initially independent of the input, source, and validation reference;

3. a finite-outcome CP instrument whose outcome sum is TP;

4. explicit discard, classical update, or an allowed input arrival.

Every terminal branch returns a state on the same declared output space. An abort has an explicit replacement output. No operation acts on omitted source registers or the external validation reference. No primitive hides an undeclared quantum memory.