# Check that an example is sensitive to the rule ## Intention I want to prove that the promised answer depends on the shown rule. A behavioural witness is separated from a mere hash change: the outcome must differ, not just the bytes. ## Incorrect form and why it stays silent A green answer without deleting the decisive form does not yet check the pitfall. ```text title="Incorrect form" // Только eligible(p), вопрос registered(p), ожидается TRUE_ONLY. // Правило Register забыли включить в программу. ``` ## Correct form A self-contained witness: ```law language "law.core" version "0.2"; package recipes.n.r13 version "0.1.0"; namespace "urn:recipe:n-package:13"; entity Person; relation eligible(p: Person); relation registered(p: Person); rule Register strict { for p: Person; when eligible(p); then registered(p); } ``` ## Frozen execution scene A local pair: | Facts | Question | Answer | |---|---|---| | eligible(p) and the Register rule | registered(p) | TRUE_ONLY | | Same facts, Register cut out | registered(p) | NEITHER | ## Counterfactual The sidecar cuts the full Register declaration through without. The same input becomes NEITHER; the outcome is checked, not a hash change. ## Boundary A surviving mutation does not prove equivalence, and a killed one does not prove completeness of the formalization. ## Pitfall Changing a label or a single hash does not count as behavioural detection of a mutant. Here the witness is the difference between Established and Not established, not refuted on one input.