# Term rewriting

Inspect every allowed reduction order in a finite family, and compare all reachable normal forms.

## Definitions

- **Rewrite rule**: A permitted local replacement; here 10 → 01.
- **Normal form**: A word containing no reducible 10 substring.
- **Confluence on a domain**: Every reduction path from each declared input can reach a common result.

## Acceptance procedure

1. Enumerate every binary word through the declared length.
2. Explore all possible one-step adjacent rewrites.
3. Collect terminal words, memoizing the reduction graph.
4. Require one normal form per input and replay the supplied concrete trace.

## Complexity

Each rewrite decreases the number of inverted 1-before-0 pairs. Exhaustive graph exploration is restricted to the stated length.

## Common failure

Two chosen reduction strategies agreeing does not establish that all strategies agree.

## Extensions

Publish a general inversion-measure termination argument and a separately checked confluence proof.

## Instances

- KL-FCS-034: All reduction orders through length 4 — Unique normal forms on the domain: yes
- KL-FCS-035: All reduction orders through length 6 — Unique normal forms on the domain: yes
- KL-FCS-036: All reduction orders through length 8 — Unique normal forms on the domain: yes

## References

- https://isa-afp.org/entries/Abstract-Rewriting.html