Manuscript VIII-A@3 · VIII-A-v3.tex · theorem · 2398a747
Theorem: Constraint-blindness
Completeness and observation invariance › A2: factorization through accessible inputs · lines 938–962 · proof included or linked
VIII-A@3#A:thm:A2
Let two configurations have the same geometry, controller state, permissions, geometric resource reservation, source embedding, and all other declared accessible inputs. Suppose
Under A:ass:control, their evaluated input packets agree. They receive the same applicability decision, proposed update, output packet, and deterministically selected certificate. Either both are certified or both are rejected.
Proof. The input packet is determined by the common geometric data. Every argument of the deterministic specification agrees. Its guard, geometry, packet, support, transport, certificate, and successor controller outputs therefore agree. The evaluated acceptance conditions have the same truth value.
Displayed formulas in this passage
unlabeled · line 944