giles 4a02a9c400 artdag: Phase 7 non-vacuous confluence gate regression + 2 tests ...

Assert mau/confluent? actually discriminates: the Peano-arithmetic variant of the
optimisation laws is flagged non-confluent with named non-joinable pairs, so the green
'opt module is confluent' is real evidence rather than a rubber stamp. maude-optimize
40/40, total 198/198.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

2026-06-19 13:58:39 +00:00

9.9 KiB

Raw Blame History

View Raw