ch:rewriting-reflection: reflected monoid equality

Problem and invariant. Normalize commutative-monoid expressions while preserving evaluation at every environment. The finite map must contain no zero multiplicities.

Representation and construction. Use variables, zero, and binary addition for expressions and an ordered list of variable–multiplicity pairs for normal forms. Normalize recursively, merge maps by addition, evaluate both representations, and compare maps only after the evaluation check has succeeded on the named environments.

Observable result and mutation. Require equal, equal, not-equal, and the summary line shown in Appendix E. Mutate the product clause to discard its right summand. The source still checks, but both positive lines change to not-equal.

Acceptance and boundary. Run the four commands of Appendix E and match its accepted source record. Restore the accepted source after mutation. The program is not a proof-producing kernel extension and proves neither simplifier termination nor reflection soundness.