Proposition: Soundness of finite syntactic networks

Every finite syntactically admissible network denotes the same complete instrument as a well-typed composite program. Legal within-tick orderings of its disjoint block evaluations have the same denotation.

Proof. At a tick, compose the generating programs in parallel on their disjoint owned interfaces. Compose these tick programs sequentially, using finite classical control for the retained histories. Assumption ass:programinterface supplies the composite program and identifies its denotation with the block network.

Channels on disjoint interfaces commute, so legal within-tick orderings give the same channel. Evaluation of the composite program then supplies a valid finite execution in the selected calculus.