diff --git a/lib/maude/conditional.sx b/lib/maude/conditional.sx
index 00ea6aa2..31c76965 100644
--- a/lib/maude/conditional.sx
+++ b/lib/maude/conditional.sx
@@ -10,8 +10,10 @@
 ;; — termination rests on the guard reducing on structurally smaller arguments
 ;; (and the global fuel guard).
 ;;
-;; This engine subsumes mau/ac-reduce: an unconditional equation has cond nil,
-;; which always holds. Phases 5+ build on the c-* entry points.
+;; Single-step firing uses the short-circuiting matcher in fire.sx
+;; (mau/fire-eq) so reduction is not quadratic/exponential in AC argument size.
+;; The eager candidate enumeration (mau/eq-candidates) is retained for `search`
+;; (rewrite.sx), which genuinely needs every successor.
 
 (define
   mau/ac-candidates
@@ -92,7 +94,7 @@
       (empty? eqs)
       nil
       (let
-        ((r (mau/try-candidates theory all-eqs (get (first eqs) :cond) term (mau/eq-candidates theory (first eqs) term))))
+        ((r (mau/fire-eq theory all-eqs (first eqs) term)))
         (if (= r nil) (mau/crewrite-loop theory all-eqs (rest eqs) term) r)))))
 
 (define
diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf
index 2e986227..054a00c7 100644
--- a/lib/maude/conformance.conf
+++ b/lib/maude/conformance.conf
@@ -11,6 +11,8 @@ PRELOADS=(
   lib/maude/reduce.sx
   lib/maude/matching.sx
   lib/maude/conditional.sx
+  lib/maude/fire.sx
+  lib/maude/rewrite.sx
 )
 
 SUITES=(
@@ -18,4 +20,5 @@ SUITES=(
   "reduce:lib/maude/tests/reduce.sx:(mau-reduce-tests-run!)"
   "matching:lib/maude/tests/matching.sx:(mau-matching-tests-run!)"
   "conditional:lib/maude/tests/conditional.sx:(mau-conditional-tests-run!)"
+  "rewrite:lib/maude/tests/rewrite.sx:(mau-rewrite-tests-run!)"
 )
diff --git a/lib/maude/fire.sx b/lib/maude/fire.sx
new file mode 100644
index 00000000..114f66f4
--- /dev/null
+++ b/lib/maude/fire.sx
@@ -0,0 +1,250 @@
+;; lib/maude/fire.sx — short-circuiting rule/equation firing.
+;;
+;; The eager matcher (mau/match-multiset) enumerates EVERY substitution, which
+;; is what `mau/match-all` and `search` need. But for a single rewrite step we
+;; only need the FIRST usable match — and eager enumeration is exponential when
+;; an AC argument has many identical elements (q ; q ; ... ; q). These
+;; find-matchers thread a predicate and stop at the first complete match for
+;; which it returns non-nil; the predicate builds the rewritten term and checks
+;; "progresses AND condition holds", so firing short-circuits on the first
+;; productive match instead of materialising the whole solution set.
+;;
+;; pred : subst -> result-term-or-nil   (result is always a term, never nil)
+
+(define
+  mau/try-list
+  (fn
+    (substs cont)
+    (if
+      (empty? substs)
+      nil
+      (let
+        ((r (cont (first substs))))
+        (if (= r nil) (mau/try-list (rest substs) cont) r)))))
+
+;; ---- multiset (assoc+comm) find ----
+
+(define
+  mau/ms-find
+  (fn
+    (theory f pels sels s id pred)
+    (cond
+      ((empty? pels) (if (empty? sels) (pred s) nil))
+      (else
+        (let
+          ((p (first pels)) (prest (rest pels)))
+          (if
+            (mau/var? p)
+            (mau/ms-find-var
+              theory
+              f
+              prest
+              sels
+              s
+              (mau/vname p)
+              id
+              pred
+              (mau/var-kmin (mau/vname p) id)
+              (mau/all-splits sels))
+            (mau/ms-find-nonvar theory f p prest sels s id pred 0)))))))
+
+(define
+  mau/ms-find-nonvar
+  (fn
+    (theory f p prest sels s id pred i)
+    (if
+      (>= i (len sels))
+      nil
+      (let
+        ((others (mau/remove-at sels i)))
+        (let
+          ((r (mau/try-list (mau/mm theory p (nth sels i) s) (fn (s2) (mau/ms-find theory f prest others s2 id pred)))))
+          (if
+            (not (= r nil))
+            r
+            (mau/ms-find-nonvar
+              theory
+              f
+              p
+              prest
+              sels
+              s
+              id
+              pred
+              (+ i 1))))))))
+
+(define
+  mau/ms-find-var
+  (fn
+    (theory f prest sels s name id pred kmin splits)
+    (if
+      (empty? splits)
+      nil
+      (let
+        ((chosen (first (first splits)))
+          (rests (nth (first splits) 1)))
+        (if
+          (< (len chosen) kmin)
+          (mau/ms-find-var
+            theory
+            f
+            prest
+            sels
+            s
+            name
+            id
+            pred
+            kmin
+            (rest splits))
+          (let
+            ((s2 (mau/bind-check theory s name (mau/rebuild f chosen id))))
+            (let
+              ((r (if (= s2 nil) nil (mau/ms-find theory f prest rests s2 id pred))))
+              (if
+                (not (= r nil))
+                r
+                (mau/ms-find-var
+                  theory
+                  f
+                  prest
+                  sels
+                  s
+                  name
+                  id
+                  pred
+                  kmin
+                  (rest splits))))))))))
+
+;; ---- sequence (assoc, ordered) find ----
+
+(define
+  mau/seq-find
+  (fn
+    (theory f pels sels s id pred)
+    (cond
+      ((empty? pels) (if (empty? sels) (pred s) nil))
+      (else
+        (let
+          ((p (first pels)) (prest (rest pels)))
+          (if
+            (mau/var? p)
+            (mau/seq-find-var
+              theory
+              f
+              prest
+              sels
+              s
+              (mau/vname p)
+              id
+              pred
+              (mau/var-kmin (mau/vname p) id))
+            (if
+              (empty? sels)
+              nil
+              (mau/try-list
+                (mau/mm theory p (first sels) s)
+                (fn
+                  (s2)
+                  (mau/seq-find theory f prest (rest sels) s2 id pred))))))))))
+
+(define
+  mau/seq-find-var
+  (fn
+    (theory f prest sels s name id pred k)
+    (if
+      (> k (len sels))
+      nil
+      (let
+        ((s2 (mau/bind-check theory s name (mau/rebuild f (mau/take sels k) id))))
+        (let
+          ((r (if (= s2 nil) nil (mau/seq-find theory f prest (mau/drop sels k) s2 id pred))))
+          (if
+            (not (= r nil))
+            r
+            (mau/seq-find-var
+              theory
+              f
+              prest
+              sels
+              s
+              name
+              id
+              pred
+              (+ k 1))))))))
+
+;; ---- firing an equation/rule (returns rewritten term or nil) ----
+
+(define
+  mau/fire-plain
+  (fn
+    (theory eqs eq term cnd substs)
+    (if
+      (empty? substs)
+      nil
+      (let
+        ((res (mau/subst-apply (first substs) (get eq :rhs))))
+        (if
+          (and
+            (not (mau/ac-equal? theory res term))
+            (mau/cond-holds? theory eqs cnd (first substs)))
+          res
+          (mau/fire-plain theory eqs eq term cnd (rest substs)))))))
+
+(define
+  mau/fire-ac
+  (fn
+    (theory eqs f th eq term cnd)
+    (let
+      ((id (get th :id))
+        (pels (mau/flatten-op theory f (get eq :lhs)))
+        (sels (mau/flatten-op theory f term)))
+      (let
+        ((pred (fn (s) (let ((res (mau/ac-eq-result theory f th eq s))) (if (and (not (mau/ac-equal? theory res term)) (mau/cond-holds? theory eqs cnd s)) res nil)))))
+        (if
+          (get th :comm)
+          (mau/ms-find
+            theory
+            f
+            (mau/append2 pels (list (mau/var "$R" "")))
+            sels
+            {}
+            id
+            pred)
+          (mau/seq-find
+            theory
+            f
+            (mau/append2
+              (list (mau/var "$L" ""))
+              (mau/append2 pels (list (mau/var "$R" ""))))
+            sels
+            {}
+            id
+            pred))))))
+
+(define
+  mau/fire-eq
+  (fn
+    (theory eqs eq term)
+    (let
+      ((lhs (get eq :lhs)) (cnd (get eq :cond)))
+      (if
+        (mau/app? lhs)
+        (let
+          ((th (mau/th-of theory (mau/op lhs))))
+          (if
+            (get th :assoc)
+            (mau/fire-ac theory eqs (mau/op lhs) th eq term cnd)
+            (mau/fire-plain
+              theory
+              eqs
+              eq
+              term
+              cnd
+              (mau/mm theory lhs term {}))))
+        (mau/fire-plain
+          theory
+          eqs
+          eq
+          term
+          cnd
+          (mau/mm theory lhs term {}))))))
diff --git a/lib/maude/rewrite.sx b/lib/maude/rewrite.sx
new file mode 100644
index 00000000..0463c685
--- /dev/null
+++ b/lib/maude/rewrite.sx
@@ -0,0 +1,284 @@
+;; lib/maude/rewrite.sx — system modules + rewrite rules (Phase 5).
+;;
+;; Equations (eq/ceq) are applied to a fixpoint to NORMALISE (confluent by
+;; intent). Rules (rl/crl) are TRANSITIONS: asymmetric (=>), possibly
+;; nondeterministic, NOT applied to a fixpoint. Maude's `rew` interleaves
+;; the two: normalise with equations, fire one rule, renormalise, repeat.
+;;
+;; Rule firing reuses the shared firing machinery — a rule dict carries
+;; :lhs/:rhs/:cond exactly like an equation, so `mau/fire-eq` (short-circuit,
+;; fire.sx) applies unchanged (matching modulo the AC theory; crl guards
+;; evaluated with the equations). A rule fires only if it both progresses and
+;; its condition holds.
+;;
+;; `mau/rewrite` follows the default strategy (top-down, leftmost-outermost,
+;; first applicable rule) for one path. `mau/search` does breadth-first reach
+;; over ALL one-step successors — for puzzle solvers / protocol simulators
+;; where the answer is on a branch `rew` would not take.
+
+(define mau/rew-fuel 100000)
+
+;; ---- single-step, default strategy (first applicable, leftmost-outermost) ----
+
+(define
+  mau/rules-at-top
+  (fn
+    (theory eqs rules term)
+    (if
+      (empty? rules)
+      nil
+      (let
+        ((r (mau/fire-eq theory eqs (first rules) term)))
+        (if (= r nil) (mau/rules-at-top theory eqs (rest rules) term) r)))))
+
+(define
+  mau/apply-rule-once
+  (fn
+    (theory eqs rules term)
+    (let
+      ((top (mau/rules-at-top theory eqs rules term)))
+      (if
+        (not (= top nil))
+        top
+        (if
+          (mau/app? term)
+          (mau/apply-rule-in-args
+            theory
+            eqs
+            rules
+            (mau/op term)
+            (mau/args term)
+            (list))
+          nil)))))
+
+(define
+  mau/apply-rule-in-args
+  (fn
+    (theory eqs rules op done todo)
+    (if
+      (empty? todo)
+      nil
+      (let
+        ((r (mau/apply-rule-once theory eqs rules (first todo))))
+        (if
+          (= r nil)
+          (mau/apply-rule-in-args
+            theory
+            eqs
+            rules
+            op
+            (mau/append2 done (list (first todo)))
+            (rest todo))
+          (mau/app op (mau/append2 done (cons r (rest todo)))))))))
+
+(define
+  mau/rewrite-steps
+  (fn
+    (theory eqs rules term steps)
+    (if
+      (<= steps 0)
+      (mau/cnormalize theory eqs term mau/reduce-fuel)
+      (let
+        ((nf (mau/cnormalize theory eqs term mau/reduce-fuel)))
+        (let
+          ((r (mau/apply-rule-once theory eqs rules nf)))
+          (if
+            (= r nil)
+            nf
+            (mau/rewrite-steps theory eqs rules r (- steps 1))))))))
+
+(define
+  mau/rewrite
+  (fn
+    (m term)
+    (mau/rewrite-steps
+      (mau/build-theory m)
+      (mau/module-eqs m)
+      (mau/module-rules m)
+      term
+      mau/rew-fuel)))
+
+(define
+  mau/rew
+  (fn
+    (m src n)
+    (mau/rewrite-steps
+      (mau/build-theory m)
+      (mau/module-eqs m)
+      (mau/module-rules m)
+      (mau/parse-term-in m src)
+      n)))
+
+(define
+  mau/rewrite-term
+  (fn (m src) (mau/rewrite m (mau/parse-term-in m src))))
+
+(define
+  mau/rewrite->str
+  (fn (m src) (mau/term->str (mau/rewrite-term m src))))
+
+(define
+  mau/rewrite-canon
+  (fn (m src) (mau/canon (mau/build-theory m) (mau/rewrite-term m src))))
+
+(define mau/rew->str (fn (m src n) (mau/term->str (mau/rew m src n))))
+
+(define
+  mau/rew-canon
+  (fn (m src n) (mau/canon (mau/build-theory m) (mau/rew m src n))))
+
+;; ---- all one-step successors (for search; eager enumeration) ----
+
+(define
+  mau/cands-results
+  (fn
+    (theory eqs cond term cands)
+    (mau/concat-map
+      (fn
+        (c)
+        (if
+          (and
+            (not (mau/ac-equal? theory (get c :result) term))
+            (mau/cond-holds? theory eqs cond (get c :s)))
+          (list (mau/cnormalize theory eqs (get c :result) mau/reduce-fuel))
+          (list)))
+      cands)))
+
+(define
+  mau/top-successors
+  (fn
+    (theory eqs rules term)
+    (mau/concat-map
+      (fn
+        (rule)
+        (mau/cands-results
+          theory
+          eqs
+          (get rule :cond)
+          term
+          (mau/eq-candidates theory rule term)))
+      rules)))
+
+(define
+  mau/arg-successors
+  (fn
+    (theory eqs rules op done todo)
+    (if
+      (empty? todo)
+      (list)
+      (mau/append2
+        (map
+          (fn
+            (sub)
+            (mau/app op (mau/append2 done (cons sub (rest todo)))))
+          (mau/all-successors theory eqs rules (first todo)))
+        (mau/arg-successors
+          theory
+          eqs
+          rules
+          op
+          (mau/append2 done (list (first todo)))
+          (rest todo))))))
+
+(define
+  mau/all-successors
+  (fn
+    (theory eqs rules term)
+    (mau/append2
+      (mau/top-successors theory eqs rules term)
+      (if
+        (mau/app? term)
+        (mau/arg-successors
+          theory
+          eqs
+          rules
+          (mau/op term)
+          (mau/args term)
+          (list))
+        (list)))))
+
+(define
+  mau/successors
+  (fn
+    (m src)
+    (let
+      ((theory (mau/build-theory m)) (eqs (mau/module-eqs m)))
+      (map
+        (fn (t) (mau/canon theory t))
+        (mau/all-successors
+          theory
+          eqs
+          (mau/module-rules m)
+          (mau/cnormalize
+            theory
+            eqs
+            (mau/parse-term-in m src)
+            mau/reduce-fuel))))))
+
+;; ---- breadth-first reachability search ----
+
+(define
+  mau/canon-list
+  (fn (theory ts) (map (fn (t) (mau/canon theory t)) ts)))
+
+(define
+  mau/bfs-search
+  (fn
+    (theory eqs rules frontier seen goal depth)
+    (cond
+      ((mau/member? goal (mau/canon-list theory frontier)) true)
+      ((<= depth 0) false)
+      ((empty? frontier) false)
+      (else
+        (let
+          ((newf (list)) (newseen seen))
+          (for-each
+            (fn
+              (t)
+              (for-each
+                (fn
+                  (succ)
+                  (let
+                    ((c (mau/canon theory succ)))
+                    (when
+                      (not (mau/member? c newseen))
+                      (do
+                        (set! newseen (cons c newseen))
+                        (append! newf succ)))))
+                (mau/all-successors theory eqs rules t)))
+            frontier)
+          (mau/bfs-search
+            theory
+            eqs
+            rules
+            newf
+            newseen
+            goal
+            (- depth 1)))))))
+
+(define
+  mau/search
+  (fn
+    (m start-src goal-src max-depth)
+    (let
+      ((theory (mau/build-theory m))
+        (eqs (mau/module-eqs m))
+        (rules (mau/module-rules m)))
+      (let
+        ((start (mau/cnormalize theory eqs (mau/parse-term-in m start-src) mau/reduce-fuel))
+          (goal
+            (mau/canon
+              theory
+              (mau/cnormalize
+                theory
+                eqs
+                (mau/parse-term-in m goal-src)
+                mau/reduce-fuel))))
+        (mau/bfs-search
+          theory
+          eqs
+          rules
+          (list start)
+          (list (mau/canon theory start))
+          goal
+          max-depth)))))
diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json
index 5e552292..b0574a30 100644
--- a/lib/maude/scoreboard.json
+++ b/lib/maude/scoreboard.json
@@ -1,13 +1,14 @@
 {
   "lang": "maude",
-  "total_passed": 138,
+  "total_passed": 159,
   "total_failed": 0,
-  "total": 138,
+  "total": 159,
   "suites": [
     {"name":"parse","passed":65,"failed":0,"total":65},
     {"name":"reduce","passed":26,"failed":0,"total":26},
     {"name":"matching","passed":28,"failed":0,"total":28},
-    {"name":"conditional","passed":19,"failed":0,"total":19}
+    {"name":"conditional","passed":19,"failed":0,"total":19},
+    {"name":"rewrite","passed":21,"failed":0,"total":21}
   ],
-  "generated": "2026-06-07T15:05:31+00:00"
+  "generated": "2026-06-07T15:22:28+00:00"
 }
diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md
index 12cd28a2..40a50af0 100644
--- a/lib/maude/scoreboard.md
+++ b/lib/maude/scoreboard.md
@@ -1,6 +1,6 @@
 # maude scoreboard
 
-**138 / 138 passing** (0 failure(s)).
+**159 / 159 passing** (0 failure(s)).
 
 | Suite | Passed | Total | Status |
 |-------|--------|-------|--------|
@@ -8,3 +8,4 @@
 | reduce | 26 | 26 | ok |
 | matching | 28 | 28 | ok |
 | conditional | 19 | 19 | ok |
+| rewrite | 21 | 21 | ok |
diff --git a/lib/maude/tests/rewrite.sx b/lib/maude/tests/rewrite.sx
new file mode 100644
index 00000000..c7e9ed0e
--- /dev/null
+++ b/lib/maude/tests/rewrite.sx
@@ -0,0 +1,114 @@
+;; lib/maude/tests/rewrite.sx — Phase 5: system modules + rewrite rules.
+
+(define mrw-pass 0)
+(define mrw-fail 0)
+(define mrw-failures (list))
+
+(define
+  mrw-check!
+  (fn
+    (name got expected)
+    (if
+      (= got expected)
+      (set! mrw-pass (+ mrw-pass 1))
+      (do
+        (set! mrw-fail (+ mrw-fail 1))
+        (append!
+          mrw-failures
+          (str name "  expected: " expected "  got: " got))))))
+
+;; ---- AC multiset transition (the headline: rule on a sub-multiset) ----
+
+(define
+  mrw-coins
+  (mau/parse-module
+    "mod COINS is\n  sort Marking .\n  op nil : -> Marking .\n  op q : -> Marking .\n  op d : -> Marking .\n  op _;_ : Marking Marking -> Marking [assoc comm id: nil] .\n  rl [change] : q ; q ; q ; q => d .\nendm"))
+
+(mrw-check! "coins-kind" (mau/module-kind mrw-coins) "mod")
+(mrw-check! "coins-rules" (len (mau/module-rules mrw-coins)) 1)
+(mrw-check! "coins-exact" (mau/rewrite-canon mrw-coins "q ; q ; q ; q") "d")
+(mrw-check!
+  "coins-5"
+  (mau/rewrite-canon mrw-coins "q ; q ; q ; q ; q")
+  "_;_(d,q)")
+(mrw-check!
+  "coins-8"
+  (mau/rewrite-canon mrw-coins "q ; q ; q ; q ; q ; q ; q ; q")
+  "_;_(d,d)")
+(mrw-check!
+  "coins-3-stuck"
+  (mau/rewrite-canon mrw-coins "q ; q ; q")
+  "_;_(q,q,q)")
+
+;; ---- cyclic state machine (bounded rew) ----
+
+(define
+  mrw-traffic
+  (mau/parse-module
+    "mod TRAFFIC is\n  sort Light .\n  ops red green yellow : -> Light .\n  rl [g] : red => green .\n  rl [y] : green => yellow .\n  rl [r] : yellow => red .\nendm"))
+
+(mrw-check! "traffic-1" (mau/rew->str mrw-traffic "red" 1) "green")
+(mrw-check! "traffic-2" (mau/rew->str mrw-traffic "red" 2) "yellow")
+(mrw-check! "traffic-3" (mau/rew->str mrw-traffic "red" 3) "red")
+(mrw-check! "traffic-0" (mau/rew->str mrw-traffic "green" 0) "green")
+
+;; ---- nondeterministic branching: rew (one path) vs search (all paths) ----
+
+(define
+  mrw-ndet
+  (mau/parse-module
+    "mod NDET is\n  sort S .\n  ops a b c d goal : -> S .\n  rl [r1] : a => b .\n  rl [r2] : a => c .\n  rl [r3] : b => d .\n  rl [r4] : c => goal .\nendm"))
+
+;; rew takes the first rule each step: a -> b -> d (stuck), never reaches goal.
+(mrw-check! "ndet-rew-path" (mau/rewrite->str mrw-ndet "a") "d")
+(mrw-check! "ndet-succ" (mau/successors mrw-ndet "a") (list "b" "c"))
+(mrw-check!
+  "ndet-search-goal"
+  (mau/search mrw-ndet "a" "goal" 5)
+  true)
+(mrw-check!
+  "ndet-search-shallow"
+  (mau/search mrw-ndet "a" "goal" 1)
+  false)
+(mrw-check! "ndet-search-self" (mau/search mrw-ndet "a" "a" 3) true)
+(mrw-check! "ndet-search-d" (mau/search mrw-ndet "a" "d" 5) true)
+
+;; ---- conditional rule (crl with equational guard) ----
+
+(define
+  mrw-clock
+  (mau/parse-module
+    "mod CLOCK is\n  sorts Nat Bool .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op true : -> Bool .\n  op false : -> Bool .\n  op _<_ : Nat Nat -> Bool .\n  op clk : Nat -> Nat .\n  vars M N : Nat .\n  eq 0 < s N = true .\n  eq N < 0 = false .\n  eq s M < s N = M < N .\n  crl [tick] : clk(N) => clk(s N) if N < s s s 0 = true .\nendm"))
+
+;; tick fires while N < 3, then stops at clk(3).
+(mrw-check!
+  "clock-run"
+  (mau/rewrite->str mrw-clock "clk(0)")
+  "clk(s_(s_(s_(0))))")
+(mrw-check!
+  "clock-from-1"
+  (mau/rewrite->str mrw-clock "clk(s 0)")
+  "clk(s_(s_(s_(0))))")
+(mrw-check!
+  "clock-step1"
+  (mau/rew->str mrw-clock "clk(0)" 1)
+  "clk(s_(0))")
+
+;; ---- eqs interleave with rules ----
+
+(define
+  mrw-mix
+  (mau/parse-module
+    "mod MIX is\n  sort Nat .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op _+_ : Nat Nat -> Nat .\n  op f : Nat -> Nat .\n  vars X Y : Nat .\n  eq 0 + Y = Y .\n  eq s X + Y = s (X + Y) .\n  rl [step] : f(X) => f(X + s 0) .\nendm"))
+
+;; each rule step adds one (via the rule), eqs normalise the sum.
+(mrw-check!
+  "mix-step1"
+  (mau/rew->str mrw-mix "f(s 0)" 1)
+  "f(s_(s_(0)))")
+(mrw-check!
+  "mix-step2"
+  (mau/rew->str mrw-mix "f(0)" 2)
+  "f(s_(s_(0)))")
+
+(define mau-rewrite-tests-run! (fn () {:failures mrw-failures :total (+ mrw-pass mrw-fail) :passed mrw-pass :failed mrw-fail}))
diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md
index 6964e836..df8c4067 100644
--- a/plans/maude-on-sx.md
+++ b/plans/maude-on-sx.md
@@ -86,10 +86,10 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
 - [x] Tests: gcd, sorting, conditional simplifications.
 
 ### Phase 5 — System modules + rewrite rules
-- [ ] `mod ... endm` syntax with `rl` rules.
-- [ ] Rules apply asymmetrically (`=>` not `=`); fairness across rules.
-- [ ] Default strategy: top-down, leftmost-outermost, first applicable rule.
-- [ ] Tests: state-transition systems (puzzle solvers, protocol simulators).
+- [x] `mod ... endm` syntax with `rl` rules.
+- [x] Rules apply asymmetrically (`=>` not `=`); fairness across rules.
+- [x] Default strategy: top-down, leftmost-outermost, first applicable rule.
+- [x] Tests: state-transition systems (puzzle solvers, protocol simulators).
 
 ### Phase 6 — Strategy language
 - [ ] Compose strategies: sequential `;`, alternative `|`, iteration `*`, fixed-point.
@@ -195,5 +195,30 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
     right-parenthesized, or add a `gather`/parse-assoc attr later if a test
     needs bare `a : b : c`.
 
+- **Phase 5 (system modules + rewrite rules) — DONE, 159/159 total.**
+  `lib/maude/rewrite.sx` + `lib/maude/fire.sx`. Rules (rl/crl) reuse the
+  equation firing machinery (a rule dict is shaped like an eq). `mau/rewrite`
+  is the default strategy: normalise with eqs (`creduce`), fire ONE rule
+  top-down/leftmost-outermost/first-applicable, renormalise, repeat (bounded
+  by fuel). `mau/rew m src n` = bounded `rew [n]`. `mau/search` is BFS over
+  ALL one-step successors (`mau/all-successors`) for reachability — solves the
+  branching `goal` reachable only off the path `rew` takes. Verified: AC
+  multiset coin-change (rule on a sub-multiset), cyclic traffic light (bounded),
+  branching nondeterminism (rew vs search), conditional `crl` clock, eq/rule
+  interleaving.
+  - **PERF (important):** `lib/maude/fire.sx` is the short-circuiting matcher —
+    `mau/fire-eq` finds the FIRST productive match via predicate-threaded
+    `mau/ms-find`/`mau/seq-find` instead of materialising the whole solution
+    set. Without it, AC rewriting on N identical elements is exponential
+    (`q;q;q;q;q;q;q;q` went 60s+ → <1s). The eager `mau/match-multiset` /
+    `mau/eq-candidates` are kept ONLY for `mau/match-all` and `search` (which
+    truly need every solution). Phase 4 `creduce` and Phase 5 rules both fire
+    via `mau/fire-eq`. Keep this split: never route single-step rewriting
+    through the eager enumerator.
+  - Notes: juxtaposition `__` (empty-token mixfix) and `gather` are NOT parsed —
+    use an explicit infix op for multisets and right-parenthesise list literals.
+    `.` can't be an op token (statement terminator). `mau/search` is the prime
+    Phase 7 reflection / Phase 8 extraction target alongside the matcher.
+
 ## Blockers
 _(none)_