Manuscript En05-A@1 · En05-A.tex · proposition · f076e703
Proposition: Executability of admissible finite networks
Two retiming statements and a boost-closure limitation › The earlier strong closure hypothesis · lines 1557–1568 · proof included or linked
En05-A@1#prop:wf
Every finite semantically admissible block network satisfies E7(a). Every finite syntactically admissible network satisfies E7(b).
Proof. Dependencies increase the original tick, so the finite graph is acyclic. Topological orderings exist. Within a tick, disjoint complete channels commute, giving ordering-independent composition. The syntactic statement is Proposition prop:sound.
Nearby in this section
- section: The earlier strong closure hypothesis
- hypothesis: Hypothesis: Unrestricted device retiming closure
- assumption: Assumption: E7: Finite causal executability
- theorem: Theorem: Formal super-cone cycle construction
- section: The earlier strong closure hypothesis
- proposition: Proposition: Closed dependencies conflict with E7(a)
- theorem: Theorem: The strong closure also excludes ordinary relays
- remark: Remark: Correct conclusion