# Thema: The Declarative Chess Theme Specification Language


Thema is the language Thema Studio uses to describe and detect themes in orthodox mate-in-two (`#2`) problems.
**New to Thema?** Read the [Tutorial](#3-tutorial-from-scratch-to-complex-themes) (Lessons 1–7), then keep the
[Language Reference](#4-language-reference) and [Primitives](#5-complete-standard-library-of-primitives) at hand.

---

## Table of Contents

**Part I: Learn**

1. [Language Overview & Philosophy](#1-language-overview--philosophy)
2. [Language Name & Etymology](#2-language-name--etymology)
3. [Tutorial: From Scratch to Complex Themes](#3-tutorial-from-scratch-to-complex-themes)
   - [Lesson 1: Anatomy of a Thema Spec](#lesson-1-anatomy-of-a-thema-spec)
   - [Lesson 2: Simple Move Characteristics & Geometry](#lesson-2-simple-move-characteristics--geometry)
   - [Lesson 3: Tactical Interferences (Grimshaw, Novotny & Plachutta)](#lesson-3-tactical-interferences-grimshaw-novotny--plachutta)
   - [Lesson 4: Multi-Phase Changed Mates (Dombrovskis & Rukhlis)](#lesson-4-multi-phase-changed-mates-dombrovskis--rukhlis)
   - [Lesson 5: Threat Separation & Try Refutations (Barnes & Cyclic)](#lesson-5-threat-separation--try-refutations-barnes--cyclic)
   - [Lesson 6: Sets, Order-Invariance, and Symmetries](#lesson-6-sets-order-invariance-and-symmetries)
   - [Lesson 7: Why Doesn't My Spec Match? (Implicit Rules & the Debugger)](#lesson-7-why-doesnt-my-spec-match-implicit-rules--the-debugger)

**Part II: Reference**

4. [Language Reference](#4-language-reference)
   - [Formal Grammar (EBNF)](#formal-grammar-ebnf)
   - [Matrix Grid & Phase Rows](#matrix-grid--phase-rows)
   - [Cell Identifiers, Conventions, Inline Annotations & Shorthands](#cell-identifiers-conventions-inline-annotations--shorthands)
   - [Variables & Binding Scopes](#variables--binding-scopes)
   - [Unified Move Properties & Relational Methods](#unified-move-properties--relational-methods)
   - [Square Properties & Special Identifiers](#square-properties--special-identifiers)
   - [Literals, Roles & Constants](#literals-roles--constants)
   - [Operators & Precedence](#operators--precedence)
   - [Set Expressions & Algebra](#set-expressions--algebra)
   - [Aggregation Primitives (`count`, `count_distinct`)](#aggregation-primitives-count-count_distinct)
   - [The `with` Clause (Per-Theme Quality Configuration)](#the-with-clause-per-theme-quality-configuration)
   - [The `subsumes` Clause & Automatic Subsumption Hierarchy](#the-subsumes-clause--automatic-subsumption-hierarchy)
   - [The `story` / `format` Clause (Presentation & Dynamic Story Engine)](#the-story--format-clause-presentation--dynamic-story-engine)
5. [Complete Standard Library of Primitives](#5-complete-standard-library-of-primitives)
   - [5.1 Geometry & Board Rays](#51-geometry--board-rays)
   - [5.2 Square Navigation & Offsets](#52-square-navigation--offsets)
   - [5.3 Board Position Specifiers & Pin Primitives](#53-board-position-specifiers--pin-primitives)
   - [5.4 Guards, Attacks & Line Relations](#54-guards-attacks--line-relations)
   - [5.5 Batteries & Half-Batteries](#55-batteries--half-batteries)
   - [5.6 King Flights & Sacrifices](#56-king-flights--sacrifices)
   - [5.7 Checkmate Footprints & Echoes](#57-checkmate-footprints--echoes)
   - [5.8 Phase, Table & Positional Metrics](#58-phase-table--positional-metrics)
6. [Pattern Matching & Try Quality Engine](#6-pattern-matching--try-quality-engine)
   - [Pattern-Driven Constraints (Eliminating Boilerplate)](#pattern-driven-constraints-eliminating-boilerplate)
   - [Automatic Try Quality Filtering](#automatic-try-quality-filtering)
7. [Theme Authoring Guidelines & Anti-Patterns](#7-theme-authoring-guidelines--anti-patterns)
8. [Canonical Themes Cookbook](#8-canonical-themes-cookbook)

**Part III: Appendices**

9. [Extended Theme Catalogue](#9-extended-theme-catalogue)

---

## 1. Language Overview & Philosophy

**Thema** is a domain-specific declarative language engineered specifically for recognizing, analyzing, and proving checkmate problem themes in orthodox chess compositions (primarily direct mate in two moves, `#2`).

Traditional chess problem software detects themes imperatively: hardcoding nested loops, maintaining ad-hoc board state flags, and writing hundreds of lines of procedural code for each theme. In contrast, **Thema separates theme topology from chess geometry**:

```
+-------------------------------------------------------+
|  THEMA MATRIX: Phase & Defense Relationship Grid      |
|  (Which moves happen in which phases against what)   |
+-------------------------------------------------------+
                           │
                           ▼
+-------------------------------------------------------+
|  WHERE CLAUSE: Chess Predicates & Geometric Calculus   |
|  (Collinear rays, self-blocks, pins, roles, sets)     |
|  * Omitted whenever the matrix alone defines the theme|
+-------------------------------------------------------+
                           │
                           ▼
+-------------------------------------------------------+
|  AUTOMATIC TRY QUALITY & PATTERN-DRIVEN MATCHING      |
|  (No boilerplate: threat & refutation counts are      |
|   inferred directly from pattern cells)               |
+-------------------------------------------------------+
```

Every Thema specification is pure, declarative, and order-invariant.

---

## 2. Language Name & Etymology

### Name: **Thema** (pronounced */ˈteɪ.mə/* or */ˈθiː.mə/*)

- **Origin**: *Thema* (plural *Themen* / *Themata*) is the universal international term across German, Russian, French, and Dutch chess problem literature (*"Das Dombrovskis-Thema"*, *"Тема Гримшоу"*). Milan Velimirović and Kari Valtonen’s *The Chess Problem Encyclopedia* and the FIDE Album codify chess problem art through *Themen*.
- **Alternative Formal Expansion**: **THEMA** — **TH**eme & **E**ffects **M**atrix **A**rchitecture.
- **File Extension**: `.thm` (used by Thema Studio, the `themes/*.thm` reference specs in this repository, and all import/export).

---

## 3. Tutorial: From Scratch to Complex Themes

### Lesson 1: Anatomy of a Thema Spec

A Thema specification consists of up to four sections:
1. **The Matrix Grid**: One or more rows defining the phase structure (`key`, `try`, `set`, `vir`, `any`, `def`), an optional phase move and parenthesized threat `phase Move? (Threat?)`, and defensive variation replies enclosed in brackets `[...]`.
2. **The `where` Clause (Optional)**: A boolean expression defining tactical or geometric constraints (roles, squares, rays, pins). When the matrix topology alone uniquely defines the theme (such as Dombrovskis, Zagoruiko, Barnes, or Switchback), no `where` clause is required.
3. **The `with` Clause (Optional)**: Per-theme candidate quality configuration (overriding try-weakness rules or enabling sacrifices and checks).
4. **The `story` Clause (Optional)**: Natural language template interpolating thematic moves and squares for reports and dashboards, with automatic resolution of `{K}`, `{Tr1}`, and `{a}`..`{h}` from the matched rows and columns.

Here is the specification for **Switchback** (a key piece returns to its origin square on move 2 to deliver mate):

```thema
key K [~K]
```
*(or written explicitly with a relational method: `key K [A] where A.switchback(K)`)*

- `key` specifies the **Key** phase (the solution).
- `K` outside brackets binds White's key move.
- `[~K]` inside brackets matches a variation checkmate that returns (`~K`) to `K`'s departure square (`A.from == K.to && A.to == K.from`).
- Square brackets `[...]` contain only defensive variation columns; the phase move and threat are written outside the brackets.

---

### Lesson 2: Simple Move Characteristics & Geometry

Suppose we want to specify a **Checking Key** (White's first move delivers check to the Black King):

```thema
key K:+
// or using a dot-property:
key K where K.check
```

Or a **Flight-Giving Key** (White's key grants the Black King new flight squares):

```thema
key K where K.flights_given > 0
```

Variables support unified dot-properties and relational methods:
- `K.from` and `K.to` (squares), `K.from.file` and `K.from.rank` (1..8)
- `K.role` (e.g. `'Q'`, `'R'`, `'B'`, `'N'`, `'P'`, `'K'`), `K.ortho_slider`, `K.diag_slider`
- `K.capture` (or `K.is_capture`), `K.check` (or `K.is_check`), `K.threat_count` (or `K.threats`), `Tr.refutation_count`, `K.waiting`, `K.sacrifice`, `a.self_block`, `a.self_pins`, `A.pure_mate`, `A.model_mate`, `X.fires_battery`
- Relational methods: `a.blocks(b, A)`, `A.recaptures(a)`, `A.umnov(a)`, `A.switchback(K)`, `a.unguards(B)`

---

### Lesson 3: Tactical Interferences (Grimshaw, Novotny & Plachutta)

#### Grimshaw (Mutual Interference)
Two Black line-pieces of different movement types (Rook and Bishop) arrive on the same intersection square, obstructing each other's defensive lines:

```thema
key [A B]
where same_square(a, b),
  {a.role, b.role} == {'R', 'B'},
  !a.capture,
  a.blocks(b, A),
  b.blocks(a, B)
```

**Key Concepts**:
1. **Variation Brackets `[A B]`**: `[A B]` binds the variation checkmates in defense columns 1 and 2, while implicitly binding their corresponding Black defenses to `a` and `b`.
2. **Relational `.blocks(other_def, mate)` Method**: `a.blocks(b, A)` asserts that `a`'s arrival square blocks the ray from `b.from` to `A.to` (`blocks_ray(a.to, b.from, A.to)`).
3. **Comma-Separated `where` Clauses**: Top-level commas `,` represent logical conjunction (`&&`).
4. **Set Equality `{a.role, b.role} == {'R', 'B'}`**: Order-invariant comparison—satisfied regardless of whether `a` is the Rook and `b` is the Bishop, or vice versa.

#### Novotny & Plachutta (Capture on Key Square `@K` + Mutual Interference)
Using the inline target square shorthand `def [a:x@K b:x@K]` (both defenses capture on `K`'s arrival square) and `unlike_sliders` / `like_sliders`:

```thema
// Novotny (Orthogonal vs Diagonal Sliders)
def [a:x@K b:x@K]
key K [A B]
where unlike_sliders(a, b),
  a.blocks(b, A),
  b.blocks(a, B)

// Plachutta (Like-Sliders)
def [a:x@K b:x@K]
key K [A B]
where a.from != b.from,
  like_sliders(a, b),
  !collinear(a.from, b.from, K.to),
  (A.recaptures(a) || B.recaptures(b)),
  a.blocks(b, A),
  b.blocks(a, B)
```

---

### Lesson 4: Multi-Phase Changed Mates (Dombrovskis & Rukhlis)

In multi-phase problems, separating the parenthesized threat `(A)` from the `[variation mates]` expresses phase relationships directly in the matrix.

#### Dombrovskis
A try threatens mate `(A)`, which Black refutes with defense `a` (`!`). A second try threatens mate `(B)`, refuted by defense `b` (`!`). In the Key, defenses `a` and `b` allow checkmates `A` and `B` respectively:

```thema
try (A) [! _]
try (B) [_ !]
key [A B]
```

**Structural Semantics**:
- **Parenthesized Threat `(A)`**: Writing a single variable in `(A)` binds the phase threat and enforces `threat_count == 1` (Rule 7).
- **Refutation Marker `!`**: Including a single `!` in a `try` row binds the refuting defense column and enforces `refutation_count == 1` (Rule 6).
- **Distinct Variables**: Different variable identifiers (`A` and `B`) are automatically constrained to be distinct moves.
- **Implicit Story Bindings**: When a `story` template references `{Tr1}`, `{Tr2}`, `{K}`, `{a}`, or `{b}`, the matcher resolves them from the locked table rows and columns without requiring explicit variables in the matrix.

#### Rukhlis
Mates against defenses `a` and `b` change in the key to `C` and `D`, while the original mates `A` and `B` are transferred to defenses `c` and `d`:

```thema
vir [A B _ _]
key [C D A B]
```

Here `vir` matches virtual play (Set Play or Try), and `A`, `B`, `C`, `D` are pairwise distinct checkmates across the four defense columns.

---

### Lesson 5: Threat Separation & Try Refutations (Barnes & Cyclic)

#### Barnes Theme
One phase carries a double threat `(AB)`, which is separated into individual single threats `(A)` and `(B)` in two other phases:

```thema
any (AB)
any (A)
any (B)
```

`(AB)` matches a phase with two threats, while `(A)` and `(B)` match phases with those individual single threats. When a row only constrains the phase move or threat, the variation brackets `[...]` can be omitted.

#### Cyclic Refutations
Try 1 is refuted by `a` and `b`. Try 2 is refuted by `b` and `c`. Try 3 is refuted by `c` and `a`:

```thema
try [! ! _]
try [_ ! !]
try [! _ !]
```

Because each try row contains two `!` markers, the try-quality filter automatically permits tries with two refutations.

---

### Lesson 6: Sets, Order-Invariance, and Symmetries

When testing piece roles or squares across multiple columns, checking `a.role == 'R' && b.role == 'B'` artificially ties the condition to whichever column happens to be bound to `a`. Using set comparisons makes the check order-invariant:

```thema
// Check that defenses are made by a Knight and a Bishop in any order:
{a.role, b.role} == {'N', 'B'}

// Check that 3 moves land on distinct squares:
count_distinct(A.to, B.to, C.to) == 3

// Check that defense destination belongs to a set of flight squares:
a.to in {up(BK), down(BK), left(BK), right(BK)}
```

---

### Lesson 7: Why Doesn't My Spec Match? (Implicit Rules & the Debugger)

Most "my spec doesn't match" surprises come from rules that are **implied by the matrix** rather than written down. Learn these first:

| You write | Thema silently requires |
|---|---|
| `(A)` (one threat variable) | the phase has **exactly 1** threat |
| `(AB)` (multi-variable) | the phase has **exactly 2** threats |
| a single `!` in a `try` row | the try has **exactly 1** refutation |
| a single variable in a cell, e.g. `[A _]` | that defense has a **unique** mate (no duals) |
| different names `A`, `B` (or `a`, `b`) | they bind **different** moves / defense columns |
| `a`, `b`, … without a `def` row | defense columns are bound implicitly, in order |
| any `try` row | **try-quality filters** discard "cheap" tries first (refutation captures the try piece, checking refutation, …) |
| `_` | anything, including a refutation or an empty cell (the only wildcard) |

Use `with` to relax a rule on purpose (e.g. `with -single_refutation`, `with permissive`), never by adding ad-hoc `where` clauses.

**Worked example: the Afek Dombrovskis** (`2N5/1n1NBBp1/rRn1Pp2/p3PkPP/p5R1/2p1KP2/2P5/1Q6 w - - 0 1`, *Load on Board* from the Studio guide). The correct spec

```thema
try (A) [! _]
try (B) [_ !]
key [A B]
```

matches with `A = Rf4#`, `B = Bg6#`, `a = fxe5`, `b = Nxe5`. Of the 8 tries in the position, the debugger's *Try Quality* stage shows only **2 eligible** (`1.Qg1?` threatening `Rf4#`, refuted by `fxe5`; `1.Qa2?` threatening `Bg6#`, refuted by `Nxe5`). The other 6 are filtered: `1.Bxf6?`, `1.Rxc6?`, `1.Qb4?` (refutation captures the try piece), `1.Qd1?`, `1.Qf1?` (two refutations), and `1.Qb3?` (both reasons).

Now break it on purpose and watch which debugger stage reports it:

```thema
// 1. Matrix fails at row 0: no *eligible* try has exactly 2 threats with 1 refutation
//    (1.Qb4? has two threats, but its refutation 1...axb4 captures the try piece)
try (AB) [! _]
try (B) [_ !]
key [A B]

// 2. Matrix fails at row 2: column order matters; after the key, 1...fxe5 is met by Rf4# (= A), not B
try (A) [! _]
try (B) [_ !]
key [B A]

// 3. Matrix locks, but the where clause fails: A = Rf4# is a rook move, not a queen move
try (A) [! _]
try (B) [_ !]
key [A B]
where A.role == "Q"
```

**Reading the debugger (in the Theme Editor tab):**
1. **Stage 1 (dimensions):** does the position have enough defense columns and eligible try rows at all?
2. **Stage 2 (matrix lock, ignoring `where`):** reports the first pattern row (0-based) that could not lock onto a phase. Check the implicit counts above.
3. **Stage 3 (`where` waterfall):** each clause is shown *Solo* (alone) and *Chain* (together with all previous clauses). The first red *Chain* is the clause that rejects the match.
4. **Stage 4 (try quality):** every try with the reason it was filtered. If the try you expected is filtered, decide whether the theme really allows it, then relax that rule explicitly with `with`.

---

## 4. Language Reference

### Formal Grammar (EBNF)

```ebnf
Comment        ::= '//' .* '\n'         (* stripped before parsing *)
Specification  ::= Branch (('---' | 'or') '\n' Branch)*
Branch         ::= MatrixSection SectionClause*
SectionClause  ::= ('where' WhereClause) | ('with' WithClause) | ('subsumes' SubsumesClause) | (('story' | 'format') StoryClause)
MatrixSection  ::= Row (('|' | '\n') Row)*
Row            ::= ('+' | '^')* RowType MoveToken? ('(' ThreatToken ')')? ('[' Cell* ']')?
RowType        ::= 'key' | 'try' | 'set' | 'vir' | 'any' | 'def'

MoveToken      ::= '_' | Cell
ThreatToken    ::= '_' | Cell
Cell           ::= '_' | '-' | '!'     (* '_' is the ONLY wildcard; '.' and bare '?' are rejected *)
                 | (VarIdent | MultiVarIdent)? ('?' | '*')? ('~' VarIdent)? (':' CellAnnot)? ('!'? '@' TargetSpec)? ('?' | '*')?
                 | '!' VarIdent (':' CellAnnot)? ('!'? '@' TargetSpec)?   (* negated cell: any move except VarIdent *)
TargetSpec     ::= VarIdent ('.' ('from' | 'to'))?
CellAnnot      ::= RoleUnion ('x' | '+')* | ('x' | '+')+ | '=' '!'? RoleUnion? | '!='
RoleUnion      ::= [PNBRQKS] ('|' [PNBRQKS])*
VarIdent       ::= [A-Za-z][A-Za-z0-9_]*
MultiVarIdent  ::= [A-Z]{2,4}

WhereClause    ::= OrExpr (',' OrExpr)*
OrExpr         ::= AndExpr ('||' AndExpr)*
AndExpr        ::= CmpExpr ('&&' CmpExpr)*
CmpExpr        ::= AddExpr ((CmpOp AddExpr)+ | 'in' SetLiteral)?
CmpOp          ::= '==' | '!=' | '<' | '<=' | '>' | '>='
AddExpr        ::= UnaryExpr (('+' | '-') UnaryExpr)*
UnaryExpr      ::= ('!' | 'not') UnaryExpr | PostfixExpr
PostfixExpr    ::= Primary ('.' Ident ('(' (OrExpr (',' OrExpr)*)? ')')?)*
Primary        ::= Ident | IntLiteral | StringLiteral | BoolLiteral 
                 | SetLiteral | TupleExpr | FuncCall | QuantifierExpr | '(' OrExpr ')'

TupleExpr      ::= '(' OrExpr (',' OrExpr)+ ')'
SetLiteral     ::= '{' (OrExpr (',' OrExpr)*)? '}'
FuncCall       ::= Ident '(' (OrExpr (',' OrExpr)*)? ')'
QuantifierExpr ::= QuantifierName '(' SetLiteral ',' LambdaExpr ')'
QuantifierName ::= 'all' | 'any' | 'none' | 'same' | 'distinct' | 'count'
LambdaExpr     ::= Ident '=>' OrExpr

WithClause     ::= PresetIdent? DeltaModifier*
PresetIdent    ::= 'strict' | 'permissive' | 'relaxed' | 'default'
DeltaModifier  ::= ('+' | '-') RuleIdent
RuleIdent      ::= 'capture_try_piece' | 'check_refutations' | 'flight_from_check'
                 | 'sparse_replies' | 'sparse_zugzwang' | 'single_refutation'
                 | 'single_threat' | 'unique_mate' | 'distinct_mates'
                 | ('min_replies_' | 'min_defenses_' | 'sparse_replies_' | 'replies_' | 'defenses_') [1-5]

StoryClause    ::= StringLiteral | TemplateText
```

---

### Matrix Grid & Phase Rows

Each row defines a phase vector in the chess solution table using the syntax:
```text
<RowType> <PhaseMove>? (<Threat>)? [ <VariationMates...> ]
```

| Keyword | Row Type | Matches | Eligible Rows |
|---|---|---|---|
| `key` | **Key** | The real solution (Key move + variations) | Exactly row 1 |
| `try` | **Try** | A deceptive White try refuted by Black | Rows 2..N (filtered by try quality) |
| `set` | **Set Play** | Play existing in the initial position before key | Row 0 |
| `vir` | **Virtual Play (Set or Try)** | Play in a virtual phase (Set Play or Try, excluding Key) | Rows 0, 2..N |
| `any` | **Any Phase** | Can bind to Set Play, Key, or any Try | Any available row |
| `def` | **Defense Header** | Specifies Black defense variables | Maps columns 2..N to Black moves |

Row types are mutually exclusive. Two row-level prefix modifiers can optionally precede any row type:
- `+` (**No Line Reset**): Disables automatic cross-row variable distinctness so distinct variable names on different rows may bind to the same move unless constrained in `where`, while still enforcing distinctness within the same row (e.g. `+try [...]`, `+any [...]`).
- `^` (**Orthogonal Matrix Distinctness / Column-Scoped Distinctness**): Enforces variable distinctness **within the same row AND within the same vertical defense column**, while allowing variables in diagonally opposite cells (different row AND different column) to coincide unless constrained in `where`. For example, in `Zagoruiko`:
  ```thema
  ^vir [A B]
  ^try [C D]
  ^key [E F]
  where count_distinct(A, B, C, D, E, F) >= 5
  ```
  Each defense column changes its mate across all 3 phases (`A != C != E` and `B != D != F`), each phase has distinct mates (`A != B`, `C != D`, `E != F`), and at most one diagonal cross-column pair may coincide—replacing 5 separate combinatorial specs with a single 4-line matrix!

#### Multi-Branch Specifications (`---` / `or` Blocks)
Many chess composition themes manifest in several structural forms (e.g., key vs try vs variation mate, or 2-defense vs 3-defense forms). A single Thema specification can declare multiple branches separated by `---` (or `or` on its own line):
```thema
key K:=!Q
story "Underpromotion: Key 1.{K}! promotes to a {K.promotion}."
---
any [A:=!Q]
story "Underpromotion: 1...{a} is answered by 2.{A}#."
---
def [a:=!Q]
any [A]
story "Underpromotion: Black defense 1...{a} underpromotes, met by 2.{A}#."
```
- Each branch has its own matrix, `where`, `with`, and `story` clauses, and is compiled into its own `PartitionedSlices` bytecode slice set.
- If earlier branches omit `subsumes` or `story`, they automatically inherit `subsumes` and `story` from the final branch.

Rows can be separated by either newlines or pipe characters (`|`) outside brackets:
```thema
try T [A] | key K [B]
```

#### Explicit Phase Header `phase Move? (Threat?)` & Variation `[Mates...]` Brackets
In Thema, the phase's first move and threat are placed outside the brackets `[...]`, so that `[...]` contains strictly defensive variation columns `1..N`:
- `try (A) [! _]` — Try with threat `A`, refuted by defense 1 (`!`).
- `key [A B]` — Key answering defenses `a` and `b` with mates `A` and `B`.
- `any (AB)` — Any phase with double threat `AB` (brackets are omitted when no variation columns are referenced).
- `try A (B)` / `key B (A)` — Threat Reversal: try move `A` threatens `B`, key move `B` threatens `A`.
- `key K:+` — Checking key move `K` (header-only phase row).
- `def [a b c]` — Black defense columns `a`, `b`, `c`. When using standard defense names `a..h` without inline cell annotations, the `def` row may be omitted entirely.

---

### Cell Identifiers, Conventions, Inline Annotations & Shorthands

Cells inside brackets `[...]` represent variation replies against Black defenses `a, b, c, ...` (separated by whitespace):

```
<RowType>  <Move>?  (<Threat>)?  [  Var_a   Var_b   ...   Var_n  ]
              │         │             │       │             │
              │         │             └───────┴─────────────┴─ Defense variation columns
              │         │                                      (Col 1 = Def a, Col 2 = Def b, etc.)
              │         └─ Parenthesized Threat move(s) — e.g. (A), (AB), (X?)
              └─ Phase first move (Key or Try move; omit when unused)
```

| Cell Token | Meaning | Example |
|---|---|---|
| `_` | **Wildcard** (the one and only wildcard symbol): any move, refutation, or empty slot. `.` and a bare `?` are **rejected** by the parser (`?` is only valid as an optional-variable suffix, e.g. `X?`) | `key [A _]` |
| `-` | **Blank**: Must be blank / unprovided (no mate exists) | `try [-]` |
| `!` | **Refutation**: Must be a refutation of this try | `try (A) [! _]` |
| `A`, `K`, `X` | **Single Move Variable**: Binds_one move (implicitly distinct from other single move variables in the same row) | `key K (X) [A]` |
| `A*`, `B*`, `*` | **Non-Exclusive Move Variable**: Binds one move without enforcing same-row distinctness against other move variables (allows shared mates across columns while keeping distinct variable names; combine with `count_distinct(A, B, ...) >= k`) | `any [A* B* C* D*]` |
| `X?`, `th?` | **Optional Move Variable**: Binds move if present; does not fail if slot is empty (e.g. zugzwang) | `key K (X?) [A]` |
| `!X` | **Negated Cell**: "some move here that is **not** `X`". Each occurrence binds its own fresh anonymous, non-exclusive variable (it never takes part in automatic distinctness) constrained by `fresh != X`; the cell must still contain a move (not empty / refutation). `X` must be bound somewhere in the matrix. Cannot be combined with `?` or `*`; may carry `:Role` / `@target` modifiers. Not to be confused with the bare refutation marker `!` | `vir [A !A]`, `+key (A) [!A !A]` |
| `AB`, `XYZ`, `ABCD:N` | **Multi-Move Variable**: Binds multiple moves in a cell; inline modifiers (`:Role`, `:x`, `:+`, `:=`, `*`, `@target`, `~target`) apply to every component variable | `any (AB)`, `key (ABCD:N)` |
| `var:Role` / `var:!Role` | **Inline Role Constraint**: Requires `var.role` to match (`:R`, `:k`) or exclude (`:!K`) role or `\|`-separated roles (`P`/`p`, `N`/`n`/`S`/`s`, `B`/`b`, `R`/`r`, `Q`/`q`, `K`/`k`; case-insensitive) | `def [a:N b:B c:R\|Q d:!K]`, `def [a:k b:k]` |
| `var:x` / `var:!x` / `var:+` / `var:!+` | **Inline Capture / Check Constraint**: Requires or forbids capture (`:x` / `:!x`) and check (`:+` / `:!+`); combinable with roles | `def [a:x b:Nx c:+ d:!x]` |
| `var:=` / `var:!=` / `var:=Role` / `var:=!Role` | **Inline Promotion Constraint**: Requires or forbids pawn promotion (`:=` / `:!=`), promotion to specific role(s) (`:=Q`, `:=N\|B\|R`), or underpromotion (`:=!Q`) | `key [A:=!Q B:=]`, `def [a:= b:=]` |
| `~Target` / `A~Target` | **Inline Switchback Shorthand**: Asserts `A.from == Target.to && A.to == Target.from` | `key K [~K]`, `key K (~K)` |
| `M@target` / `@target` | **Inline Target Square Shorthand**: Asserts `M.to == target.to` (or `M.to == target.from` when `@target.from` is written) | `key [@a.from @b.from]`, `def [a:x@K b:x@K]` |
| `M!@target` / `!@target` | **Inline Non-Target Square Shorthand**: Asserts `M.to != target.to` (e.g. non-capturing mate on a self-blocked flight) | `key [A!@a B@b]` |
| `[:Role]` / `[@target]` / `[*]` | **Anonymous Constrained Cell**: Any cell with a modifier (`:`, `@`, `!@`, `~`, `*`) and no explicit variable prefix automatically binds the next unused canonical variable for its slot (`a..h` in `def`, `K/T` in move slot, `X..W` in threat slot, `A..H` in variation slots) | `key [@a.from @b.from]`, `key [:K]` |

**Inline Cell Shorthand Examples**:
```thema
// Switchback: key piece returns to its departure square to mate
key K [~K]

// Umnov: mates land on the squares just vacated by Black's defenses
key [A@a.from B@b.from]

// Novotny: two unlike sliders capture on the key's arrival square (@K)
def [a:x@K b:x@K]
key K [A B]
where unlike_sliders(a, b), a.blocks(b, A), b.blocks(a, B)

// Hannelius: try moves are recaptured by Black's refuting defenses
def [a:x@A b:x@B]
try A [! _]
try B [_ !]
key [B A]
```

---

### Variables & Binding Scopes

- **White Moves**: Identified by uppercase names (`A`, `B`, `K`, `T`, `M1`).
- **Black Defenses**: Identified by lowercase names (`a`, `b`, `c`, `d`).
- **Implicit Defenses**: If no `def` header row is present, columns 2..9 are **automatically and implicitly mapped** as variables `a`, `b`, `c`, `d`, `e`, `f`, `g`, `h`. You can reference `a` or `b` in the `where` clause without declaring `def [a b]`.

Variable uniqueness: Distinct variable names of the same kind (e.g. `A` and `B`, or `a` and `b`) **cannot bind to the same move** unless explicitly permitted.

---

### Comma-Separated `where` Clauses, Chained Comparisons & Tuple Broadcasting

Thema provides ergonomic syntax in `where` clauses to eliminate repetitive `&&` chains:

1. **Comma-Separated `where` Clauses**: Top-level commas `,` in a `where` clause act as logical conjunction (`&&`), allowing clean, checklist-style constraints:
   ```thema
   where same_square(a, b),
     unlike_sliders(a, b),
     !(a, b).is_capture,
     blocks_ray(a.to, b.from, A.to),
     blocks_ray(b.to, a.from, B.to)
   ```

2. **Chained Comparisons (`==`, `!=`, `<`, `<=`, `>`, `>=`)**:
   - `a.to == b.to == c.to` desugars to `a.to == b.to && b.to == c.to`.
   - **Pairwise All-Different (`!=` chain)**: `A != B != C != D` means **all pairwise distinct** (`count_distinct(A, B, C, D) == 4`), matching mathematical notation.

3. **Direct `distinct(...)` (or `all_different(...)` / `all_distinct(...)`) and `same(...)`**:
   - `distinct(A, B, C, D)` (also accepted as `all_different(A, B, C, D)` or `all_distinct(A, B, C, D)`) desugars to `count_distinct(A, B, C, D) == 4` (with automatic early-pruning in the bytecode compiler).
   - `same(a.to, b.to, c.to)` desugars to `a.to == b.to && b.to == c.to`.

4. **Tuple Broadcasting & Multi-Argument Unary Predicates**:
   - **Property & Boolean Broadcasting on Tuples `(v1, v2, ...)`**:
     - `(a, b, c, d).role == 'N'` $\equiv$ `a.role == 'N' && b.role == 'N' && c.role == 'N' && d.role == 'N'`
     - `(a, b).role in {'R', 'Q'}` $\equiv$ `a.role in {'R', 'Q'} && b.role in {'R', 'Q'}`
     - `(a, b).is_capture` $\equiv$ `a.is_capture && b.is_capture`
     - `!(a, b).is_capture` $\equiv$ `!a.is_capture && !b.is_capture`
   - **Multi-Argument Unary Predicates**: Any unary predicate (`self_block`, `was_flight`, `fires_battery`, `is_sacrifice`, `creates_pin`, `is_double_check`, `is_discovered_check`, `is_Linear`, etc.) accepts multiple arguments and broadcasts over all of them:
     - `self_block(a, b, c, d)` $\equiv$ `self_block(a) && self_block(b) && self_block(c) && self_block(d)`
     - `was_flight(a, b, c)` $\equiv$ `was_flight(a) && was_flight(b) && was_flight(c)`

5. **Chess-Domain Shorthands**:
   | Shorthand | Desugars To | Meaning |
   |---|---|---|
   | `recaptures(A, a)` / `captures_on(A, a)` | `A.to == a.to` | Move `A` captures/lands on the arrival square of `a` |
   | `same_square(a, b, ...)` | `a.to == b.to && ...` | All moves land on the same destination square |
   | `diff_square(a, b, ...)` | `distinct(a.to, b.to, ...)` | All moves land on pairwise distinct destination squares |
   | `same_piece(a, b, ...)` | `a.from == b.from && ...` | Moves in the same phase originate from the same piece/square |
   | `diff_piece(a, b, ...)` | `distinct(a.from, b.from, ...)` | Moves originate from pairwise distinct departure squares |
   | `flight_block(a, ...)` | `distance(a.to, BK) == 1 && ...` | Defense lands on a square adjacent to the Black King |
   | `ortho_slider(m, ...)` | `m.role in {'R', 'Q'} && ...` | Piece is an orthogonal slider (Rook or Queen) |
   | `diag_slider(m, ...)` | `m.role in {'B', 'Q'} && ...` | Piece is a diagonal slider (Bishop or Queen) |
   | `slider(m, ...)` | `m.role in {'R', 'B', 'Q'} && ...` | Piece is a line-piece (Rook, Bishop, or Queen) |
   | `leaper(m, ...)` | `m.role in {'N', 'K', 'P'} && ...` | Piece is a non-slider |
   | `ortho(m, ...)` | `m.ortho && ...` | Move trajectory is orthogonal (along a file or rank) |
   | `diag(m, ...)` | `m.diag && ...` | Move trajectory is diagonal ($\|\Delta f\| = \|\Delta r\| > 0$) |
   | `cross_dirs(m1, m2, ...)` | `(m1, m2, ...).ortho && distinct(m1.dir, m2.dir, ...)` | Moves travel along distinct orthogonal compass rays (up to 4: N, S, E, W) |
   | `star_dirs(m1, m2, ...)` | `(m1, m2, ...).diag && distinct(m1.dir, m2.dir, ...)` | Moves travel along distinct diagonal compass rays (up to 4: NE, NW, SE, SW) |
   | `bristol(m1, m2)` / `clears_line(m1, m2)` | `m1.clears_line_for(m2)` | Move `m1` clears a line and `m2` traverses across `m1.from` along that same line |
   | `mutual_obstruction(a, b, A, B)` / `mutually_blocks(a, b, A, B)` | `same_square(a, b) && a.from != b.from && a.blocks(b, A) && b.blocks(a, B)` | Defenses `a` and `b` converge on the same square from distinct origins and mutually block each other's rays to `A.to` and `B.to` |
   | `pawn_quartet(m1, m2, m3, m4)` / `pawn_cross(m1, m2, m3, m4)` | `same_piece(m1, m2, m3, m4) && (m1, m2, m3, m4).role == 'P' && m1.one_step && m2.two_step && m3.left_capture && m4.right_capture` | A single White or Black pawn executes all 4 canonical pawn moves (1-step push, 2-step push, left capture, right capture) |
   | `corrects(b, a)` | `b.corrects(a)` | Black defense `b` is a correction move of the same piece as random move `a` (`same_piece(a, b) && a.to != b.to && a.role != 'K' && a.role != 'P'`) |
   | `underpromotion(m, ...)` | `m.is_promotion && m.promotion != 'Q'` | Pawn promotes to a non-Queen piece (Knight, Bishop, or Rook) |
   | `like_sliders(a, b)` | `(ortho(a) && ortho(b)) \|\| (diag(a) && diag(b))` | Both pieces share the same sliding geometry (Plachutta / Holzhausen) |
   | `unlike_sliders(a, b)` / `grimshaw_pair(a, b)` | `(a.role == 'R' && b.role in {'B', 'Q'}) \|\| ...` | Orthogonal slider vs diagonal slider (Grimshaw / Novotny) |

---

### Unified Move Properties & Relational Methods

Every move variable supports both attribute properties (`m.from`, `m.to`, `m.role`) and unary/relational chess predicates directly via dot syntax (`m.property` or `m.method(...)`), including on tuples `(a, b, c, d).self_block`:

#### Core Move Properties
| Property | Return Type | Description |
|---|---|---|
| `m.from` | Square | Square departed from |
| `m.to` | Square | Square arrived at |
| `m.role` | Role | Moving piece role (`'P'`, `'N'`, `'B'`, `'R'`, `'Q'`, `'K'`) |
| `m.capture` / `m.is_capture` | bool | Whether the move captures an opposing piece |
| `m.check` / `m.is_check` | bool | Whether the move gives check |
| `m.ep` / `m.is_ep` | bool | Whether the move is an en passant capture |
| `m.castling` / `m.is_castling`| bool | Whether the move is castling |
| `m.is_kingside_castling` | bool | O-O kingside castling |
| `m.is_queenside_castling`| bool | O-O-O queenside castling |
| `m.promotion` / `m.is_promotion` | bool / Role | Whether the pawn promotes (or promoted role when compared against a Role literal) |
| `m.underpromotion` / `m.is_underpromotion` | bool | Whether the move is an underpromotion (`m.is_promotion && m.promotion != 'Q'`) |
| `m.dir` / `m.direction` | int | Compass step direction of trajectory (`1`=N, `2`=S, `3`=E, `4`=W, `5`=NE, `6`=NW, `7`=SE, `8`=SW, `0`=knight/non-linear) |
| `m.north`, `m.south`, `m.east`, `m.west` | bool | True if move trajectory is strictly North (`dir == 1`, alias `.up`), South (`dir == 2`, alias `.down`), East (`dir == 3`, alias `.right`), or West (`dir == 4`, alias `.left`) |
| `m.ne`, `m.nw`, `m.se`, `m.sw` | bool | True if move trajectory is strictly North-East (`dir == 5`, aliases `.north_east`, `.right_up`), North-West (`dir == 6`, aliases `.north_west`, `.left_up`), South-East (`dir == 7`, aliases `.south_east`, `.right_down`), or South-West (`dir == 8`, aliases `.south_west`, `.left_down`) |
| `m.along_file` / `m.vertical` | bool | True if `m.from.file == m.to.file` (move stays on the same file) |
| `m.along_rank` / `m.horizontal` | bool | True if `m.from.rank == m.to.rank` (move stays on the same rank) |
| `m.ortho` / `m.is_ortho` | bool | True if move trajectory is orthogonal (along a file or rank) |
| `m.diag` / `m.is_diag` | bool | True if move trajectory is diagonal ($\|\Delta f\| = \|\Delta r\| > 0$) |
| `m.corner` / `m.is_corner` | bool | True if `m.from` or `m.to` is one of the 4 board corners (`CORNERS`) |
| `m.corner_to_corner` | bool | True if `m` moves from one board corner to another distinct board corner |
| `m.one_step` | bool | True if pawn `m` advances 1 rank straight ahead (direction-aware: `+1` rank for White uppercase variables, `-1` rank for Black lowercase variables) |
| `m.two_step` / `m.double_step` | bool | True if pawn `m` advances 2 ranks straight ahead (`+2` ranks for White, `-2` ranks for Black) |
| `m.left_capture` | bool | True if pawn `m` captures 1 step diagonally to the left (`left_up` for White, `left_down` for Black) |
| `m.right_capture` | bool | True if pawn `m` captures 1 step diagonally to the right (`right_up` for White, `right_down` for Black) |

#### Tactical & Mate Quality Dot-Properties (Usable on Single Moves or Tuples `(a, b, c).prop`)
| Dot-Property | Equivalent Function | Description |
|---|---|---|
| `m.self_block` | `self_block(m)` | Black defense blocks a King flight square |
| `m.flight_block` | `distance(m.to, BK) == 1` | Move lands adjacent to the Black King |
| `m.was_flight` | `was_flight(m)` | Mate lands on a square that was previously a King flight |
| `m.fires_battery` | `fires_battery(m)` | Move fires a discovered check/mate from a battery |
| `m.battery_rear` | `battery_rear(m)` | Square of the rear piece of the battery fired by `m` (or of a pre-move direct battery on `start` for phase moves) |
| `m.battery_front` | `battery_front(m)` | Square of the front piece of a pre-move direct battery on `start` (or `m.from` when `m` fires a battery or indirect battery) |
| `m.self_pins` | `self_pins(m)` | Defense moves an unpinned piece onto a pin line |
| `m.self_pins_piece` | `self_pins_piece(m)` | Moving piece itself becomes pinned to its King |
| `m.sacrifice` / `m.active_sacrifice` | `is_sacrifice(m)` / `is_active_sacrifice(m)` | Move places the piece en prise to capture |
| `m.passive_sacrifice` / `m.is_passive_sacrifice` | `is_passive_sacrifice(m)` | Move unguards a friendly piece, leaving it en prise |
| `m.anti_bristol` / `m.is_anti_bristol` | `is_anti_bristol(m)` | Move travels along a line toward a friendly slider, obstructing its line |
| `m.half_pin` / `m.is_half_pin` | `is_half_pin(m)` | Move leaves or exploits a Black half-pin line (`K.half_pin` or `BK.half_pin` checks the post-key position) |
| `m.white_half_pin` / `m.is_white_half_pin` | `is_white_half_pin(m)` | Move leaves or exploits a White half-pin line (`K.white_half_pin` or `WK.white_half_pin` checks the post-key position) |
| `m.white_interferences` / `m.white_interferences_count` | `white_interferences_count(m)` | Number of White self-interferences caused by move `m` (`K.white_interferences` checks the key) |
| `m.mating_origins` / `m.mating_origins_count` | `mating_origins_count()` | Number of distinct White piece origins delivering mate across variations (`K.mating_origins`) |
| `m.pinned_before` / `m.is_pinned_before` | `is_pinned(m.from, before(m))` | Moving piece on `m.from` was pinned immediately before move `m` |
| `m.pinned_after` / `m.is_pinned_after` | `is_pinned(m.to, after(m))` | Moving piece on `m.to` is pinned immediately after move `m` |
| `m.flights_given` | `flights_given(m)` | Number of new flight squares granted to BK by `m` (`K.flights_given` also works without binding `K`) |
| `m.flights_taken` | `flights_taken(m)` | Number of flight squares taken from BK by `m` (`K.flights_taken` also works without binding `K`) |
| `m.threat_count` / `m.threats` | `threat_count(m)` | Number of threats introduced by phase move `m` (`K.threat_count` also works without binding `K` in the matrix) |
| `m.refutation_count` / `m.refutations` | `refutation_count(m)` | Number of refutations against try move `m` |
| `m.mate_count` / `m.mates` | `mate_count(m)` | Number of checkmates in the variation cell of mate `m` |
| `m.pure` / `m.is_pure` | `is_pure(m)` | True if variation mate `m` is the unique mate in its cell (`m.mate_count == 1`) |
| `m.waiting` / `m.is_waiting` | `!m.check && m.threat_count == 0` | True if phase move `m` is a non-checking waiting move with zero threats |
| `m.pure_mate` | `is_pure_mate(m)` | Mate is a pure mate |
| `m.model_mate` | `is_model_mate(m)` | Mate is a model mate (pure + economical) |
| `m.ideal_mate` | `is_ideal_mate(m)` | Mate is an ideal mate (all pieces on board participate) |
| `m.mirror_mate` | `is_mirror_mate(m)` | Mate leaves all 8 squares around BK unoccupied |
| `m.smothered_mate` | `is_smothered_mate(m)` | Knight mate against a King surrounded by friendly pieces |
| `m.epaulette_mate` | `is_epaulette_mate(m)` | Mate with BK flanked by two parallel friendly pieces |
| `m.pin_mate` | `is_pin_mate(m)` | Mate relies on a pinned Black defender |
| `m.double_pin` | `is_double_pin(m)` | Move exploits or creates a double pin (`K.double_pin` also works without binding `K`) |
| `m.creates_half_pin` | `creates_half_pin(m)` | Move establishes a half-pin line (`K.creates_half_pin` also works without binding `K`) |
| `m.double_check` | `is_double_check(m)` | Move delivers double check |
| `m.interferes` | `interferes(m)` | Move closes the line of a friendly slider |
| `m.ortho_slider` | `m.role in {'R', 'Q'}` | Piece is a Rook or Queen |
| `m.diag_slider` | `m.role in {'B', 'Q'}` | Piece is a Bishop or Queen |
| `m.slider` | `m.role in {'R', 'B', 'Q'}` | Piece is a line-piece |
| `m.leaper` | `m.role in {'N', 'K', 'P'}` | Piece is a non-slider |

#### Relational Move Methods (`m.method(...)`)
| Method Call | Desugars To | Meaning |
|---|---|---|
| `a.blocks(b, A)` / `a.blocks_line(b, A)` | `blocks_ray(a.to, b.from, A.to)` | Defense `a` blocks the ray of piece `b` toward mate `A`'s square (evaluated on `start` for Set-play patterns or `after_key` for Key play) |
| `a.guards(sq_or_move)` / `a.attacks(sq_or_move)` | `guards(a, target_sq)` / `attacks(a.to, target_sq)` | Piece after move `a` guards/attacks `target_sq` (or `.to` of move arg) |
| `A.recaptures(a)` / `A.captures_on(a)` | `A.to == a.to` | Move `A` captures/lands on `a`'s arrival square |
| `A.umnov(a)` | `A.to == a.from` | Move `A` lands on the square vacated by `a` (Umnov effect) |
| `A.switchback(K)` | `A.from == K.to && A.to == K.from` | Move `A` returns piece `K` to its origin square |
| `a.unguards(B)` | `unguards(a, B.to)` | Move `a` abandons non-King guard of `B.to` (or square arg), including squares adjacent to `BK` |
| `a.unpins(A \| BK \| WK)` | `unpins(a, A.from \| BK \| WK)` | Move `a` unpins piece `A` (coerced to `A.from`) or any piece pinned to `BK`/`WK` |
| `X.unpins_piece(a)` | `unpins_piece(X, a.to)` | Move `X` unpins the piece on `a.to` |
| `a.interferes_with('B')` | `interferes_with(a, 'B')` | Move `a` interferes with a friendly piece of given role (excluding the moving side's own King square) |
| `K.cuts_enemy_line(['R'])` | `cuts_enemy_line(K, ['R'])` | Move `K` cuts an enemy slider line (excluding the enemy King's own square) |
| `a.cuts_line_to(A)` | `cuts_line_to(a, A.to)` | Move `a` cuts a line directed at `A.to` |
| `K.opens_line([sq])` / `K.closes_line([sq])` | `opens_line(K, ...)` | Move opens or closes a line of action (excluding the friendly King's own square) |
| `a.pins(A \| BK \| WK)` | `pins(a, A.from \| BK \| WK)` | Move `a` pins piece `A` (coerced to `A.from`) or establishes a pin against `BK`/`WK` |
| `a.pinned_to(BK \| WK)` / `sq.pinned_to(BK \| WK)` | `pinned_to(a.to \| sq, BK \| WK)` | Piece on `a.to` (or `sq`) is pinned to `BK`/`WK` (supports tuple broadcasting `(a, b, c).pinned_to(BK)`) |
| `a.obstructs(A)` | `obstructs_slider(a, A)` | Defense `a` obstructs a friendly slider to allow mate `A` |
| `A.echo(B)` / `A.chameleon_echo(B)` | `echo_mate(A, B)` / `chameleon_echo(A, B)` | Mates `A` and `B` form an echo (or opposite-colored chameleon echo) |
| `a.indirect_pins(BK)` | `indirect_pins(a, BK)` | Move `a` unmasks an indirect pin against `BK` |
| `K.anti_bristol(A)` | `is_anti_bristol(K, A)` | Move `K` moves along a line toward `A`, obstructing it |
| `m.crosses(sq_or_move)` | `between(target_sq, m.from, m.to)` | Move `m` strictly traverses over `target_sq` (defaults to `.to` if a move is passed) |
| `m.along(sq_or_move)` | `collinear(m.from, m.to, target_sq)` | Move `m` moves along the straight line passing through `target_sq` (defaults to `.from` if a move is passed) |
| `m1.clears_line_for(m2)` | `collinear(m1.from, m1.to, m2.from) && collinear(m2.from, m1.from, m2.to) && between(m1.from, m2.from, m2.to)` | Pure Bristol line clearance: `m1` vacates its line and `m2` traverses across `m1.from` along that exact line |
| `a.mutually_blocks(b, A, B)` | `same_square(a, b) && a.from != b.from && a.blocks(b, A) && b.blocks(a, B)` | Defenses `a` and `b` converge on the same square from distinct origins and mutually block each other's rays to `A.to` and `B.to` |
| `b.corrects(a)` | `corrects(b, a)` | Black defense `b` is a correction move of the same piece as random move `a` |
| `a.valve(A)` / `a.is_valve(A)` | `is_valve(a, A)` | Defense `a` simultaneously opens one line and closes another to allow mate `A` |
| `a.bivalve(A)` / `a.is_bivalve(A)` | `is_bivalve(a, A)` | Defense `a` simultaneously opens a friendly line and closes another to allow mate `A` |
| `a.anti_levman(A)` / `a.is_anti_levman(A)` | `is_anti_levman(a, A)` | Defense `a` unblocks or unpins a friendly piece along a line exploited by mate `A` |

---

### Square Properties & Special Identifiers

Properties on squares (`sq.property`):

| Property | Return Type | Range | Description |
|---|---|---|---|
| `sq.file` | int | `1..8` | File 1 = `a`, 2 = `b`, ..., 8 = `h` |
| `sq.rank` | int | `1..8` | Rank 1 = `1`, ..., 8 = `8` |
| `sq.corner` / `sq.is_corner` | bool | `bool` | True if `sq` is one of the 4 corner squares (`'a1'`, `'a8'`, `'h1'`, `'h8'`) |
| `sq.up`, `sq.down`, `sq.left`, `sq.right` | Square | `Square` | Adjacent square 1 step (or `sq.up(n)` for `n` steps) in the given orthogonal direction |
| `sq.left_up`, `sq.right_up`, `sq.left_down`, `sq.right_down` | Square | `Square` | Adjacent square 1 step (or `sq.left_up(n)` for `n` steps) in the given diagonal direction |
| `BK.flights` / `BK.king_flights` | int | `0..8` | Number of legal King flight moves available to `BK` after the key |
| `BK.y_flight` / `BK.is_y_flight` | bool | `bool` | True if `BK` has three flight moves forming a Y-shape pattern |
| `BK.half_pin` / `WK.white_half_pin` | bool | `bool` | True if a Black (or White) half-pin line is active against `BK` (or `WK`) |

Special Square & Set Identifiers:
- `WK`: White King square in current position
- `BK`: Black King square in current position
- `CORNERS`: Built-in set constant `{'a1', 'a8', 'h1', 'h8'}` usable in set comparisons (`{K.from, K.to, A.to, B.to} == CORNERS`) and membership tests (`K.to in CORNERS`)

Example:
```thema
where A.to.file == BK.file  // Mate delivers check along Black King's file
```

---

### Literals, Roles & Constants

- **Role Literals**: `'P'`, `'N'` (or `'S'`), `'B'`, `'R'`, `'Q'`, `'K'`, or keywords `pawn`, `knight`, `bishop`, `rook`, `queen`, `king`.
- **Square Literals**: Quoted algebraic coordinates: `"e4"`, `"d5"`, `"a1"`.
- **Integers**: Decimal numbers `0`, `1`, `2`, `8`.
- **Booleans**: `true`, `false`.

---

### Operators & Precedence

Precedence (highest to lowest):
1. Postfix access: `.`
2. Unary prefix: `!`, `not`
3. Multiplicative / Additive: `+`, `-`
4. Relational & Membership: `==`, `!=`, `<`, `<=`, `>`, `>=`, `in`
5. Logical Conjunction: `&&`
6. Logical Disjunction: `||`

---

### Set Expressions & Algebra

Thema has first-class mathematical set support. Sets in `where` clauses are defined with curly braces `{ ... }`:

```thema
// Role set membership
a.role in {'R', 'B'}

// Set equality (order-invariant)
{a.to, b.to} == {"d4", "e5"}

// Set subset (every element in left is in right)
{a.role, b.role} <= {'R', 'B', 'Q'}

// Set strict subset (left ⊂ right) and superset (left ⊇ right)
{a.role} < {'R', 'B'}

{a.role, b.role, c.role} >= {'R', 'B'}
```
---

### Quantifiers & Iteration

Quantifiers eliminate repetitive predicates over multiple variables. They take an explicit set of variables and a **lambda** (`x => expr`) that is applied to each element. Quantifiers are **desugared at parse time** into expanded boolean/comparison chains — zero runtime overhead.

**Syntax**: `quantifier({var1, var2, ...}, x => body)`

| Quantifier | Semantics | Returns |
|---|---|---|
| `all({set}, x => P(x))` | Every element satisfies `P` | `bool` |
| `any({set}, x => P(x))` | At least one element satisfies `P` | `bool` |
| `none({set}, x => P(x))` | Zero elements satisfy `P` | `bool` |
| `same({set}, x => f(x))` | All elements produce identical value for `f` | `bool` |
| `distinct({set}, x => f(x))` | All elements produce unique values for `f` | `bool` |
| `count({set}, x => P(x))` | Number of elements satisfying `P` | `int` |

**Desugaring equivalences**:
```
all({a, b, c}, x => P(x))      ≡  P(a) && P(b) && P(c)
any({a, b, c}, x => P(x))      ≡  P(a) || P(b) || P(c)
none({a, b, c}, x => P(x))     ≡  !P(a) && !P(b) && !P(c)
same({a, b, c}, x => f(x))     ≡  f(a) == f(b) && f(b) == f(c)
distinct({a, b, c}, x => f(x)) ≡  f(a) != f(b) && f(a) != f(c) && f(b) != f(c)
count({a, b, c}, x => P(x))    ≡  count(P(a), P(b), P(c))
```

The set is any explicit `{...}` of bound variables — white, black, or mixed. The lambda variable name is arbitrary.

**Examples**:
```thema
// All defenses are by the same Knight from the same square
where all({a, b, c, d}, x => x.role == 'N')
   && same({a, b, c, d}, x => x.from)
   && distinct({a, b, c, d}, x => x.to)

// At least 2 of 4 defenses are captures
where count({a, b, c, d}, x => x.is_capture) >= 2

// Grimshaw: both defenses arrive at same square, neither gives check
where same({a, b}, x => x.to)
   && none({a, b}, x => x.is_check)

// All mates land on corner squares
where all({A, B, C, D}, m => m.to in {'a1', 'a8', 'h1', 'h8'})
   && distinct({A, B, C, D}, m => m.to)

// Mixed white+black: all thematic moves are by the same piece type
where same({a, b, A, B}, x => x.role)
```

> **Note**: `count({set}, x => pred)` (quantifier form with lambda) is distinct from `count(cond1, cond2, ...)` (variadic boolean form). The parser distinguishes them by the presence of `=>` in the second argument.

---

### Aggregation Primitives (`count`, `count_distinct`)

#### `count_distinct(x1, x2, ...)` (or `len(...)`, `size(...)`)
Returns the number of unique elements among its arguments:
```thema
where count_distinct(A, B, C) == 3        // All 3 mates are distinct
where count_distinct(a.to, b.to) == 1     // Both defenses land on the same square
```

#### `count(cond1, cond2, ...)`
Evaluates how many boolean conditions are `true`:
```thema
where count(A.is_check, B.is_check, C.is_check) >= 2
```

---

### The `with` Clause (Per-Theme Quality Configuration)

By default, Thema enforces strict candidate quality filtering on tries, threats, and mates. The optional `with` clause allows specifications to override or relax quality filters on a per-theme basis.

The `with` clause is specified **after the `where` clause** (or directly after the matrix if no `where` clause is present).

#### Syntax
```text
with <preset>? (+rule | -rule)*
```

- **Presets**:
  - `strict` (or `default`): All 5 try weakness filters active, `single_refutation = true`, `single_threat = true`, `unique_mate = true`. Used when `with` is omitted.
  - `permissive` (or `all`): All quality filters disabled; all candidate tries, dual threats, and dual mates are permitted.
  - `relaxed`: Weakness filters active, but allows multi-refutations, dual threats, and dual mates.

- **Delta Modifiers**:
  - `+rule`: **Enforces** the quality filter / requires strict verification.
  - `-rule`: **Relaxes** the quality filter / allows exceptions (zero double negatives!).

#### Quality Rules & Identifiers

| Rule | Thema Identifier | `-rule` (Relax / Allow) | `+rule` (Enforce / Require) |
|---|---|---|---|
| Rule 1 | `sparse_replies` | Allow tries with 0 threats and $\le 2$ replies | Filter out tries with few replies |
| Rule 2 | `sparse_zugzwang` | Allow sparse zugzwang tries | Filter out sparse zugzwang tries |
| Rule 3 | `check_refutations` | Allow refutations giving check | Filter out checking refutations |
| Rule 4 | `flight_from_check` | Allow King flight refutations vs checking tries | Filter out checking tries refuted by flight |
| Rule 5 | `capture_try_piece` | **Allow Black capturing the moving try piece** | Filter out try-piece captures |
| Rule 6 | `single_refutation` | Allow multi-refutation tries | **Require exactly 1 distinct refutation** |
| Rule 7 | `single_threat` | Allow dual/triple threats | **Require exactly 1 threat for single variables** |
| Rule 8 | `unique_mate` | Allow dual mates | **Require unique checkmate per variation** |
| Threat-Defending Replies ($N \in 1..5$) | `min_replies_1` .. `min_replies_5` (aliases `min_defenses_1..5`, `sparse_replies_1..5`, `replies_1..5`, `defenses_1..5`) | `-min_replies_N` disables the minimum threshold (default when omitted is `0`, i.e. no extra filtering) | `+min_replies_N` (or bare `min_replies_N` / `+sparse_replies_N` / `-sparse_replies_N`): **Require Black to have at least $N$ distinct replies that defend against (parry or separate) the try's threat(s)** (including both mating variations and refutations) |
| Exclusivity | `distinct_mates` (alias `exclusive_mates`) | Allow distinct uppercase variables (`A`, `B`, `C`) in the same row to bind the same move | **Require distinct uppercase variables in the same row to bind distinct moves** |

*Aliases are supported for convenience: `capture_try`, `check_refutation`, `refutation_is_check`, `flight_escapes_check`, `sparse_mates`, `threat_matching`, `mate_matching`, `min_defenses_1..5`, `sparse_replies_1..5`, `replies_1..5`, `defenses_1..5`.*

#### Examples

```thema
// 1. Try sacrifice theme: Black refutes by capturing White's try piece
try T (A) [!]
key K [A]
where a.to == T.to
with strict -capture_try_piece

// 2. Cyclic refutations: permissive mode with strict single-threat verification
try [! ! _]
try [_ ! !]
try [! _ !]
with permissive +single_threat

// 3. Relax check refutations and King flights without repeating preset (defaults to strict)
key K [A]
try T [B]
with -check_refutations -flight_from_check
```

#### Multi-Threat Purity Semantics (Standing-Threat Exclusion & Cross-Row Threat Disjointness)

In a 1-threat phase `1.K! (threat 2.X#)`, any Black defense `1...a` that fails to parry `2.X#` produces `TableCell::Blank` (`-`), so every mate in `TableCell::Mates` is guaranteed to be a genuine contingent variation mate ($A \neq X$). By contrast, in a multi-threat phase `1.K! (threats 2.X#, 2.Y#)`, a Black defense `1...a` that parries `2.Y#` while leaving `2.X#` unparried places the standing threat `[2.X#]` into `TableCell::Mates` so threat-separation themes (`PrimaryThreat`: `key (AB) [A B]`, `ThreatSeparation`, `Zuk`) can inspect separated threats.

To prevent non-multi-threat table themes from treating unparried standing threats or overlapping multi-threat/multi-mate sets as changed/contingent mates, the Thema matcher (`mate2/src/pattern_dsl/matcher.rs`) enforces four structural purity invariants:
1. **Standing-Threat Exclusion in Defense Columns (`is_unparried_standing_threat`)**:
   When a locked table row `trow` has $\ge 2$ standing threats (`trow.threats.len() >= 2`), a defense-column mate variable `PatCell::Var(v) | PatCell::OptVar(v)` (`pcol >= 2`, when not explicitly bound in `prow`'s own threat cell `cell 1`) can **never** bind to an unparried standing threat of `trow` (regardless of how many defense columns leave that standing threat unparried), **except** when the defense captures the phase's first-move piece (`col.to == first_move.to`, such as a Novotny sacrifice `1.f3! Bxf3 / Rxf3` where capturing the sacrificed piece closes a line to separate the two threats).
2. **Cross-Row Single-Threat Disjointness (`conflicts_with_other_row_threats`)**:
   When two phase rows in a multi-phase pattern specify distinct exclusive single-threat variables `(A)` and `(B)`, neither row may bind a threat that already exists in the other row's standing threat set (`trow.threats`), and when both rows have $\ge 2$ standing threats (`prev_trow.threats.len() >= 2 && trow.threats.len() >= 2`), their threat sets must be disjoint (sharing neither UCI nor canonical mate SAN). Two phases sharing an overlapping multi-threat set (e.g. `{X, Y}` vs `{X, Z}`) cannot masquerade as a threat change by picking `A = Y` in row 1 and `B = Z` in row 2.
3. **Cross-Row Multi-Threat Non-Duplication (`multi_threat_conflicts_with_other_rows`)**:
   When a phase row specifies a `MultiVar` threat cell `(AB)` (e.g. `try (AB) / key [A B]`) and another locked phase row in the same pattern does not specify `(AB)`, the second row cannot contain the entire threat set `{A, B}` among its own standing threats.
4. **Multi-Phase Column Mate Purity (`conflicts_with_other_row_col_mates`)**:
   - *Same-column changed-mate purity*: When two phase rows specify distinct exclusive single-mate variables `[A]` and `[B]` (`A != B`) in the same defense column `pcol`, the two table cells cannot share any common mate move (preventing a dual addition `[A, B]` from matching as a changed mate `A -> B` when `-match_mate_count` is enabled).
   - *Cross-column transferred-mate purity*: When a mate variable `A` appears in `(pr, pcol)` and in a different column `pcol_other != pcol` of another row `pr_other` whose cell at `(pr_other, pcol)` is `_` (`PatCell::Wild`) or `-` (`PatCell::Blank`), `A` cannot match a mate that was already present in `(pr_other, pcol)` or in `pr_other`'s threats (matched by either UCI or canonical mate SAN `canonical_mate_san`).
   - *Blank-cell (`-`) removed-play purity*: When a mate variable `A` in `(pr, pcol)` is paired with `-` (`PatCell::Blank`) in the Key row `(pr_other, pcol)`, `A` is rejected if `A` still appears as a threat or variation mate in the Key row, or if `A` is still a legal checkmate after `(Key, pcol)` (where the cell was only `Blank` because the defense failed to parry the key's new threat).

---

### The `subsumes` Clause & Automatic Subsumption Hierarchy

When analyzing a chess problem against all 661 canonical themes, lower-order ("subset") themes inevitably co-occur whenever a higher-order ("superset") theme is present—for example:
- **Double Salazar** (`try A [C _] / try B [_ C] / key C [A B]`) always triggers **Salazar** (`try A [B] / key B [A]`) and **Changed Mate** (`try [A] / key [B]`).
- **Complete Lacny** (`vir [A B C] / try [B C A] / key [C A B]`) always triggers **Lacny** and **Zagoruiko**.
- **Soviet-French** (`try (A) [! _] / try (B) [_ !] / key K [A B] where K.flights_given > 0`) always triggers **Dombrovskis**, **Dombrovskis Paradox**, and **Flight-Giving Key**.
- **Brojt / Double-Decker Novotny** always triggers **Novotny**, **Grimshaw**, **Rook Sacrifice**, and **Active Sacrifice**.

To ensure only the highest-order (most specific) themes are reported while keeping the specification library future-proof, Thema includes a three-layer **Subsumption & Specificity Filtering Engine** (`mate2/src/pattern_dsl/subsumption.rs`):

1. **Automatic AST Homomorphism, Try-Quality Compatibility & Constraint Implication**:
   At startup, Thema's static analyzer (`pattern_implies(super_pat, sub_pat)`) searches over all injective row mappings (`try`/`set` $\implies$ `vir` $\implies$ `any`), column mappings, and variable homomorphisms, verifies `TryQualityConfig` compatibility (`match_threat_count`, `match_mate_count`, `require_single_refutation`, `skip_refutation_is_check`, `skip_refutation_escapes_check`, `skip_refutation_captures_try_piece`), and proves logical implication across `where` conjuncts (equality transitivity, distinctness preservation, role subset inclusion, square-set membership, and integer bounds). Any theme $A$ whose AST strictly embeds theme $B$ ($A \implies B \land B \not\implies A$) automatically subsumes $B$ with zero manual annotations.
2. **Corpus-Verified Declarative `subsumes` Clause (452 / 661 Themes, 949 Direct Hasse Edges / 1,459 Transitive Edges)**:
   Across all 661 canonical specifications in `mate2/src/pattern_dsl/specs.rs`, `subsumes` declarations are transitively reduced (Hasse diagram direct cover) and verified by combining **strict empirical superset verification** ($\text{Hits}(A) \subsetneq \text{Hits}(B)$, i.e. $P(B \mid A) = 1.0$ and $|A| < |B|$ across our 80,064-problem `#2` corpus) with **logical/predicate entailment**:
   ```thema
   def [a:R:x@K b:B:x@K c:R:!x d:B:!x]
   key K [A B C D]
   where same_square(c, d), c.to != K.to
   subsumes Novotny, Grimshaw, "Rook sacrifice"
   story "Brojt (Double-Decker Novotny): ..."
   ```
   The `subsumes` clause accepts comma-separated theme names, aliases, or `NamedTheme` identifiers (case-insensitive, quotes optional). Exact-equivalence alias pairs (19 symmetric pairs verified across the 80,064-problem corpus) are guarded in `is_duplicate_alias_pair` so the `SubsumptionGraph` is guaranteed to be a strict, cycle-free DAG.
3. **Transitive DAG Filtering & WASM Metadata**:
   - `detect_all_themes(fen, &table)` and `detect_all_dsl_specs(fen, &table)` filter raw matches through the precomputed transitive `SubsumptionGraph` DAG, returning only top-level themes not subsumed by any other detected theme.
   - `detect_all_themes_unfiltered(fen, &table)` and `detect_all_dsl_specs_unfiltered(fen, &table)` return all raw matches without subsumption filtering.
   - `analyze_dsl_json(fen)` includes `"subsumed": [...]` on each top-level theme object listing the lower-order themes folded into it on that position.

---

### The `story` / `format` Clause (Presentation & Dynamic Story Engine)

Thema is not only an analysis engine, but also an automated storyteller for chess compositions. In chess problem publications, databases, and interactive web dashboards, a dry list of matched variables is insufficient. Problemists and readers expect a narrative explaining the thematic mechanism (e.g. *"Grimshaw on e5: 1...Re5 2.Qd3# vs 1...Be5 2.Nf7#"*).

The optional `story` (or `format`) clause allows authors to specify custom interpolation templates. When omitted, Thema automatically generates a **canonical chess composition story** from the solution table.

#### Syntax
```text
story: "Template text with {placeholders}..."
// or
story "Template text..."
// or
format "Template text..."
```

The `story` / `format` clause can appear anywhere after the matrix section, alongside `where` and `with`.

#### Interpolation Placeholders

Within the template string, curly braces `{...}` interpolate dynamic move details bound during matching:

| Placeholder | Expands To | Example Value |
|---|---|---|
| `{var}` | Move in standard algebraic notation (SAN) | `1...Re5`, `2.Qd3#`, `1.Qd8!` |
| `{var.from}` | Departure square coordinate | `e8`, `c3` |
| `{var.to}` | Arrival square coordinate | `e5`, `d4` |
| `{var.role}` / `{var.piece}` | Human-readable piece name | `pawn`, `Knight`, `Bishop`, `Rook`, `Queen` |
| `{var.role_char}` | Single-letter uppercase piece role | `P`, `N`, `B`, `R`, `Q` |
| `{var.piece_desc}` | Piece name with departure square | `pawn on f2`, `Knight on a5` |
| `{var.promotion}` | Promoted piece name | `Knight`, `Bishop`, `Rook`, `Queen` |
| `{key}` / `{K}` | Key move of problem (resolved automatically even if `K` is omitted from the pattern!) | `1.Qd8!` |
| `{Tr}` / `{T}` / `{Tr1}`..`{Tr3}` | Try moves of the 1st/2nd/3rd matched try rows (resolved automatically even if omitted from the pattern!) | `1.Bc5?` |
| `{a}`..`{h}` | Black defense moves in columns 1..8 (and `.from`/`.to`/`.role`, resolved automatically even if omitted!) | `1...Re5`, `e5` |
| `{threat}` | Threat move of primary phase (Key or Try) | `2.Qe7#` |
| `{threat_clause}` | Formatted threat clause if threat(s) exist (` (threat 2.X#)` or ` (threats 2.X#, 2.Y#)`), else empty | ` (threat 2.Qe7#)` |
| `{refutation}` | Refutation move of primary try phase | `1...d5!` |
| `{phase1}`, `{phase2}`, `{phase3}` | Human-readable phase label for the 1st/2nd/3rd matched phase row | `Set-play`, `Try 1.Bc5?`, `Key 1.Re6!` |

#### Automatic Checkmate Suffix Normalization
When templates specify move numbers and mate signs, e.g. `2.{A}#`, Thema automatically prevents double checkmate markers (`##`). Because engine SAN generation already appends `#` to checkmating moves, `{A}#` safely produces `2.Qd3#` rather than `2.Qd3##`.

#### Canonical Auto-Story Engine (Default Fallback)
If a specification does not include an explicit `story` clause, Thema's presentation engine synthesizes a structured story according to standard problem literature:

1. **Try Phases**: Formatted with question marks, parenthesized threats, and refutations:
   ```
   1.Re4? (threat 2.Qd5#) 1...d5!
   ```
2. **Set Play Phases**: Formatted with set play prefix `*` and variations:
   ```
   * 1...Re5 2.Nf7# | 1...Be5 2.Qd3#
   ```
3. **Key Phase**: Formatted with exclamation mark, parenthesized threat, and thematic defensive variations:
   ```
   1.Qd8! (threat 2.Qd5#) 1...Re5 2.Nf7# | 1...Be5 2.Qd3#
   ```

#### Spec Examples with Story Templates

```thema
// Grimshaw with custom narrative format
def [a b]
key [A B]
where a.to == b.to
  && {a.role, b.role} == {'R', 'B'}
  && a.from != b.from && !a.is_capture
  && blocks_ray(a.to, b.from, A.to)
  && blocks_ray(b.to, a.from, B.to)
story "Grimshaw on {a.to}: 1...{a} 2.{A} vs 1...{b} 2.{B}"
```

```thema
// Switchback with origin and return squares
key [K _ A]
where A.from == K.to && A.to == K.from
story "Switchback of {K.role}: 1.{K} ... 2.{A} (returns {K.to}->{A.to})"
```

---

## 5. Complete Standard Library of Primitives

Every primitive in Thema is orthogonal and general-purpose.

### 5.1 Geometry & Board Rays

#### `collinear(sq1, sq2, sq3)` -> `bool`
True if all three squares lie on the same straight line (rank, file, or diagonal).
```thema
where collinear(a.from, b.from, K.to)
```

#### `between(sq, sqA, sqB)` -> `bool`
True if square `sq` strictly lies between `sqA` and `sqB` on a straight collinear line.
```thema
where between(a.to, b.from, BK)
```

#### `distance(sq1, sq2)` -> `int`
Chebyshev distance (King move distance) between two squares: $\max(|\Delta f|, |\Delta r|)$.
```thema
where distance(K.to, BK) == 1
```

#### `ray_clear(from_sq, to_sq)` -> `bool`
True if the straight ray between `from_sq` and `to_sq` contains zero intermediate pieces.
```thema
where ray_clear(A.from, BK)
```

#### `blocks_ray(blocker_sq, from_sq, to_sq)` -> `bool`
True if `blocker_sq` lies strictly between `from_sq` and `to_sq` and interrupts an otherwise clear line of slider action. When evaluated with board context (`is_slider_line_cut_off`), `blocks_ray` (and `a.blocks(b, A)` / `a.mutually_blocks(b, A, B)`) checks whether the Black slider at `from_sq` is cut off by `blocker_sq` from:
- guarding or arriving on `to_sq` (`A.to`),
- interposing on a direct check line (`A.to -> BK`), or
- capturing a rear battery piece (`cur_sq == rear_sq`) or interposing on a discovered/battery check line (`rear_sq -> BK`) when the move to `to_sq` fires a discovered check.
```thema
where blocks_ray(a.to, b.from, A.to)
```

---

### 5.2 Square Navigation & Offsets

Directional square offsets return the square shifted by `dist` squares (default `dist = 1`), or `-1` if off the board:

- `up(sq, [dist])` — North (+Rank)
- `down(sq, [dist])` — South (-Rank)
- `left(sq, [dist])` — West (-File)
- `right(sq, [dist])` — East (+File)
- `left_up(sq, [dist])` — North-West
- `right_up(sq, [dist])` — North-East
- `left_down(sq, [dist])` — South-West
- `right_down(sq, [dist])` — South-East

Example:
```thema
// Check if defense lands on a star flight around the King
where a.to in {up(BK), down(BK), left(BK), right(BK)}
```

---

### 5.3 Board Position Specifiers & Pin Primitives

#### Board Position Specifiers: `before(...)` and `after(...)`
Board-state-dependent predicates (such as `is_pinned`, `guards`, `attacks`, `flights`) can be evaluated against explicit board states using `before(...)` and `after(...)`:
- `before(M)`: The board state immediately **before** move `M` was played (e.g., `before(K)` is the starting position; `before(a)` is the position before defense `a` was played).
- `after(M)`: The board state immediately **after** move `M` was played (e.g., `after(K)` is the position after the key; `after(a)` is after defense `a`; `after(X)` is after threat `X` is played).
- `before()`: Contextual before state (in variations: the pre-defense position `after_key`).
- `after()`: Contextual after state (in variations: the post-defense position `after_replies[tc]`).
- **Default Position**: When the position argument is omitted, predicates evaluate against `after()` by default.

#### `is_pinned(sq, [pos])` -> `bool`
True if the piece at `sq` is pinned against its friendly King in board position `pos` (default: `after()`).
```thema
// Check if Black piece on a.from was NOT pinned before 1...a,
// but became pinned on a.to after 1...a, and would be unpinned by threat X:
where !is_pinned(a.from, before(a))
  && is_pinned(a.to, after(a))
  && !is_pinned(a.to, after(X))
```

#### `self_pins(move)` -> `bool`
True if `move` (typically a defense move) moves an unpinned piece to a destination square where it becomes pinned against its friendly King.

#### `self_pins_piece(move)` -> `bool`
True if the specific piece making `move` is pinned to its King after the move, but was not pinned before the move.

#### `unpins_piece(move, target_sq)` -> `bool`
True if `move` (such as a key or threat) unpins the piece standing at `target_sq`.

#### `pinned_to(sq, king_sq)` -> `bool`
True if the piece at `sq` is pinned against `king_sq` (`BK` or `WK`). Resolves against pre-defense or post-defense states automatically. Also available as method `move.pinned_to(king_sq)` or `sq.pinned_to(king_sq)`.

#### `pins(move, [target_king])` -> `bool`
True if `move` establishes a new pin on a piece against `target_king` (default: opposing King) that was not pinned prior to `move`.

#### `unpins(move, [target_king])` -> `bool`
True if `move` unpins a friendly or enemy piece.

#### `indirect_pins(move, target_king)` -> `bool`
True if `move` creates a new pin on a piece against `target_king` via line opening/discovery (where `move.from` was collinear with the newly pinned piece and `target_king`, and `move.to` steps off that line, or for a Black move `move.to` is not the newly pinned square).

#### `is_half_pin()` -> `bool`
True if two Black pieces stand on a line between the Black King and a White slider in either the post-key position (`after_key`) or the initial diagram position (`start`).

#### `creates_half_pin()` -> `bool`
True if the key move creates a half-pin arrangement.

#### `is_white_half_pin([move])` -> `bool`
True if two White pieces stand in a half-pin between the White King and a Black slider (in `start` or `after_key`), and (when `move` is supplied) one of the two half-pinned White pieces is the piece departing from `move.from` (for all 64 squares `0..64`, including `a1`).

#### `is_double_pin([move])` -> `bool`
True if the post-key position (when called with 0 arguments: `is_double_pin()`) or the position after `move` (when called with 1 argument: `is_double_pin(a)` or `a.double_pin`) has $\ge 2$ pinned Black pieces.

---

### 5.4 Guards, Attacks & Line Relations

#### `guards(from_sq, target_sq)` -> `bool`
True if the piece at `from_sq` controls / guards `target_sq` in the most specific active board position (current defense reply position, or key position if `from_sq` was vacated by the defense).

#### `attacks(from_sq, target_sq)` -> `bool`
True if the piece at `from_sq` directly attacks `target_sq`.

#### `unguards(move, target_sq)` -> `bool`
True if the moving player had at least one effective (unpinned, or pinned along the ray to `target_sq`) guard on `target_sq` immediately prior to `move` being executed, and no longer has any effective guard on `target_sq` after `move` is played. Essential for unguard-based themes like Somov (B1), Bikos, and Deflection.

#### `interferes(move)` -> `bool`
True if `move` steps across and closes the line of action of a friendly line piece (Rook, Bishop, or Queen), excluding rays whose only obstructed square is the friendly King's own square.

#### `interferes_with(move, role)` -> `bool`
True if `move` closes the line of action of a friendly line piece of specific role (e.g. `interferes_with(a, 'B')` or `interferes_with(b, 'R')` in Grimshaw), excluding the friendly King's own square.

#### `cuts_enemy_line(move, [role])` -> `bool`
True if `move` steps across and closes the line of action of an opponent slider (optionally filtered by role `'R'`, `'B'`, `'Q'`), excluding rays where the only square beyond `move.to` is the opponent King's own square. Essential for Novotny and related intersection keys.

#### `cuts_line_to(move, target_sq)` -> `bool`
True if `move` closes a line piece's ray of action directed toward `target_sq`.

#### `opens_line(move, [target_sq])` -> `bool`
True if `move` unmasks a friendly slider line of action (optionally directed at `target_sq`).

#### `closes_line(move, [target_sq])` -> `bool`
True if `move` steps across and obstructs a friendly or enemy line of action.

#### `departs_line(move, target_sq)` -> `bool`
Geometric line departure: True if the moving piece was on a slider's line of action toward `target_sq` and departs from that line.

#### `arrives_line(move, target_sq)` -> `bool`
Geometric line arrival: True if the moving piece arrives on a slider's line of action toward `target_sq`.

#### `obstructs_slider(defense_move, target)` -> `bool`
True if `defense_move` blocks a slider from reaching `target`.

#### `is_anti_bristol(mv1, mv2)` -> `bool`
Anti-Bristol line clearance: A piece moves along a collinear line **toward** another piece, closing its line of action (the exact opposite of Bristol clearance, where a piece moves away to clear the line).

#### `is_valve(defense_move, mate_move)` -> `bool`
Defense opens a White line and closes a Black line, met by mate.

#### `is_bivalve(defense_move, mate_move)` -> `bool`
Defense opens a Black line and closes another Black line.

#### `is_anti_levman(defense_move, mate_move)` -> `bool`
Anti-Levman: White mate unmasks a White line and closes another White line toward BK.

---

### 5.5 Batteries & Half-Batteries

#### `fires_battery(move)` -> `bool`
True if `move` is a discovered check/mate delivered by moving the front piece of an active battery.

#### `battery_rear(move)` -> `Square`
- On a mating or threat move (`A`, `X`): returns the board square of the rear slider of the battery fired by `move` (or, for an indirect battery mate that does not give discovered check directly to `BK`, the rear slider unveiled onto a Black King flight square), or an invalid sentinel if `move` does not fire a direct or indirect battery.
- On a phase move (`K`, `Tr`): returns the rear slider square of a pre-move direct battery on `start` associated with `move` (where the front piece is capable of legally moving off the battery line), or an invalid sentinel if none exists.
Useful for verifying that multiple battery mates fire from the same rear piece (`battery_rear(A) == battery_rear(B)`), ensuring that the key piece forms the rear (`battery_rear(A) == K.to`) or front (`A.from == K.to`) of a newly created battery, or checking pre-move battery geometry (`between(K.battery_front, K.battery_rear, BK)`).

#### `battery_front(move)` -> `Square`
- On a phase move (`K`, `Tr`): returns the front piece square of a pre-move direct battery on `start` associated with `move` (requiring the front piece to have at least one legal move off the battery line so blocked/immobile pawns are excluded), or an invalid sentinel if none exists.
- On a mating or threat move (`A`, `X`): returns `move.from` when `move` fires a direct or indirect battery, or an invalid sentinel otherwise.

Common composable battery patterns:
```thema
// Battery creation (key forms front or rear of a battery that fires in play)
any K (X)
where X.fires_battery, K.to == X.from || K.to == X.battery_rear

// Half-battery (key vacates the battery line so the remaining piece fires)
key K [A]
where A.fires_battery, between(K.from, A.battery_rear, BK), !collinear(K.from, K.to, BK)

// Battery destruction (key abandons a pre-move direct battery without firing it)
key K [A]
where between(K.battery_front, K.battery_rear, BK),
  (K.from == K.battery_rear && !collinear(K.from, K.to, BK)) || (K.from == K.battery_front && !K.check && !A.fires_battery)

// Indirect battery (rear slider aims at a flight square rather than BK, or front piece delivers direct mate while rear slider guards a flight)
key [A]
where (A.fires_battery && !collinear(A.battery_rear, A.from, BK))
  || (!A.fires_battery && A.battery_front == A.from)
```

---

### 5.6 King Flights & Sacrifices

#### `king_flights()` -> `int`
Number of legal flight squares available to the Black King in the starting position.

#### `flights_taken([move])` -> `int`
Number of flight squares removed by `move` (default: key move).

#### `flights_given([move])` -> `int`
Number of new flight squares granted to the Black King by `move`.

#### `was_flight(mate_move)` -> `bool`
True if `mate_move.to` was an available King flight square prior to the move.

#### `is_king_y_flight()` -> `bool`
True if the Black King's flight squares form a symmetrical Y-shape.

#### `self_block(defense_move)` -> `bool`
Harmful effect of defense: Black's move occupies a square in the Black King's field that was previously guarded or empty, depriving the King of an escape square.

#### `is_sacrifice(move)` -> `bool`
True if the destination square of `move` can be legally captured by an opposing piece on the next turn.

#### `is_active_sacrifice([move])` -> `bool`
True if the piece moves actively into capture.

#### `is_passive_sacrifice()` -> `bool`
True if White's key passively leaves a piece en prise to Black capture.

---

### 5.7 Checkmate Footprints & Echoes

#### `is_pure_mate(mate_move)` -> `bool`
Pure mate: Every square in the Black King's field is attacked exactly once by White, or occupied by a single Black piece.

#### `is_mirror_mate(mate_move)` -> `bool`
Mirror mate: All squares in the Black King's field are completely unoccupied by other pieces.

#### `is_model_mate(mate_move)` -> `bool`
Model mate: Both pure and economical (all White units, except possibly King and pawns, participate in the mate).

#### `is_ideal_mate(mate_move)` -> `bool`
Ideal mate: A model mate in which every piece of both colors on the board participates.

#### `is_smothered_mate(mate_move)` -> `bool`
Smothered mate: The Black King is completely surrounded by friendly pieces and mated by a Knight.

#### `is_epaulette_mate(mate_move)` -> `bool`
Epaulette mate: The Black King is flanked on opposite parallel sides by two friendly pieces (epaulettes) blocking escape.

#### `is_pin_mate(mate_move)` -> `bool`
Pin mate: Checkmate depends critically on a pinned Black piece unable to interpose or capture.

#### `echo_mate(m1, m2)` -> `bool`
Echo mate: The mating configurations following `m1` and `m2` have identical geometric footprints on different squares.

#### `chameleon_echo(m1, m2)` -> `bool`
Chameleon echo: An echo mate occurring on squares of opposite color.

---

### 5.8 Phase, Table & Positional Metrics

#### `threat_count()` -> `int`
Number of threats generated by the key.

#### `try_count()` -> `int`
Total number of non-weak tries in the solution table.

#### `refutation_count(try_move)` -> `int`
Number of distinct refutations for the specified try move.

#### `unprovided_count()` -> `int`
Number of unprovided checks / defenses in the starting position.

#### `set_mate_count()` -> `int`
Number of variations with prepared mates in set play.

#### `variation_count()` -> `int`
Number of distinct defense variations in the key row.

#### `mate_count(var)` -> `int`
Number of mating moves bound to variable `var` (used for dual-mate verification).

#### `is_pure(var)` -> `bool`
True if the cell bound to `var` has exactly 1 checkmating move (no duals).

#### `mating_origins_count()` -> `int`
Number of distinct origin squares from which White delivers checkmate.

#### `piece_count([role])` -> `int`
Total pieces on board (White + Black), or total pieces of the given role (`'P'`, `'N'`, `'B'`, `'R'`, `'Q'`, `'K'`) when `role` is provided.

#### `pawn_count()` -> `int`
Total pawns on board (`piece_count('P')`).

#### `white_piece_count([role])` -> `int`
Total White pieces on board, or total White pieces of the given role (`'P'`, `'N'`, `'B'`, `'R'`, `'Q'`, `'K'`) when `role` is provided (e.g. `white_piece_count('Q') == 1 && white_piece_count('R') == 2` for Hertzsprung material).

#### `black_piece_count([role])` -> `int`
Total Black pieces on board, or total Black pieces of the given role when `role` is provided.

#### `start_is_check()` -> `bool`
True if the starting position begins with White or Black in check.

#### `is_double_check(move)` -> `bool`
True if `move` delivers check from two pieces simultaneously.

#### `is_position_symmetric()` -> `bool`
True if the starting board setup has bilateral or rotary symmetry.

#### `has_symmetric_try()` -> `bool`
True if the White King, Black King, and key-piece origin (`K.from`) lie on the same symmetry axis (file or rank), at least one pair of off-axis pieces is symmetric across that axis, and White has a single-refutation try by the same piece mirroring `K.to` across that axis (`2 * axis - K.to`).

#### `set_play_complete()` -> `bool`
True if set play is complete for every legal Black move (complete block).

#### `has_removed_set_defense()` -> `bool`
True if White's key eliminates a defense that existed in set play.

#### `try_threat_in_key(try_move)` -> `bool`
True if the threat of `try_move` reappears as a variation mate in the key.

#### `white_interference_count()` -> `int`
Number of distinct White moves cutting friendly slider lines.

---

## 6. Pattern Matching & Try Quality Engine

### Pattern-Driven Constraints (Eliminating Boilerplate)

Thema is designed so that the pattern grid itself carries the structural constraints. You do not need to write defensive `where` clauses:

1. **Single Threat vs Multi-Threat**:
   - If cell 1 contains a single variable (`A`), Thema matches **only** rows with exactly 1 threat.
   - If cell 1 contains multiple variables (`AB`), Thema matches rows with **exactly 2 threats**, binding `A` and `B` to distinct threat move indices.
   - If the threat slot is the wildcard `_` (or omitted), threat count is unconstrained.
2. **Multi-Threat Separation in `SolutionTable`**:
   - In any phase with $k \ge 1$ distinct `(from, to)` threats, a Black reply is included as a thematic defense column if it parries all threats, OR (when $k \ge 2$) if it separates the threats by parrying at least $k - 1$ threats and leaving at most 1 distinct `(from, to)` mating move. This allows threat-separation themes (Fleck, double-threat Novotny, Finnish Novotny, Robert theme, multi-threat Pickaninny, Sushkov) to be matched directly on the `SolutionTable`.
3. **Single Refutation vs Multi-Refutations**:
   - If a try pattern row contains a single `!` refutation marker, Thema matches **only** tries with **exactly 1 distinct refutation**.
   - If a try pattern row contains multiple `!` markers (e.g. `CyclicRefutations`), Thema automatically allows multi-refuted tries.
4. **Single Mate vs Dual Mates (`MultiVar` Cells)**:
   - If a variation cell contains a single variable (`A`), Thema matches **only** variations with a unique checkmate (eliminating unintended duals).
   - If a variation cell contains `AB` (e.g. `[AB _ _]` in Robert theme or `[XA YA B]` in Dual-Avoidance Black Correction), it requires at least $k$ mating options in that cell and backtracks over all $k$-permutations of distinct candidate moves within the cell (`try_bind_multivar_mates`), ensuring variables with asymmetric constraints or pre-bound cross-column identities match regardless of move ordering inside the `TableCell::Mates` list.
5. **Variable Distinctness**:
   - Distinct Black defense variables (`a`, `b`, `c`, `d`) are always bound to distinct defense columns (`a != b` is always guaranteed automatically).
   - Distinct White move variable names (`A`, `B`, `C`, or `Tr`, `K`) cannot bind to the same chess move unless a variable carries the `*` non-exclusive modifier (`A*`) or a row carries the `+` no-line-reset prefix across phases without sharing a row or `^` column. You never need to write `A != B`, `a != b`, or `distinct(A, B, C)` within a standard pattern.
6. **Capture Self-Blocks & En Passant Flags**:
   - `a.self_block` (`self_block(a)`) holds whenever a non-King Black move lands on a square adjacent to the Black King (`distance(a.to, BK) == 1`) and White's mate does not recapture on `a.to` (`mate.to != a.to`), including capture self-blocks on flight squares.
   - Diagonal pawn moves onto an empty target square in any phase or variation automatically set both `FLAG_CAPTURE` and `FLAG_EP` (`is_en_passant`).
7. **Single Wildcard `_` (Phase Move, Threat & Variation Cells)**:
   - `_` is the **only** wildcard symbol. You don't need to name the phase move or threat if you aren't inspecting it: simply omit it (`key [A B]` is equivalent to `key _ (_) [A B]`).
   - Inside brackets, `_` matches anything in that column (a mate, a refutation, or an empty cell), e.g. `try (A) [! _]`.
   - Any other non-identifier cell token (such as `.` or a bare `?`) is a **syntax error**. (Historically, `.` was silently parsed as a shared variable named `"."`, which forced all such cells to bind one identical move.)

### Automatic Try Quality Filtering

In chess problem composition, themes only count when tries are serious and artistic. The Thema engine automatically filters out trivial "stupid" tries before pattern matching:

- **No threats + few replies**: Tries with zero threats and $\le 2$ legal Black replies.
- **Sparse zugzwang tries**: Tries with zero threats, multiple refutations, and $\le 2$ mating replies.
- **Checking refutations**: Refutations that deliver check to the White King.
- **Checking tries refuted by King moves**: Checking tries trivially refuted by King flight.
- **Direct capture of the try piece**: Refutations where Black simply captures the piece that moved to its destination square (e.g. try `Nd4?`, refuted by `Bxd4!`).

Because these filters run automatically, Thema specifications remain clean, concise, and focused on theme aesthetics. Individual themes can override or relax these rules using the [`with` clause](#the-with-clause-per-theme-quality-configuration) (e.g. `with strict -capture_try_piece`).

---

## 7. Theme Authoring Guidelines & Anti-Patterns

### ✅ Best Practices
1. **Omit Unnecessary `where` Clauses**:
   If the phase and column relationships define the theme, don't add a `where` clause.
2. **Use Inline Cell Annotations for Roles, Captures & Checks**:
   Write `def [a:N b:N c:B d:B]` or `def [a:x b:x]` instead of verbose `a.role == 'N' && b.role == 'N' ...` in `where`.
3. **Omit `_ _` in `def` Rows (or Omit `def` Entirely)**:
   Write `def [a:N b:N]` (automatically aligned to columns 2..N), or omit `def` completely when using `a, b, c, d` without cell annotations.
4. **Use Tuple Broadcasting, Chained Comparisons & Direct `distinct`/`same`**:
   - `(a, b, c, d).role == 'P'` instead of repeating `.role == 'P'` four times.
   - `self_block(a, b, c, d)` instead of repeating `self_block(...)` four times.
   - `a.to == b.to == c.to` and `distinct(A, B, C, D)` instead of verbose `count_distinct(...) == 4`.
5. **Use Comma-Separated `where` Checklists**:
   Separate top-level conditions in `where` with `,` (or `&&`) for clean, readable multi-line specs.
6. **Use Set Comparisons or Shorthands for Order-Invariant Roles**:
   ```thema
   // GOOD: Order-invariant
   {a.role, b.role} == {'R', 'B'}

   // GOOD: Equivalent shorthand
   unlike_sliders(a, b)

   // BAD: Fragile column-ordering dependency
   a.role == 'R' && b.role == 'B'
   ```

### ❌ Anti-Patterns to Avoid
1. **Never Re-invent Geometric Primitives**:
   Do not write file/rank arithmetic to test lines; use `collinear(a, b, c)` or `blocks_ray(...)`.
2. **Avoid Redundant Same-Row Inequality Checks**:
   Do not write `where A != B` when `A` and `B` are already distinct variables in the same row (unless the row uses `+` no-line-reset across phases).
3. **Avoid Redundant Count Checks**:
   Do not write `threat_count(T) == 1` or `refutation_count(T) == 1` when the pattern row already specifies single threat and single refutation.

---

## 8. Canonical Themes Cookbook

### 8.1 Dombrovskis
```thema
try (A) [! _]
try (B) [_ !]
key [A B]
```

### 8.2 Grimshaw
```thema
key [A B]
where same_square(a, b),
  {a.role, b.role} == {'R', 'B'},
  a.from != b.from, !a.capture,
  a.blocks(b, A),
  b.blocks(a, B)
```

### 8.3 Novotny
```thema
def [a:x@K b:x@K]
key K [A B]
where unlike_sliders(a, b),
  a.blocks(b, A),
  b.blocks(a, B)
```

### 8.3b Plachutta
```thema
def [a:x@K b:x@K]
key K [A B]
where a.from != b.from,
  like_sliders(a, b),
  !collinear(a.from, b.from, K.to),
  (A.recaptures(a) || B.recaptures(b)),
  a.blocks(b, A),
  b.blocks(a, B)
```

### 8.4 Barnes Theme
```thema
any (AB)
any (A)
any (B)
```

### 8.4b Switchback & Umnov
```thema
// Switchback: key piece returns to its origin square on move 2
key K [~K]

// Umnov: mates land on the squares vacated by Black's defenses
key [A@a.from B@b.from]
```

### 8.5 Pickaninny (Complete 4-Move Black Pawn Play)
```thema
def [a:P b:P c:P d:P]
any [A* B* C* D*]
where same_piece(a, b, c, d),
  count_distinct(A, B, C, D) >= 2,
  a.to == down(a.from),
  b.to == down(b.from, 2),
  c.to == left_down(c.from),
  d.to == right_down(d.from)
```

### 8.6 Albino (Complete 4-Move White Pawn Play)
```thema
key [A:P B:P C:P D:P]
where same_piece(A, B, C, D),
  distinct(A.to, B.to, C.to, D.to)
```

### 8.7 Horseblock & Mule Theme
```thema
// Horseblock (4 Black Knight self-blocks)
def [a:N b:N c:N d:N]
key [A B C D]
where (a, b, c, d).self_block

// Mule Theme (2 Black Knight + 2 Black Bishop self-blocks)
def [a:N b:N c:B d:B]
key [A B C D]
where (a, b, c, d).self_block
```

### 8.8 Star-Flights & Cross-Flights
```thema
// Star-flights (4 diagonal King flights)
def [a:K b:K c:K d:K]
key [A B C D]
where (a, b, c, d).to in {left_up(BK), right_up(BK), left_down(BK), right_down(BK)}

// Cross-flights (4 orthogonal King flights)
def [a:K b:K c:K d:K]
key [A B C D]
where (a, b, c, d).to in {up(BK), down(BK), left(BK), right(BK)}
```

### 8.9 Bikos Theme (Reciprocal Change of Harmful Defense Effects)
```thema
vir [A B]
+any [C D]
where A != C, B != D,
  (a, b).flight_block,
  (A.recaptures(a) && !B.recaptures(b) && !C.recaptures(a) && D.recaptures(b))
  || (!A.recaptures(a) && B.recaptures(b) && C.recaptures(a) && !D.recaptures(b))
```

### 8.10 Black Correction (Block-Based)
```thema
key [_ _ A A B]
where threat_count() == 0,
  a.role in {'N', 'B', 'R', 'Q'},
  same_piece(a, b, c),
  distinct(a.to, b.to, c.to),
  a.to != A.to, b.to != A.to
```

### 8.11 Somov (Somov B1: Loss of Guard in Black Correction)
A Black correction defense where the corrective move parries White's threat or general mate, but features the secondary flaw of unguarding a square, enabling White to deliver checkmate on that square:
- **Threat-based Somov**:
```thema
key (T) [T B]
where same_piece(a, b),
  (b.to != B.to || pinned_to(b.to, WK)),
  b.unguards(B)
```
- **General-mate Somov**:
```thema
key [A A B]
where same_piece(a, b, c),
  (c.to != B.to || pinned_to(c.to, WK)),
  c.unguards(B)
```

### 8.12 Salazar & Double Salazar (Reversal of White's 1st and 2nd Moves)
```thema
// Salazar: White's first and second moves reverse between try and key against the same defense
try A [B]
key B [A]

// Double Salazar: Two tries answer defenses with C, and Key C answers with A and B
try A [C _]
try B [_ C]
key C [A B]
```

### 8.13 Stavrinides & Kubbel Cycle (Circular Square-to-Square Umnov Cycle)
```thema
// Stavrinides (2-variation closed cycle)
key [A B]
where A.to == b.to, B.to == a.to, A.to != B.to

// Kubbel Cycle (3-variation closed cycle)
key [A B C]
where A.to == b.to, B.to == c.to, C.to == a.to, distinct(A.to, B.to, C.to)
```

### 8.14 Herlin Counter-Clearance & Black Umnov
```thema
// Black Umnov: Black defense moves onto the square vacated by the White key piece
def [a@K.from]
key K [A]

// Herlin Counter-Clearance: Mutual head-on line duel between a Black slider and a White slider
def [a:!x b:x@B.from]
key [B:x@a A:x@b]
where same_piece(a, b), a.slider, B.slider,
  collinear(a.from, a.to, B.from), between(a.to, a.from, B.from)
```

### 8.15 Secondary Dombrovskis, Kharkov 2, King's Le Grand & Soviet-French
```thema
// Secondary Dombrovskis (defense-level correction mate transference)
vir [A _]
+any [C A]
where same_piece(a, b)

// Kharkov 2 (chained try refutations resolved by changed mates)
try [! -]
try [A !]
key [C D]

// King's Le Grand (Le Grand reciprocal play against a Black King flight)
def [a:K]
try (A) [B]
key (B) [A]

// Soviet-French Theme (Dombrovskis try threats combined with a flight-giving key)
try (A) [! _]
try (B) [_ !]
key K [A B]
where K.flights_given > 0
```

---

## 9. Extended Theme Catalogue

Additional canonical specifications, listed in `specs.rs` order. Use them as further examples; open any of them in Thema Studio via the Encyclopedia (⌘K → Edit).

### 9.1 Encyclopedia & YACPDB Themes (specs #342–#361)
```thema
// 342. Karlstrøm-Fleck (multi-threat key + total defenses forcing fresh non-threat mates)
key (XY) [A B]
with -match_threat_count

// 343. Bi-coloured Bristol (opposite-color line clearance)
def [a:Q|R|B]
key K:Q|R|B [A]
where K.clears_line_for(a)

// 344. Azerbaijani Novotny (3-capture sacrifice on R+B intersection square)
def [a:R:x@K b:B:x@K c:x@K]
key K [A B C]
where distinct(a.from, b.from, c.from), a.blocks(b, A), b.blocks(a, B)

// 345. English Grimshaw (Queen + Rook/Bishop mutual interference)
def [a:Q:!x b:R|B:!x]
key [A B]
where same_square(a, b), a.from != b.from

// 346. English Novotny (Queen + Rook/Bishop line-cutting sacrifice)
key K (AB)
where K.cuts_enemy_line('Q'), K.cuts_enemy_line('R') || K.cuts_enemy_line('B')

// 347. Double bind Grimshaw (4 Black sliders converging on the same intersection square)
def [a:!x b:!x c:!x d:!x]
key [A B C D]
where same_square(a, b, c, d), distinct(a.from, b.from, c.from, d.from),
  (a, b, c, d).slider

// 348. Ukrainian theme (3-phase cyclic threat-mate shift against the same defense)
try (A) [B]
try (B) [C]
key (C) [A]

// 349. Herpai theme (reciprocal mate/refutation on the same square united in key)
try [A !]
try [! B]
key [A B]
where same_square(a, b), a.from != b.from

// 350. Brojt / Double-Decker Novotny (Novotny on K.to + Grimshaw on second square)
def [a:R:x@K b:B:x@K c:R:!x d:B:!x]
key K [A B C D]
where same_square(c, d), c.to != K.to

// 351. Luukkonen theme (same-square mate X becomes key threat while defenses split into A, B)
vir [X X]
key (X) [A B]
where same_square(a, b), a.from != b.from
with -match_threat_count

// 352. Threat return (threat is a switchback of the key piece)
key K (T~K)

// 353. Rook sacrifice (White Rook sacrificed to at least 2 Black captors)
def [a:x@K b:x@K]
key K:R [A B]
where a.from != b.from

// 354. 2 capture flights (Black King has at least 2 legal capture flights)
def [a:K:x b:K:x]
key [A B]
where a.to != b.to

// 355. Queen's cross (White Queen mates along both orthogonal and diagonal cross rays)
key [A:Q B:Q C:Q D:Q E:Q F:Q]
where same_piece(A, B, C, D, E, F),
  (A, B, C).ortho, (D, E, F).diag,
  A.to < B.to < C.to, D.to < E.to < F.to

// 356. Sushkov analog for secondary threats
try (AB) [_ _]
try [A !]
try [! B]
key [A B]

// 357. Black underpromotion (distinct promotions by the same Black pawn)
def [a:= b:=]
key [A B]
where same_piece(a, b), a.to == b.to, a.promotion != b.promotion

// 358. Cyclic Pseudo-Le Grand (tries threaten A, B, AB; key threatens C and mates A, B)
try (A) [_ _]
try (B) [_ _]
try (AB) [_ _]
key (C) [A B]

// 359. Anti-Dombrovskis (try threat A becomes try variation mate A, then changes to C in key)
try (A) [B]
try (D) [A]
key (E) [C]

// 360. Anti-Le Grand (double threat AB separated in try and inverted with changed mate in key)
try (AB) [_ _]
try (B) [_ A]
key (A) [B C]

// 361. Shanshin dual avoidance (reciprocal exchange between double-threat component and variation mate)
try (AB) [C _]
key (DC) [_ B]

// 362. Black correction (try refutation: 2 random moves of a Black piece allow mate A in a try, while correction c refutes)
def [a:N|B|R|Q b c]
try (T) [A A !]
where same_piece(a, b, c), distinct(a.to, b.to, c.to), a.to != A.to, b.to != A.to, !c.capture

// 363. Black correction (general mate + capture-dual on random moves, single mate on correction move)
def [a:B|R|Q b c]
key [XA YA B]
where same_piece(a, b, c), distinct(a.to, b.to, c.to), X.recaptures(a), Y.recaptures(b), !A.recaptures(a), !A.recaptures(b), !c.capture

// 364. Vladimirov + Dombrovskis (try piece A with threat B is doubly refuted; key answers those refutations with A and B)
try A (B) [! !]
key [A B]

// 365. White correction (tries by the same White piece with distinct threats and refutations)
try Tr1 (X) [! _]
try Tr2 (Y) [_ !]
key K [A B]
where same_piece(Tr1, Tr2), Tr1.to != Tr2.to

// 366. Vladimirov (try piece A refuted by Black capture on A.to; in key, Black moves to A.to and is answered by A#)
try A [! _]
key [_ A]
where a.to == A.to, b.to == A.to, !b.capture
with -capture_try_piece -match_threat_count

// 367. Goethart (Black defense obstructs a pinned Black piece, allowing White's non-battery mate to interpose and indirectly unpin it)
key [A]
where a.closes_line() || a.self_block, unpins(A, BK), !A.fires_battery

// 368. Gamage (Black defense obstructs a pinned Black piece, allowing White's pinning slider to depart the pin line and directly unpin it)
key [A]
where a.closes_line() || a.self_block, A.slider, unpins(A, BK), !A.fires_battery

// 369. Anti-Goethart (Black defense indirectly unpins a Black piece, answered by White's battery or interference mate)
key [A]
where unpins(a, BK), A.fires_battery || a.closes_line(A)

// 370. Rupp (key move simultaneously changes the pin status of both a White piece and a Black piece)
key K
where (K.pins(BK) && K.pins(WK)) || (K.unpins(WK) && (K.unpins(BK) || K.pins(WK)))

// 371. Perfect Novotny (3-variation Novotny: 2 slider captures + 1 non-capture defense with 3 distinct mates)
def [a:R:x@K b:B:x@K c:!x]
key K [A B C]
where a.from != b.from, a.blocks(b, A), b.blocks(a, B)

// 372. Latvian Novotny (White try sacrifices on an R+B intersection to threaten 2 mates, refuted by a non-capturing Black defense)
def [a:!x]
try Tr (AB) [!]
where Tr.cuts_enemy_line('R'), Tr.cuts_enemy_line('B'), a.to != Tr.to

// 373. Mansfield (two Black pieces capture on the same square and self-pin, answered by distinct White battery mates)
def [a:x b:x]
key [A B]
where same_square(a, b), a.from != b.from,
  A.fires_battery, B.fires_battery, a.self_pins, b.self_pins

// 374. Anti-Reversal (Salazar reversal with one move changed across try and key)
try A [B]
key C [A]
where distinct(A, B, C)

// 375. Black Correction with General-Mate Duals (random moves allow general mate A plus secondary duals, correction forces B)
def [a:N|B|R|Q b c]
vir [XA YA B]
where same_piece(a, b, c), distinct(a.to, b.to, c.to), a.to != A.to, b.to != A.to

// 376. Set Hannelius (virtual mates Y and X reappear reciprocally as threats in two tries refuted by a and b)
vir     [Y X]
try (X) [! _]
try (Y) [_ !]
with -match_threat_count -match_mate_count

// 377. Boros Unpin (Black defense closes a Black line or self-blocks while indirectly unpinning a Black piece)
def [a:!K]
any [A]
where unpins(a, BK), (a.closes_line() || a.self_block)

// 378. Mari Battery Unpin (Black defense allows White's battery piece to interpose on a pin line and indirectly unpin a Black piece)
key [A]
where unpins(A, BK), A.fires_battery, (a.closes_line() || a.self_block || a.capture)

// 379. Pelle Move (a pinned White or Black piece moves along its pin line)
any [A]
where (pinned_to(A.from, WK) && collinear(A.from, A.to, WK))
   || (pinned_to(a.from, BK) && collinear(a.from, a.to, BK))

// 380. Urania (a single White move A appears across 3 distinct phases as first move, threat, and mate)
any A
any (A)
any [A]
with -capture_try_piece -match_threat_count -match_mate_count -no_threats_few_replies -no_threats_sparse_mates

// 381. Erokhin (try threatens A and answers defense a with B; subsequent phase plays B as first move and answers a with A)
try (A) [B]
+any B [A]
where A != B
with -refutation_is_check -match_threat_count -capture_try_piece

// 382. Set Dombrovskis (virtual mates A and B against defenses a and b reappear as try threats refuted by a and b)
vir     [A B]
try (A) [! _]
try (B) [_ !]
with -match_threat_count -match_mate_count -single_refutation -capture_try_piece -refutation_is_check

// 383. Moscow Theme I (1928: two Black defenses open a Black line to parry the threat while closing a Black line or self-blocking)
key (T) [A B]
where a.opens_line(), b.opens_line(), a.closes_line() || a.self_block, b.closes_line() || b.self_block
with -match_threat_count

// 384. Black Correction on Mating Square (random moves a and b allow quiet mate A; correction c arrives on A.to and is captured by A)
def [a:N|B|R|Q b c]
any [A A A]
where same_piece(a, b, c), distinct(a.to, b.to, c.to), a.to != A.to, b.to != A.to, c.to == A.to
```

### 9.2 Additional Orthodox `#2` Themes (specs #362–#461)
Batch 16 expands the canonical library with 100 orthodox `#2` themes across 10 thematic families (reaching **428 `NamedTheme` variants**, **461 `ThemeSpec` definitions**, and **518 compiled patterns**):

1. **Line Clearance & Turton / Bristol Family (10 themes)**:
   - `LoydTurton`, `BrunnerTurton`, `ZeplerTurton`, `DoubleBristol`, `BlackBristol`, `BlackAntiBristol`, `OrthogonalBristol`, `DiagonalBristol`, `ClearanceKey`, `VacatingSacrifice`
2. **Interference, Novotny, Grimshaw & Valve Variants (12 themes)**:
   - `SilentNovotny`, `CheckNovotny`, `PawnNovotny`, `CaptureNovotny`, `ThreatGrimshaw`, `TripleGrimshaw`, `SetGrimshaw`, `TryGrimshaw`, `DoubleValve`, `DoubleBivalve`, `WhiteValve`, `MutualSelfObstruction`
3. **Multi-Phase & Changed/Transferred Mate Matrix Themes (12 themes)**:
   - `TripleDombrovskis`, `TripleHannelius`, `TripleLeGrand`, `TriplePseudoLeGrand`, `DoubleBanny`, `DoubleLacny`, `DoubleRudenko`, `QuadrupleChangedMates`, `SetChangedPlusAddedMate`, `ReciprocalTransferredMates`, `TryThreatBecomesKey`, `KeyBecomesTryThreat`
4. **Pinning, Unpinning & Half-Pin Family (10 themes)**:
   - `DirectWhiteUnpin`, `IndirectWhiteUnpin`, `DirectBlackUnpin`, `IndirectBlackUnpin`, `WhiteSelfPin`, `BlackSelfPin`, `DoubleHalfPin`, `CrossPin`, `PinReplacement`, `SchiffmannDefenseI`
5. **Battery & Masked Line Family (10 themes)**:
   - `DoubleDirectBattery`, `DoubleIndirectBattery`, `RoyalBattery`, `BlackBatteryCreation`, `MaskedBatteryKey`, `OrthogonalBatteryMates`, `DiagonalBatteryMates`, `AntiBatteryDefense`, `PawnBatteryMate`, `PromotionBatteryMate`, `SwitchbackBatteryMate`
6. **Pawn Play, Promotion & En Passant Family (9 themes)**:
   - `Allumwandlung`, `BabsonTask`, `TriplePromotion`, `DoubleUnderpromotion`, `KnightPromotions`, `RookPromotions`, `BishopPromotions`, `MutualEnPassant`, `ExcelsiorStep`
7. **Geometrical, Task & Star/Wheel Family (10 themes)**:
   - `BlackQueenWheel`, `WhiteRookCross`, `WhiteBishopCross`, `BlackRookCross`, `BlackBishopCross`, `TripleSwitchback`, `QuadrupleSwitchback`, `DoubleCornerToCorner`, `MaximumFlightTask`, `PendulumTheme`
8. **King Flights, Give-and-Take & Sacrifices (10 themes)**:
   - `GiveAndTakeTwo`, `GiveAndTakeThree`, `FourFlightKey`, `ThreeCaptureFlights`, `QueenSacrifice`, `BishopSacrifice`, `KnightSacrifice`, `DoubleSacrificeKey`, `QuadrupleSelfBlock`, `RoyalSelfBlock`
9. **Correction, Focal & Dual Avoidance Family (8 themes)**:
   - `TripleBlackCorrection`, `SecondaryWhiteCorrection`, `KnightCorrection`, `BishopCorrection`, `RookCorrection`, `QueenCorrection`, `FocalInterference`, `DualSeparationBySelfBlock`
10. **Mate Aesthetics, Twins & Structural Conditions (8 themes)**:
    - `MiniaturesSeven`, `UltraMiniature`, `SymmetricalPosition`, `DoubleModelMate`, `TripleModelMate`, `DoublePureMate`, `DoubleMirrorMate`, `DoublePinMate`, `TriplePinMate`

Representative Batch 16 Thema specifications:
```thema
// Loyd-Turton: Stronger White slider (Q) withdraws across intersection so weaker slider (R/B) steps infront to mate
key K:Q [A:R|B]
where collinear(K.from, K.to, A.to), between(A.to, K.from, K.to),
  collinear(A.from, A.to, BK), between(A.to, K.to, BK)

// Allumwandlung (AUW): Promotions to all 4 piece types (Q, R, B, N) across the solution
any [A:= B:= C:= D:=]
where {A.promotion, B.promotion, C.promotion, D.promotion} == {'Q', 'R', 'B', 'N'}

// Give-and-Take (2 flights): Key takes at least 1 flight and grants at least 2 new flights
key K [A B]
where K.flights_taken >= 1, K.flights_given >= 2, (a, b).role == 'K', a.to != b.to

// Triple Dombrovskis: 3 try threats refuted by their respective thematic defenses become mates after those defenses in the key
try (A) [! _ _]
try (B) [_ ! _]
try (C) [_ _ !]
key [A B C]
```

### 9.3 Named Encyclopedia, YACPDB & WinChloe Themes (specs #462–#661)
Added 200 genuine named `#2` composition themes from *The Chess Problem Encyclopedia* (Velimirović & Valtonen), YACPDB (`#2` keyword taxonomy), and WinChloe across 10 thematic families, expanding the canonical Thema library to **628 `NamedTheme` variants** (`661` `ThemeSpec` definitions, `718` compiled patterns):

1. **Named Dual Avoidance & Good Companion Themes (`#462`–`#481`, 20 themes)**:
   - `ThemeA`, `ThemeB`, `ThemeC`, `ThemeD`, `ThemeE`, `ThemeF`, `ThemeG`, `ThemeH`, `Feldmann1`, `Feldmann2`, `Roels`, `AntiRoels`, `Weenink`, `Guidelli`, `Bottacchi`, `Foschini`, `Chicco`, `Brogi`, `Padulli`, `Sackmann`
2. **Named Novotny, Grimshaw, Plachutta & Interference Themes (`#482`–`#501`, 20 themes)**:
   - `BakuNovotny`, `NorwegianNovotny`, `PickabishNovotny`, `GreekNovotny`, `RemoteNovotny`, `SchiffmannNovotny`, `BorosNovotny`, `BorosGrimshaw`, `LatvianPlachutta`, `BorosPlachutta`, `KubbelGrimshaw`, `WhiteNovotny`, `RoyalGrimshaw`, `CederInterference`, `SchneiderInterference`, `HarmoniumPipes`, `Avanta`, `Elmgren`, `NanningTheme`, `BicolorBivalve`
3. **Named Pin, Half-Pin, Unpin & Cross-Check Themes (`#502`–`#521`, 20 themes)**:
   - `Cristoffanini`, `Costachel`, `Seilberger`, `Moeller`, `Dentist`, `Taale`, `Schiffmann2`, `KingsSchiffmann`, `WhiteSchiffmann`, `Schor`, `Ianovcic`, `Castellari`, `CastellariMari`, `CastellariSchor`, `Dobbs`, `Tuxen`, `Hume`, `AntiHume`, `AntiGamage`, `AntiRupp`
4. **Named Multi-Phase, Cyclic & Matrix Themes (`#522`–`#541`, 20 themes)**:
   - `Zappas`, `ZappasSimple`, `Crimean`, `SpisskaBorovicka`, `Zhuravlev`, `PseudoErokhin`, `AntiSalazar`, `PseudoSalazar`, `PapackCycle`, `CyclicHerpai`, `OneLineHerpai`, `Hermanson`, `Zarur`, `Poltava`, `Fokin`, `Kiev`, `Neva`, `Munich`, `Kontrawechsel`, `Adabashev`
5. **Named Correction, Umnov & Threat-Mechanism Themes (`#542`–`#561`, 20 themes)**:
   - `PseudoUmnov1`, `PseudoUmnov2`, `LarsenTheme`, `Szoghy1`, `Szoghy2`, `Szoghy3`, `Fuehrer`, `AntiFuehrer`, `AntiHassberg`, `Hassberg`, `Dalton`, `Pedersen`, `Mikulcak`, `Arnstam`, `Ojanen`, `Paros`, `BogdanovRychkov`, `VelimirovicAttack`, `Mlynka`, `Gooderson`
6. **Named Battery, Ambush, Clearance & Line Themes (`#562`–`#581`, 20 themes)**:
   - `Oudot`, `Mousetrap`, `Klasinc`, `Lahti`, `Blikeng`, `Kuchler`, `AmericanIndian`, `TargetBristol`, `SacrificeBristol`, `Schnoebelen`, `FleckBurkhardt`, `BurkhardtMate`, `TotalFleck`, `Barthelemy`, `FreiePresse`, `Seneca`, `AlainCWhite`, `Fastosky`, `RomppMates`, `KubbelChain`
7. **Named Half-Pin, Unblock & Structural Tactical Themes (`#582`–`#601`, 20 themes)**:
   - `FourPinWay`, `Servais`, `LoydHalfPin`, `Arguelles`, `Dawson`, `Wigwag`, `Hess`, `Martin`, `AntiSomovA1`, `AntiSomovA2`, `Hagemann`, `Monitor`, `Hirlap`, `Melnikov`, `Larceu`, `TemaArgentino`, `Kinnunen`, `Howard`, `Bograd`, `Muleblock`
8. **Named Piece Tasks, Wheels, Crosses & Pawn Themes (`#602`–`#621`, 20 themes)**:
   - `Superalbino`, `GavrilovPickaninny`, `Pawnee`, `Isardam`, `Kindergarten`, `Phoenix`, `Ropke`, `Schiegl`, `KubbelTheme`, `Octagon`, `Octopus`, `FourHandsRound`, `LarsenTask`, `Durbar`, `PerpetuumMobile`, `Magee`, `Segal`, `AnderssenMate`, `SupportMate`, `HertzsprungMaterial`
9. **Named Composer & Regional Encyclopedia Themes (`#622`–`#641`, 20 themes)**:
   - `Barulin1`, `Barulin2`, `BarulinB2`, `Mackenzie`, `Kniest`, `Ventura`, `JonssonCycle`, `BuenosAires`, `Torngren`, `Onitiu`, `Amazon`, `Velikij`, `Leibovici`, `SurkovSlesarenko`, `Peris`, `BretonAdverse`, `Siegfried`, `Ekstrom`, `MonrealPeugeot`, `MonrealMichel`
10. **Additional Encyclopedia & Multi-Phase Synthesis Themes (`#642`–`#661`, 20 themes)**:
    - `KingsNietvelt`, `Hochberger`, `Michel`, `WhiteGamage`, `Nesic`, `Bouttier`, `Salamanca`, `Volga`, `EllermanMakihovi`, `AreaClearkeeping`, `Monkey`, `WhiteOrganPipes`, `BorosPlachuttaLatvian`, `AntiMoscow`, `KopaevReciprocal`, `DombroZagoruiko`, `ShedeyLacny`, `UraniaDoubled`, `VolgogradDouble`, `CompleteShedeyCycle`

Representative Batch 17 Thema specifications:
```thema
// Theme A (Good Companion): Key creates double threat on the same square, separated when a Black piece pins one White attacker in turn
key K (AB) [A B]
where A.to == B.to, A.from != B.from, same_piece(a, b), a.to != b.to
with -match_threat_count

// Baku Novotny: White sacrifice on intersection of R & B lines, where one Black capture is a check
def [a:R:x@K:+ b:B:x@K]
key K (XY) [A B]
with -match_threat_count

// Zappas theme: Two tries each carry a double threat and are refuted by two defenses; the key threatens a third mate and answers those two defenses with the four try threats
try (AB) [! _]
try (CD) [_ !]
key (E) [A C]
with -match_threat_count

// Phoenix: Key sacrifices a White piece (Q, R, B, or N), and after Black captures it, a White pawn promotes to the exact same piece type
def [a:x@K]
key K:Q|R|B|N [A:P:=]
where A.promotion == K.role

// Ambush Key (King-field ambush): Zugzwang slider key moves behind an obstacle piece aiming into the Black King's field
key K [A]
where threat_count() == 0, K.slider, A.from != K.to, A.to != a.from, !collinear(K.from, K.to, a.from), ray_clear(K.to, a.from), !collinear(K.to, a.from, a.to),
  (between(a.from, K.to, BK) || between(a.from, K.to, BK.north) || between(a.from, K.to, BK.south) || between(a.from, K.to, BK.east) || between(a.from, K.to, BK.west) || between(a.from, K.to, BK.ne) || between(a.from, K.to, BK.nw) || between(a.from, K.to, BK.se) || between(a.from, K.to, BK.sw)),
  ((K.role in {'R', 'Q'} && (K.to.file == a.from.file || K.to.rank == a.from.rank)) || (K.role in {'B', 'Q'} && K.to.file != a.from.file && K.to.rank != a.from.rank))

// Zhuravlev theme: Try 1.C? carries double threat (2.A#, 2.B#); Phase 2 plays 1.B threatening 2.C# with variation mate 1...a 2.A#
try C (AB)
+any B (C) [A]
with -match_threat_count -match_mate_count -capture_try_piece -single_refutation -refutation_is_check
```


---

*Thema Specification Version 1.0*