Scheduled ancestry

The same argument applies to a finite acyclic port network. Give every operation all its actual input ports, including classical control and guard inputs. Pull an output observable backward through a reverse topological order. A disjoint operation sees identity and adds no support; an intersecting operation adds at most its declared predecessor ports. Thus

This is the timed-dependency shape of VII-J CheungVIIJ. It is proved here for the complete declared network, not imported as a premise.