diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf
index af3f75da..5655e386 100644
--- a/lib/maude/conformance.conf
+++ b/lib/maude/conformance.conf
@@ -9,9 +9,11 @@ PRELOADS=(
   lib/maude/term.sx
   lib/maude/parser.sx
   lib/maude/reduce.sx
+  lib/maude/matching.sx
 )
 
 SUITES=(
   "parse:lib/maude/tests/parse.sx:(mau-parse-tests-run!)"
   "reduce:lib/maude/tests/reduce.sx:(mau-reduce-tests-run!)"
+  "matching:lib/maude/tests/matching.sx:(mau-matching-tests-run!)"
 )
diff --git a/lib/maude/matching.sx b/lib/maude/matching.sx
new file mode 100644
index 00000000..e43239dd
--- /dev/null
+++ b/lib/maude/matching.sx
@@ -0,0 +1,565 @@
+;; lib/maude/matching.sx — equational matching modulo assoc/comm/id (Phase 3).
+;;
+;; The chisel. Syntactic matching (reduce.sx) returns at most one substitution;
+;; matching modulo a theory is MULTI-VALUED — `X + Y` against `a + b + c` (with
+;; _+_ assoc comm) has several solutions. `mau/mm` returns the full list of
+;; substitutions; callers (rule application) pick.
+;;
+;; Operator theories come from the signature attributes, collected into a dict
+;; OP-NAME -> {:assoc B :comm B :id ELT}. Matching dispatches on the head op's
+;; theory:
+;;   free        positional, exact arity
+;;   comm        binary, try both argument orderings
+;;   assoc       flatten the f-spine, match the pattern sequence against the
+;;               subject sequence (variables grab contiguous blocks)
+;;   assoc+comm  flatten, match as multisets (variables grab sub-multisets)
+;; Identity (id: e) lets a variable grab the empty block, contributing e.
+;;
+;; Equational rewriting (mau/ac-reduce) extends each f-AC equation l=r to
+;; f(REST..., l) -> f(REST..., r) so a rule fires on any sub-multiset of an
+;; AC term, then renormalises to a fixpoint. A candidate rewrite is taken only
+;; if it changes the AC-canonical form (mau/canon) — idempotency/identity
+;; matches that would re-fire forever are skipped, guaranteeing progress.
+
+;; ---------- theory table ----------
+
+(define
+  mau/build-theory
+  (fn
+    (m)
+    (let
+      ((th {}))
+      (for-each
+        (fn
+          (op)
+          (let
+            ((a (get op :attrs)))
+            (dict-set! th (get op :name) {:id (get a :id) :assoc (= (get a :assoc) true) :comm (= (get a :comm) true)})))
+        (mau/module-ops m))
+      th)))
+
+(define
+  mau/th-of
+  (fn
+    (theory op)
+    (let ((e (get theory op))) (if (= e nil) {:id nil :assoc false :comm false} e))))
+
+;; ---------- small list utilities ----------
+
+(define
+  mau/concat-map
+  (fn
+    (f xs)
+    (if
+      (empty? xs)
+      (list)
+      (mau/append2 (f (first xs)) (mau/concat-map f (rest xs))))))
+
+(define
+  mau/remove-at
+  (fn (xs i) (mau/append2 (mau/take xs i) (mau/drop xs (+ i 1)))))
+
+;; All (chosen complement) pairs over every subset of xs.
+(define
+  mau/all-splits
+  (fn
+    (xs)
+    (if
+      (empty? xs)
+      (list (list (list) (list)))
+      (let
+        ((subsplits (mau/all-splits (rest xs))) (x (first xs)))
+        (mau/concat-map
+          (fn
+            (pair)
+            (let
+              ((c (first pair)) (r (nth pair 1)))
+              (list (list (cons x c) r) (list c (cons x r)))))
+          subsplits)))))
+
+;; ---------- flattening of associative spines ----------
+
+(define
+  mau/flatten-op
+  (fn
+    (theory f term)
+    (if
+      (and (mau/app? term) (= (mau/op term) f))
+      (mau/flatten-op-list theory f (mau/args term))
+      (list term))))
+
+(define
+  mau/flatten-op-list
+  (fn
+    (theory f args)
+    (if
+      (empty? args)
+      (list)
+      (mau/append2
+        (mau/flatten-op theory f (first args))
+        (mau/flatten-op-list theory f (rest args))))))
+
+(define
+  mau/foldr-app
+  (fn
+    (f block)
+    (if
+      (empty? (rest block))
+      (first block)
+      (mau/app f (list (first block) (mau/foldr-app f (rest block)))))))
+
+(define
+  mau/rebuild
+  (fn
+    (f block id)
+    (cond
+      ((empty? block) (if (= id nil) (mau/const "$EMPTY") (mau/const id)))
+      ((empty? (rest block)) (first block))
+      (else (mau/foldr-app f block)))))
+
+(define mau/ac-build (fn (theory f els id) (mau/rebuild f els id)))
+
+;; ---------- AC-canonical form / equality ----------
+
+(define
+  mau/insert-str
+  (fn
+    (x ys)
+    (cond
+      ((empty? ys) (list x))
+      ((<= x (first ys)) (cons x ys))
+      (else (cons (first ys) (mau/insert-str x (rest ys)))))))
+
+(define
+  mau/sort-strings
+  (fn
+    (xs)
+    (if
+      (empty? xs)
+      xs
+      (mau/insert-str (first xs) (mau/sort-strings (rest xs))))))
+
+(define
+  mau/drop-identity
+  (fn
+    (theory f els id)
+    (if
+      (= id nil)
+      els
+      (let
+        ((idc (mau/canon theory (mau/const id))))
+        (filter (fn (e) (not (= (mau/canon theory e) idc))) els)))))
+
+(define
+  mau/canon
+  (fn
+    (theory term)
+    (cond
+      ((mau/var? term) (str "?" (mau/vname term)))
+      ((mau/const? term) (mau/op term))
+      ((mau/app? term)
+        (let
+          ((f (mau/op term)) (th (mau/th-of theory (mau/op term))))
+          (if
+            (get th :assoc)
+            (let
+              ((els (mau/drop-identity theory f (mau/flatten-op theory f term) (get th :id))))
+              (cond
+                ((empty? els)
+                  (if (= (get th :id) nil) "$EMPTY" (get th :id)))
+                ((empty? (rest els)) (mau/canon theory (first els)))
+                (else
+                  (let
+                    ((cs (map (fn (e) (mau/canon theory e)) els)))
+                    (let
+                      ((cs2 (if (get th :comm) (mau/sort-strings cs) cs)))
+                      (str f "(" (join "," cs2) ")"))))))
+            (if
+              (get th :comm)
+              (str
+                f
+                "("
+                (join
+                  ","
+                  (mau/sort-strings
+                    (map (fn (e) (mau/canon theory e)) (mau/args term))))
+                ")")
+              (str
+                f
+                "("
+                (join
+                  ","
+                  (map (fn (e) (mau/canon theory e)) (mau/args term)))
+                ")")))))
+      (else (str term)))))
+
+(define
+  mau/ac-equal?
+  (fn (theory a b) (= (mau/canon theory a) (mau/canon theory b))))
+
+;; ---------- variable block bounds ----------
+
+(define
+  mau/rest-var?
+  (fn
+    (name)
+    (and
+      (> (len name) 0)
+      (= (slice name 0 1) "$"))))
+
+(define
+  mau/var-kmin
+  (fn
+    (name id)
+    (if (or (mau/rest-var? name) (not (= id nil))) 0 1)))
+
+(define
+  mau/bind-check
+  (fn
+    (theory s name val)
+    (let
+      ((b (get s name)))
+      (if
+        (= b nil)
+        (assoc s name val)
+        (if (mau/ac-equal? theory b val) s nil)))))
+
+;; ---------- core multi-valued matcher ----------
+
+(define
+  mau/mm
+  (fn
+    (theory pat subj s)
+    (cond
+      ((mau/var? pat)
+        (let
+          ((bound (get s (mau/vname pat))))
+          (if
+            (= bound nil)
+            (list (assoc s (mau/vname pat) subj))
+            (if (mau/ac-equal? theory bound subj) (list s) (list)))))
+      ((mau/app? pat)
+        (if (mau/app? subj) (mau/mm-app theory pat subj s) (list)))
+      (else (list)))))
+
+(define
+  mau/extend-all
+  (fn
+    (theory p subj substs)
+    (mau/concat-map (fn (s) (mau/mm theory p subj s)) substs)))
+
+(define
+  mau/mm-args
+  (fn
+    (theory ps ss substs)
+    (cond
+      ((and (empty? ps) (empty? ss)) substs)
+      ((or (empty? ps) (empty? ss)) (list))
+      (else
+        (mau/mm-args
+          theory
+          (rest ps)
+          (rest ss)
+          (mau/extend-all theory (first ps) (first ss) substs))))))
+
+(define
+  mau/mm-comm
+  (fn
+    (theory pat subj s)
+    (let
+      ((p1 (nth (mau/args pat) 0))
+        (p2 (nth (mau/args pat) 1))
+        (q1 (nth (mau/args subj) 0))
+        (q2 (nth (mau/args subj) 1)))
+      (mau/append2
+        (mau/mm-args theory (list p1 p2) (list q1 q2) (list s))
+        (mau/mm-args theory (list p1 p2) (list q2 q1) (list s))))))
+
+(define
+  mau/mm-assoc
+  (fn
+    (theory f pat subj s)
+    (let
+      ((pels (mau/flatten-op theory f pat))
+        (sels (mau/flatten-op theory f subj))
+        (th (mau/th-of theory f)))
+      (if
+        (get th :comm)
+        (mau/match-multiset theory f pels sels s (get th :id))
+        (mau/match-sequence theory f pels sels s (get th :id))))))
+
+(define
+  mau/mm-app
+  (fn
+    (theory pat subj s)
+    (let
+      ((f (mau/op pat))
+        (g (mau/op subj))
+        (th (mau/th-of theory (mau/op pat))))
+      (cond
+        ((get th :assoc) (mau/mm-assoc theory f pat subj s))
+        ((get th :comm)
+          (if
+            (and
+              (= f g)
+              (= (mau/arity pat) 2)
+              (= (mau/arity subj) 2))
+            (mau/mm-comm theory pat subj s)
+            (list)))
+        (else
+          (if
+            (and (= f g) (= (mau/arity pat) (mau/arity subj)))
+            (mau/mm-args theory (mau/args pat) (mau/args subj) (list s))
+            (list)))))))
+
+;; ---------- associative (ordered) sequence matching ----------
+
+(define
+  mau/match-sequence
+  (fn
+    (theory f pels sels s id)
+    (cond
+      ((empty? pels) (if (empty? sels) (list s) (list)))
+      (else
+        (let
+          ((p (first pels)) (prest (rest pels)))
+          (if
+            (mau/var? p)
+            (mau/seq-var-loop
+              theory
+              f
+              prest
+              sels
+              s
+              (mau/vname p)
+              id
+              (mau/var-kmin (mau/vname p) id))
+            (if
+              (empty? sels)
+              (list)
+              (mau/concat-map
+                (fn
+                  (s2)
+                  (mau/match-sequence theory f prest (rest sels) s2 id))
+                (mau/mm theory p (first sels) s)))))))))
+
+(define
+  mau/seq-var-loop
+  (fn
+    (theory f prest sels s name id k)
+    (if
+      (> k (len sels))
+      (list)
+      (let
+        ((block (mau/take sels k)) (rests (mau/drop sels k)))
+        (let
+          ((val (mau/rebuild f block id)))
+          (let
+            ((s2 (mau/bind-check theory s name val)))
+            (mau/append2
+              (if
+                (= s2 nil)
+                (list)
+                (mau/match-sequence theory f prest rests s2 id))
+              (mau/seq-var-loop
+                theory
+                f
+                prest
+                sels
+                s
+                name
+                id
+                (+ k 1)))))))))
+
+;; ---------- associative-commutative (multiset) matching ----------
+
+(define
+  mau/match-multiset
+  (fn
+    (theory f pels sels s id)
+    (cond
+      ((empty? pels) (if (empty? sels) (list s) (list)))
+      (else
+        (let
+          ((p (first pels)) (prest (rest pels)))
+          (if
+            (mau/var? p)
+            (mau/ms-var-splits theory f prest sels s (mau/vname p) id)
+            (mau/ms-nonvar-loop theory f p prest sels s id 0)))))))
+
+(define
+  mau/ms-nonvar-loop
+  (fn
+    (theory f p prest sels s id i)
+    (if
+      (>= i (len sels))
+      (list)
+      (let
+        ((elem (nth sels i)) (others (mau/remove-at sels i)))
+        (mau/append2
+          (mau/concat-map
+            (fn (s2) (mau/match-multiset theory f prest others s2 id))
+            (mau/mm theory p elem s))
+          (mau/ms-nonvar-loop theory f p prest sels s id (+ i 1)))))))
+
+(define
+  mau/ms-var-splits
+  (fn
+    (theory f prest sels s name id)
+    (let
+      ((kmin (mau/var-kmin name id)))
+      (mau/concat-map
+        (fn
+          (pair)
+          (let
+            ((chosen (first pair)) (rests (nth pair 1)))
+            (if
+              (< (len chosen) kmin)
+              (list)
+              (let
+                ((val (mau/rebuild f chosen id)))
+                (let
+                  ((s2 (mau/bind-check theory s name val)))
+                  (if
+                    (= s2 nil)
+                    (list)
+                    (mau/match-multiset theory f prest rests s2 id)))))))
+        (mau/all-splits sels)))))
+
+;; ---------- public matching entry ----------
+
+(define
+  mau/match-all
+  (fn (m pat subj) (mau/mm (mau/build-theory m) pat subj {})))
+
+;; ---------- AC-aware equational rewriting ----------
+
+(define
+  mau/restv
+  (fn
+    (theory f s name)
+    (let
+      ((v (get s name)))
+      (cond
+        ((= v nil) (list))
+        ((and (mau/app? v) (= (mau/op v) "$EMPTY")) (list))
+        (else (mau/flatten-op theory f v))))))
+
+(define
+  mau/ac-eq-result
+  (fn
+    (theory f th eq s)
+    (if
+      (get th :comm)
+      (mau/ac-build
+        theory
+        f
+        (mau/append2
+          (mau/flatten-op theory f (mau/subst-apply s (get eq :rhs)))
+          (mau/restv theory f s "$R"))
+        (get th :id))
+      (mau/ac-build
+        theory
+        f
+        (mau/append2
+          (mau/restv theory f s "$L")
+          (mau/append2
+            (mau/flatten-op theory f (mau/subst-apply s (get eq :rhs)))
+            (mau/restv theory f s "$R")))
+        (get th :id)))))
+
+;; Walk the candidate matches and return the first rewrite that actually
+;; changes the term's canonical form (skips idempotency/identity no-ops).
+(define
+  mau/first-change
+  (fn
+    (theory f th eq term matches)
+    (if
+      (empty? matches)
+      nil
+      (let
+        ((result (mau/ac-eq-result theory f th eq (first matches))))
+        (if
+          (mau/ac-equal? theory result term)
+          (mau/first-change theory f th eq term (rest matches))
+          result)))))
+
+(define
+  mau/ac-rewrite-eq
+  (fn
+    (theory f th eq term)
+    (let
+      ((id (get th :id))
+        (pels (mau/flatten-op theory f (get eq :lhs)))
+        (sels (mau/flatten-op theory f term)))
+      (let
+        ((matches (if (get th :comm) (mau/match-multiset theory f (mau/append2 pels (list (mau/var "$R" ""))) sels {} id) (mau/match-sequence theory f (mau/append2 (list (mau/var "$L" "")) (mau/append2 pels (list (mau/var "$R" "")))) sels {} id))))
+        (mau/first-change theory f th eq term matches)))))
+
+(define
+  mau/ac-rewrite-top
+  (fn
+    (theory eqs term)
+    (cond
+      ((empty? eqs) nil)
+      (else
+        (let
+          ((eq (first eqs)))
+          (if
+            (= (get eq :cond) nil)
+            (let
+              ((lhs (get eq :lhs)))
+              (let
+                ((th (if (mau/app? lhs) (mau/th-of theory (mau/op lhs)) {:id nil :assoc false :comm false})))
+                (let
+                  ((r (if (and (mau/app? lhs) (get th :assoc)) (mau/ac-rewrite-eq theory (mau/op lhs) th eq term) (let ((ss (mau/mm theory lhs term {}))) (if (empty? ss) nil (mau/subst-apply (first ss) (get eq :rhs)))))))
+                  (cond
+                    ((= r nil) (mau/ac-rewrite-top theory (rest eqs) term))
+                    ((mau/ac-equal? theory r term)
+                      (mau/ac-rewrite-top theory (rest eqs) term))
+                    (else r)))))
+            (mau/ac-rewrite-top theory (rest eqs) term)))))))
+
+(define
+  mau/ac-normalize
+  (fn
+    (theory eqs term fuel)
+    (if
+      (<= fuel 0)
+      term
+      (cond
+        ((mau/var? term) term)
+        ((mau/app? term)
+          (let
+            ((nargs (map (fn (a) (mau/ac-normalize theory eqs a fuel)) (mau/args term))))
+            (let
+              ((t2 (mau/app (mau/op term) nargs)))
+              (let
+                ((r (mau/ac-rewrite-top theory eqs t2)))
+                (if
+                  (= r nil)
+                  t2
+                  (mau/ac-normalize theory eqs r (- fuel 1)))))))
+        (else term)))))
+
+(define
+  mau/ac-reduce
+  (fn
+    (m term)
+    (mau/ac-normalize
+      (mau/build-theory m)
+      (mau/module-eqs m)
+      term
+      mau/reduce-fuel)))
+
+(define
+  mau/ac-reduce-term
+  (fn (m src) (mau/ac-reduce m (mau/parse-term-in m src))))
+
+(define
+  mau/ac-reduce->str
+  (fn (m src) (mau/term->str (mau/ac-reduce-term m src))))
+
+(define
+  mau/ac-canon
+  (fn (m src) (mau/canon (mau/build-theory m) (mau/ac-reduce-term m src))))
diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json
index e9ea5da0..2eec89ae 100644
--- a/lib/maude/scoreboard.json
+++ b/lib/maude/scoreboard.json
@@ -1,11 +1,12 @@
 {
   "lang": "maude",
-  "total_passed": 91,
+  "total_passed": 119,
   "total_failed": 0,
-  "total": 91,
+  "total": 119,
   "suites": [
     {"name":"parse","passed":65,"failed":0,"total":65},
-    {"name":"reduce","passed":26,"failed":0,"total":26}
+    {"name":"reduce","passed":26,"failed":0,"total":26},
+    {"name":"matching","passed":28,"failed":0,"total":28}
   ],
-  "generated": "2026-06-07T14:45:37+00:00"
+  "generated": "2026-06-07T15:00:34+00:00"
 }
diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md
index 3d9e113e..690c1cab 100644
--- a/lib/maude/scoreboard.md
+++ b/lib/maude/scoreboard.md
@@ -1,8 +1,9 @@
 # maude scoreboard
 
-**91 / 91 passing** (0 failure(s)).
+**119 / 119 passing** (0 failure(s)).
 
 | Suite | Passed | Total | Status |
 |-------|--------|-------|--------|
 | parse | 65 | 65 | ok |
 | reduce | 26 | 26 | ok |
+| matching | 28 | 28 | ok |
diff --git a/lib/maude/tests/matching.sx b/lib/maude/tests/matching.sx
new file mode 100644
index 00000000..745f8b61
--- /dev/null
+++ b/lib/maude/tests/matching.sx
@@ -0,0 +1,170 @@
+;; lib/maude/tests/matching.sx — Phase 3: matching modulo assoc/comm/id.
+
+(define mmt-pass 0)
+(define mmt-fail 0)
+(define mmt-failures (list))
+
+(define
+  mmt-check!
+  (fn
+    (name got expected)
+    (if
+      (= got expected)
+      (set! mmt-pass (+ mmt-pass 1))
+      (do
+        (set! mmt-fail (+ mmt-fail 1))
+        (append!
+          mmt-failures
+          (str name "  expected: " expected "  got: " got))))))
+
+;; ---- multi-valued matching enumeration ----
+
+(define
+  mmt-acg
+  (mau/parse-module
+    "fmod ACG is\n  sort S .\n  op a : -> S .\n  op b : -> S .\n  op c : -> S .\n  op _+_ : S S -> S [assoc comm] .\n  op _._ : S S -> S [assoc] .\n  vars X Y : S .\nendfm"))
+
+;; X + Y against a + b + c (AC, no id): 6 solutions (each non-empty 2-split).
+(mmt-check!
+  "ac-match-count"
+  (len
+    (mau/match-all
+      mmt-acg
+      (mau/parse-term-in mmt-acg "X + Y")
+      (mau/parse-term-in mmt-acg "a + b + c")))
+  6)
+;; X + a against a + b + c: X must be b + c (one solution, multiset).
+(mmt-check!
+  "ac-match-partial"
+  (len
+    (mau/match-all
+      mmt-acg
+      (mau/parse-term-in mmt-acg "X + a")
+      (mau/parse-term-in mmt-acg "a + b + c")))
+  1)
+;; assoc-only X . Y against a . b . c: ordered 2-splits -> 2 solutions.
+(mmt-check!
+  "assoc-match-count"
+  (len
+    (mau/match-all
+      mmt-acg
+      (mau/parse-term-in mmt-acg "X . Y")
+      (mau/parse-term-in mmt-acg "a . b . c")))
+  2)
+;; no match: a + a pattern against a + b
+(mmt-check!
+  "ac-no-match"
+  (len
+    (mau/match-all
+      mmt-acg
+      (mau/parse-term-in mmt-acg "a + a")
+      (mau/parse-term-in mmt-acg "a + b")))
+  0)
+
+;; ---- comm (non-assoc) matching ----
+
+(define
+  mmt-pair
+  (mau/parse-module
+    "fmod PAIR is\n  sort S .\n  op a : -> S .\n  op b : -> S .\n  op p : S S -> S [comm] .\n  op fst : S -> S .\n  vars X Y : S .\n  eq fst(p(X, a)) = X .\nendfm"))
+
+(mmt-check!
+  "comm-both-orders"
+  (mau/ac-reduce->str mmt-pair "fst(p(b, a))")
+  "b")
+(mmt-check! "comm-swapped" (mau/ac-reduce->str mmt-pair "fst(p(a, b))") "b")
+
+;; ---- identity ----
+
+(define
+  mmt-id
+  (mau/parse-module
+    "fmod IDMOD is\n  sort S .\n  op a : -> S .\n  op b : -> S .\n  op e : -> S .\n  op _*_ : S S -> S [assoc comm id: e] .\n  vars X Y : S .\nendfm"))
+
+(mmt-check! "id-drop" (mau/ac-canon mmt-id "a * e") "a")
+(mmt-check! "id-drop-mid" (mau/ac-canon mmt-id "a * e * b") "_*_(a,b)")
+(mmt-check! "id-only" (mau/ac-canon mmt-id "e * e") "e")
+;; with id, X * Y matching a (singleton) succeeds (one var empty)
+(mmt-check!
+  "id-match-singleton"
+  (>
+    (len
+      (mau/match-all
+        mmt-id
+        (mau/parse-term-in mmt-id "X * Y")
+        (mau/parse-term-in mmt-id "a")))
+    0)
+  true)
+
+;; ---- multiset / bag rewriting ----
+
+(define
+  mmt-bag
+  (mau/parse-module
+    "fmod BAG is\n  sort S .\n  op a : -> S .\n  op b : -> S .\n  op c : -> S .\n  op _+_ : S S -> S [assoc comm] .\n  eq a + a = a .\nendfm"))
+
+(mmt-check! "bag-collapse" (mau/ac-canon mmt-bag "a + b + a") "_+_(a,b)")
+(mmt-check! "bag-deep" (mau/ac-canon mmt-bag "a + a + a") "a")
+(mmt-check! "bag-reorder" (mau/ac-canon mmt-bag "c + a + b + a") "_+_(a,b,c)")
+(mmt-check!
+  "bag-flatten-assoc"
+  (mau/ac-canon mmt-bag "(a + b) + (a + c)")
+  "_+_(a,b,c)")
+
+;; ---- set theory: idempotent union with empty (identity) ----
+
+(define
+  mmt-set
+  (mau/parse-module
+    "fmod SET is\n  sort Set .\n  op empty : -> Set .\n  op a : -> Set .\n  op b : -> Set .\n  op c : -> Set .\n  op _U_ : Set Set -> Set [assoc comm id: empty] .\n  var X : Set .\n  eq X U X = X .\nendfm"))
+
+(mmt-check! "set-dedup" (mau/ac-canon mmt-set "a U b U a") "_U_(a,b)")
+(mmt-check! "set-triple" (mau/ac-canon mmt-set "a U a U a") "a")
+(mmt-check!
+  "set-union"
+  (mau/ac-canon mmt-set "a U b U c U a U b")
+  "_U_(a,b,c)")
+(mmt-check! "set-empty" (mau/ac-canon mmt-set "a U empty") "a")
+(mmt-check! "set-empty-only" (mau/ac-canon mmt-set "empty U empty") "empty")
+
+;; ---- group equations (assoc, non-comm, identity + inverse) ----
+
+(define
+  mmt-group
+  (mau/parse-module
+    "fmod GROUP is\n  sort G .\n  op e : -> G .\n  op a : -> G .\n  op b : -> G .\n  op _*_ : G G -> G [assoc] .\n  op i : G -> G .\n  var X : G .\n  eq e * X = X .\n  eq X * e = X .\n  eq i(X) * X = e .\n  eq X * i(X) = e .\n  eq i(e) = e .\n  eq i(i(X)) = X .\nendfm"))
+
+(mmt-check! "group-inverse" (mau/ac-canon mmt-group "i(a) * a") "e")
+(mmt-check! "group-cancel" (mau/ac-canon mmt-group "i(a) * a * b") "b")
+(mmt-check! "group-cancel-mid" (mau/ac-canon mmt-group "b * i(a) * a") "b")
+(mmt-check! "group-double-inv" (mau/ac-canon mmt-group "i(i(a))") "a")
+(mmt-check! "group-id-left" (mau/ac-canon mmt-group "e * a") "a")
+(mmt-check! "group-right-inv" (mau/ac-canon mmt-group "a * i(a) * b") "b")
+
+;; ---- AC equality (canonical form) ----
+
+(define mmt-th (mau/build-theory mmt-acg))
+
+(mmt-check!
+  "ac-equal-reorder"
+  (mau/ac-equal?
+    mmt-th
+    (mau/parse-term-in mmt-acg "a + b + c")
+    (mau/parse-term-in mmt-acg "c + a + b"))
+  true)
+(mmt-check!
+  "ac-equal-renest"
+  (mau/ac-equal?
+    mmt-th
+    (mau/parse-term-in mmt-acg "(a + b) + c")
+    (mau/parse-term-in mmt-acg "a + (b + c)"))
+  true)
+(mmt-check!
+  "ac-noncomm-order"
+  (mau/ac-equal?
+    mmt-th
+    (mau/parse-term-in mmt-acg "a . b")
+    (mau/parse-term-in mmt-acg "b . a"))
+  false)
+
+(define mau-matching-tests-run! (fn () {:failures mmt-failures :total (+ mmt-pass mmt-fail) :passed mmt-pass :failed mmt-fail}))
diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md
index 57692dba..87e3b4d3 100644
--- a/plans/maude-on-sx.md
+++ b/plans/maude-on-sx.md
@@ -73,12 +73,12 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
 - [x] Tests: peano arithmetic, list manipulation, propositional logic simplifier.
 
 ### Phase 3 — Equational matching (assoc / comm / id)
