8.1. QUERY Reduces to the Same Set🔗

kernel_query_eq_mops_query proves that, for a head-keyed query, the kernel's indexed candidate firing produces exactly the MOPS whole-space QUERY reduct set. The optimisation drops no reduct and invents none.

The proof follows from the indexing soundness and completeness results in the metatheory (candidates_sound, candidates_complete). The head bucket contains precisely the rules that could match, so scanning it loses nothing.

8.2. A Bisimulation🔗

Start at a single step, then lift to the whole reduction relation:

• The kernel's one-step rewriting (KernelStep) and the MOPS one-step rewriting (MopsStep) coincide (kernelStep_iff_mopsStep).

• The identity on atoms is therefore a bisimulation between them (kernel_mops_bisim).

• Their reflexive-transitive closures agree (reflTransGen_kernelStep_iff_mops).

The two semantics agree over single steps and over entire evaluation sequences.

8.3. Scope🔗

KernelStep is the kernel's indexed rule-firing core: the candidates matched against the redex. It corresponds to MOPS at the reduct-set level. It is not yet the full queryOp. Three things are abstracted out:

• rule-variable freshening;

• ambient-binding merge;

• cyclic-substitution pruning.

Rules added to the space at runtime (world.selfExtra, consulted by candidatesW) are also out of scope. The correspondence is stated over the static knowledge base. A lemma connecting queryOp to KernelStep up to α-equivalence is recorded as future work in the discussion chapter. The α-equivalence setoid already exists in the development.

What is proved here is that first-argument indexing leaves the reduct set unchanged: which rules fire and what they produce.