Manuscript En05-A@1 · En05-A.tex · assumption · f076e703
Assumption: E7: Finite causal executability
Two retiming statements and a boost-closure limitation › The earlier strong closure hypothesis · lines 1545–1555
En05-A@1#ass:E7
Every admitted finite wired device network has a well-founded linearization consistent with its input–output dependencies. Composition along any legal linearization gives the same complete outcome law.
If the network is calculus generated and well typed under Assumption ass:programinterface, its linearization is realized by a finite composite program with that denotation.
Nearby in this section
- section: The earlier strong closure hypothesis
- hypothesis: Hypothesis: Unrestricted device retiming closure
- proposition: Proposition: Executability of admissible finite networks
- 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