-- [ ] Extend matching to handle `assoc` operators (flatten then match across permutations of subterm groups).
-- [ ] Handle `comm` (try both argument orderings).
-- [ ] Handle `id: e` (X * e ≡ X).
-- [ ] Combinations: `assoc comm id` together.
-- [ ] Returns *all* matches, not just first — caller drives.
-- [ ] Tests: classic AC-matching examples (multiset rewriting, set theory, group equations).
+- [x] Extend matching to handle `assoc` operators (flatten then match across permutations of subterm groups).
+- [x] Handle `comm` (try both argument orderings).
+- [x] Handle `id: e` (X * e ≡ X).
+- [x] Combinations: `assoc comm id` together.
+- [x] Returns *all* matches, not just first — caller drives.
+- [x] Tests: classic AC-matching examples (multiset rewriting, set theory, group equations).
 
 ### Phase 4 — Conditional equations
 - [ ] `ceq L = R if Cond` — apply only when `Cond` reduces to true.
@@ -153,5 +153,29 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
   non-linear `same(X,X)`. Innermost is fine for confluent terminating eq sets;
   Phase 3 will replace the matcher with AC-aware matching (multi-valued).
 
+- **Phase 3 (matching modulo assoc/comm/id) — DONE, 119/119 total. THE CHISEL.**
+  `lib/maude/matching.sx`. `mau/mm` is the multi-valued matcher (returns the
+  full list of substitutions): free=positional, comm=both orderings,
+  assoc=flatten f-spine + ordered sequence match (vars grab contiguous blocks),
+  assoc+comm=multiset match (vars grab sub-multisets via `mau/all-splits` =
+  2^n subset/complement pairs). `id: e` lets a var grab the empty block
+  (contributing e); `mau/var-kmin` gives kmin 0 under id. `mau/canon` is the
+  AC-canonical printout (flatten, drop identities, sort comm args) and powers
+  `mau/ac-equal?` (used for bound-var checks too). AC *rewriting* extends each
+  f-AC equation l=r with rest vars — comm: `f(l,$R)`; assoc: `f($L,l,$R)` —
+  so a rule fires on any sub-multiset/subword (`$`-prefixed rest vars allowed
+  empty). `mau/first-change` walks candidate matches and only commits a rewrite
+  that changes the canonical form — this is what makes idempotency (`X U X = X`)
+  and identity-absorbing matches terminate. API: `mau/ac-reduce` /
+  `mau/ac-reduce->str` / `mau/ac-canon` / `mau/match-all`. Verified: AC match
+  counts (X+Y vs a+b+c = 6), bag collapse, set dedup with empty, group
+  cancellation (assoc non-comm + inverse).
+  - Notes for next phases: AC matching is multi-valued — Phase 5 rule
+    application should iterate ALL of `mau/mm`'s results, not just first. The
+    `mau/ac-rewrite-eq` extension trick (rest vars) is the reusable core for
+    a future `lib/guest/rewriting/` (Phase 8). Keep `mau/canon` as the equality
+    oracle. `$EMPTY` is a transient marker for empty rest blocks w/o id; never
+    leaks past `mau/restv`.
+
 ## Blockers
 _(none)_