#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 (Lessons 1–7), then keep the

Language Reference and Primitives at hand.

#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 — THeme & Effects Matrix Architecture.
• 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):

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):

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):

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:

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:

// 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:

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:

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:

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:

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:

// 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:

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

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:

// 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)

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:

<RowType> <PhaseMove>? (<Threat>)? [ <VariationMates...> ]

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:

  ^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):

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:

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)

Inline Cell Shorthand Examples:

// 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:

   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)

1. 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.

1. 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.

1. 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)

1. Chess-Domain Shorthands:

#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

#Tactical & Mate Quality Dot-Properties (Usable on Single Moves or Tuples (a, b, c).prop)

#Relational Move Methods (m.method(...))

#Square Properties & Special Identifiers

Properties on squares (sq.property):

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:

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 { ... }:

// 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)

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:

// 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:

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:

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

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

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

// 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).

1. 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.

1. 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.

1. 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.

1. 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:

   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.

1. 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

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:

#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!

1. Set Play Phases: Formatted with set play prefix * and variations:

   * 1...Re5 2.Nf7# | 1...Be5 2.Qd3#

1. 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

// 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}"

// 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).

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.

where between(a.to, b.from, BK)

#distance(sq1, sq2) -> int

Chebyshev distance (King move distance) between two squares: $\max(|\Delta f|, |\Delta r|)$.

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.

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.

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:

// 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()).

// 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:

// 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.

1. 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.

1. 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.

1. 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.

1. 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.

1. 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).

1. 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 (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.

1. 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.

1. 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.

1. 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.

1. Use Comma-Separated where Checklists:

Separate top-level conditions in where with , (or &&) for clean, readable multi-line specs.

1. Use Set Comparisons or Shorthands for Order-Invariant Roles:

   // 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(...).

1. 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).

1. 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

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

#8.2 Grimshaw

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

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

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

any (AB)
any (A)
any (B)

#8.4b Switchback & Umnov

// 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)

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)

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

// 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

// 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)

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)

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:

key (T) [T B]
where same_piece(a, b),
  (b.to != B.to || pinned_to(b.to, WK)),
  b.unguards(B)

• General-mate Somov:

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)

// 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)

// 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

// 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

// 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)

// 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

1. Interference, Novotny, Grimshaw & Valve Variants (12 themes):

• SilentNovotny, CheckNovotny, PawnNovotny, CaptureNovotny, ThreatGrimshaw, TripleGrimshaw, SetGrimshaw, TryGrimshaw, DoubleValve, DoubleBivalve, WhiteValve, MutualSelfObstruction

1. Multi-Phase & Changed/Transferred Mate Matrix Themes (12 themes):

• TripleDombrovskis, TripleHannelius, TripleLeGrand, TriplePseudoLeGrand, DoubleBanny, DoubleLacny, DoubleRudenko, QuadrupleChangedMates, SetChangedPlusAddedMate, ReciprocalTransferredMates, TryThreatBecomesKey, KeyBecomesTryThreat

1. Pinning, Unpinning & Half-Pin Family (10 themes):

• DirectWhiteUnpin, IndirectWhiteUnpin, DirectBlackUnpin, IndirectBlackUnpin, WhiteSelfPin, BlackSelfPin, DoubleHalfPin, CrossPin, PinReplacement, SchiffmannDefenseI

1. Battery & Masked Line Family (10 themes):

• DoubleDirectBattery, DoubleIndirectBattery, RoyalBattery, BlackBatteryCreation, MaskedBatteryKey, OrthogonalBatteryMates, DiagonalBatteryMates, AntiBatteryDefense, PawnBatteryMate, PromotionBatteryMate, SwitchbackBatteryMate

1. Pawn Play, Promotion & En Passant Family (9 themes):

• Allumwandlung, BabsonTask, TriplePromotion, DoubleUnderpromotion, KnightPromotions, RookPromotions, BishopPromotions, MutualEnPassant, ExcelsiorStep

1. Geometrical, Task & Star/Wheel Family (10 themes):

• BlackQueenWheel, WhiteRookCross, WhiteBishopCross, BlackRookCross, BlackBishopCross, TripleSwitchback, QuadrupleSwitchback, DoubleCornerToCorner, MaximumFlightTask, PendulumTheme

1. King Flights, Give-and-Take & Sacrifices (10 themes):

• GiveAndTakeTwo, GiveAndTakeThree, FourFlightKey, ThreeCaptureFlights, QueenSacrifice, BishopSacrifice, KnightSacrifice, DoubleSacrificeKey, QuadrupleSelfBlock, RoyalSelfBlock

1. Correction, Focal & Dual Avoidance Family (8 themes):

• TripleBlackCorrection, SecondaryWhiteCorrection, KnightCorrection, BishopCorrection, RookCorrection, QueenCorrection, FocalInterference, DualSeparationBySelfBlock

1. Mate Aesthetics, Twins & Structural Conditions (8 themes):

• MiniaturesSeven, UltraMiniature, SymmetricalPosition, DoubleModelMate, TripleModelMate, DoublePureMate, DoubleMirrorMate, DoublePinMate, TriplePinMate

Representative Batch 16 Thema specifications:

// 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

1. 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

1. 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

1. 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

1. 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

1. 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

1. 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

1. 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

1. 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

1. 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:

// 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