diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md
index 30519136..8e2055f1 100644
--- a/plans/minikanren-on-sx.md
+++ b/plans/minikanren-on-sx.md
@@ -173,6 +173,29 @@ _(none yet)_
 
 _Newest first._
 
+- **2026-05-08** — **Session snapshot**: 17 lib files, 61 test files, 1229
+  library LOC + 4360 test LOC, **551/551 tests cumulative**. Library covers
+  Phases 1–5 fully, Phase 6 partial (FD helpers + intarith escape), Phase 7
+  documented via cyclic-graph divergence test. lib-guest validation
+  completed: `lib/minikanren/unify.sx` ≈ 50 LOC of local logic over
+  `lib/guest/match.sx`'s ≈100 LOC kit (kit earns ~3× by line count). Major
+  classic miniKanren tests green: appendo forwards/backwards, Peano
+  arithmetic, 4-queens, Pythagorean triples, family-relations / pet
+  puzzle / symbolic differentiation, 2x2 Latin square. Ready for Phase 6
+  (native FD with arc-consistency) and Phase 7 (tabling) as future work.
+- **2026-05-08** — **zip-with-o**: element-wise relational combine over two
+  lists with a 3-arg combiner. Ground-only by composition. 5 new tests.
+- **2026-05-08** — **take-while-o + drop-while-o**: predicate-driven
+  prefix/suffix split. Roundtrip property verified. 8 new tests.
+- **2026-05-08** — **arith-progo**: arithmetic-progression list generator
+  via project. 6 new tests.
+- **2026-05-08** — **counto**: count occurrences of x in l (intarith).
+  6 new tests.
+- **2026-05-08** — **nub-o**: dedupe via membero-on-tail. Multiplicity
+  caveat documented in tests. 5 new tests.
+- **2026-05-08** — **simplify-step-o**: algebraic identity simplifier
+  (conda demo). 6 new tests.
+- **2026-05-08** — **flat-mapo**: concatMap-style relation. 5 new tests.
 - **2026-05-08** — **foldl-o (relational left fold)**: complement to foldr-o. Combiner has args (acc, head) -> new-acc. (foldl-o pluso-i (1 2 3 4 5) 0 q) -> 15; (foldl-o flipped-conso l () q) reverses l. 5 new tests, 510/510 cumulative.
 - **2026-05-08** — **foldr-o (relational right fold)**: takes a 3-arg combiner relation rel, a list, an initial accumulator, produces the result. (foldr-o appendo lists () q) is a flatten; (foldr-o conso l () q) rebuilds l. 4 new tests, 505/505 cumulative.
 - **2026-05-08** — **enumerate-i / enumerate-from-i — 500-test milestone**: index-each-element relations. (enumerate-i l result) -> result is l with each element paired with its 0-based index. (enumerate-from-i n l result) starts at n. 5 new tests, **501/501** cumulative.