diff --git a/Bib.lean b/Bib.lean
index a3ec26e..7ba801c 100644
--- a/Bib.lean
+++ b/Bib.lean
@@ -50,6 +50,12 @@ def love2026 : Article where
   number  := inlines!""
   url     := "https://github.com/lean-forward/logical_verification_2026"
 
+def danielsson2010 : InProceedings where
+  title     := inlines!"Total Parser Combinators"
+  authors   := #[inlines!"Nils Anders Danielsson"]
+  year      := 2010
+  booktitle := inlines!"Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP 2010)"
+
 def FPiL : Article where
   title   := inlines!"Functional Programming in Lean"
   authors := #[inlines!"David Thrane Christiansen"]
diff --git a/Book.lean b/Book.lean
index 8f9478a..b9c7212 100644
--- a/Book.lean
+++ b/Book.lean
@@ -10,6 +10,7 @@ import CSwL.Morphology
 import CSwL.InfEngine
 import CSwL.ModelChecking
 import CSwL.Composition
+import CSwL.Parsing
 
 import VersoManual
 
@@ -37,3 +38,4 @@ set_option verso.code.warnLineLength 80
 {include CSwL.InfEngine}
 {include CSwL.ModelChecking}
 {include CSwL.Composition}
+{include CSwL.Parsing}
diff --git a/CSwFP.yaml b/CSwFP.yaml
index eff5aee..100b86c 100644
--- a/CSwFP.yaml
+++ b/CSwFP.yaml
@@ -158,6 +158,25 @@ exercises:
     7.26 (p. 180): deferred with 7.7 (issue 43)
     7.27 (p. 181): deferred with 7.7 (issue 43)
     7.28 (p. 182): deferred with 7.7 (issue 43)
+  CSwFP/9:
+    9.1 (p. 208): imm-dominance
+    9.2 (p. 210): c-command-dominance
+    9.3 (p. 210): mutual-c-command
+    9.4 (p. 211): imm-precedence
+    9.5 (p. 211): command
+    9.6 (p. 214): split-nonempty
+    9.7 (p. 214): absorbed into the cue on termination, which says why left
+      recursion is no trouble for recognition by splitting
+    9.8 (p. 217): symbol-satisfy
+    9.9 (p. 222): absorbed into the closing cue of parser-combinators, which
+      says why left recursion makes a parser loop
+    9.10 (p. 237): TODO
+    9.11 (p. 241): TODO
+    9.12 (p. 244): TODO
+    9.13 (p. 246): TODO
+    9.14 (p. 248): TODO
+    9.15 (p. 257): TODO
+    9.16 (p. 259): TODO
 
 original:
   IntroL.lean: [sum-of-squares, sum-to, sum-list, count-zeros]
@@ -205,6 +224,7 @@ original:
     - left-mon-pattern # from the prose on ↑MON and ↓MON in 7.2, "left to the reader"
     - lang-and-or     # from the prose on quantifier automata in 7.2
     - all-kstar       # from the prose in 7.2, "all corresponds to the regular language 1∗"
+  Parsing/Combinators.lean: [parse-many-as]
 
 depends:
   bangu-proof: bangu-form
@@ -336,7 +356,17 @@ sections:
         reach looked of little use (issue 43).
     7.8 Further Reading: omitted
   CSwFP/8 Extension and Intension: not yet taken up
-  CSwFP/9 Parsing: not yet taken up
+  CSwFP/9:
+    9.1 Talking About Parse Trees: Parsing
+    9.2 Recognizing and Parsing Context-Free Languages: Parsing
+    9.3 Parsers and Parser Combinators: Parsing, without the Mastermind
+      parser, since Mastermind is dropped with 5.4
+    9.4 Features and Categories: Parsing, not yet written
+    9.5 Lexical Lookup and Scanning: Parsing, not yet written
+    9.6 Parsing Categories: Parsing, not yet written
+    9.7 Handling Extractions: Parsing, not yet written
+    9.8 Adding Semantics: Parsing, not yet written
+    9.9 Further Reading: omitted
   CSwFP/10 Handling Relations and Scoping: not yet taken up
   CSwFP/11 Continuation Passing Style Semantics: not yet taken up
   CSwFP/12 Discourse Representation and Context: not yet taken up
diff --git a/CSwL/Parsing.lean b/CSwL/Parsing.lean
new file mode 100644
index 0000000..f17cd99
--- /dev/null
+++ b/CSwL/Parsing.lean
@@ -0,0 +1,50 @@
+import CSwLMeta
+import Bib
+import CSwL.Parsing.ParseTrees
+import CSwL.Parsing.Recognition
+import CSwL.Parsing.Combinators
+
+open Verso.Genre Manual
+open CSwLMeta
+
+#doc (Manual) "Análise sintática" =>
+%%%
+tag := "Parsing"
+file := "Parsing"
+%%%
+
+:::dev NOW
+Plan. The headings follow CSwFP/9.1–9.8 (9.9, further reading, is
+omitted). Sections are written `terse` first (see `STYLE-CODE.md`).
+
+- 9.1: `ParseTree α β`, positions, and the tree relations as lists of
+  pairs; dominance with Lean's `<+:`.
+- 9.2: recognition and parsing by splitting, for the palindrome grammar,
+  total by `termination_by`; agreement with Mathlib's `List.Palindrome`
+  proved for every word over `{a, b, c}`.
+- 9.3: list-of-successes parsers as `StateT (List α) List`, with
+  Mathlib's `Monad`/`Alternative List`; recursive parsers are
+  `partial def`. Lean's `Std.Internal.Parsec` returns one result, not
+  all parses; it can serve the lexer of 9.5.
+- 9.4–9.8: to plan. The representation of `Cat` is tied to issue 42.
+:::
+
+:::terse
+- Até aqui as árvores sintáticas eram construídas à mão. Agora o caminho
+  é o inverso: partir de uma sequência de palavras e encontrar as árvores
+  que a gramática lhe atribui.
+- Primeiro, relações entre os nós de uma árvore. Depois, reconhecer e
+  analisar linguagens livres de contexto.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate the CSwFP/9 summary.
+:::
+::::
+
+{include 1 CSwL.Parsing.ParseTrees}
+
+{include 1 CSwL.Parsing.Recognition}
+
+{include 1 CSwL.Parsing.Combinators}
diff --git a/CSwL/Parsing/Combinators.lean b/CSwL/Parsing/Combinators.lean
new file mode 100644
index 0000000..d5c9434
--- /dev/null
+++ b/CSwL/Parsing/Combinators.lean
@@ -0,0 +1,420 @@
+import CSwLMeta
+import Bib
+import CSwL.Parsing.ParseTrees
+import Mathlib.Data.List.Monad
+
+open Verso.Genre Manual
+open CSwLMeta
+
+#doc (Manual) "Parsers e combinadores de parsers" =>
+%%%
+tag := "parser-combinators"
+file := "Combinators"
+%%%
+
+```lean
+namespace Parsing
+```
+
+:::terse
+- Objetivo: um método geral para analisar com qualquer gramática livre
+  de contexto, em que o código do parser tem a forma das regras da
+  gramática.
+- Basta tratar três coisas: os símbolos terminais, a escolha `|` entre
+  regras, e a sequência B₁ ⋯ Bₙ do lado direito de uma regra.
+- Um parser lê um *prefixo* da entrada e devolve todos os pares
+  (resultado, resto da entrada) que consegue construir. A lista vazia é
+  a falha; mais de um par é ambiguidade.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.3, from the start to the type of a parser.
+:::
+::::
+
+:::terse
+- Em Lean, esse tipo já existe: `StateT (List α) List β`. O estado é o
+  resto da entrada, e `List` dá as várias respostas.
+- O `example` mostra que os dois tipos são o mesmo, por definição: um
+  `Parser` é uma função, e pode ser escrito como tal.
+- Usar `StateT` dá de graça as operações de que vamos precisar, com a
+  notação que o Lean já tem para elas: `pure`, `failure`, `<|>`, `<$>` e
+  `do`.
+:::
+
+```lean
+abbrev Parser (α β : Type) := StateT (List α) List β
+
+example {α β : Type} :
+    Parser α β = (List α → List (β × List α)) := rfl
+```
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.3, from "The parser uses the grammar rules…" to
+Figure 9.1 and the paragraph after it.
+:::
+::::
+
+:::terse
+- Os dois parsers mais simples não leem nada. O parser `pure r` sempre
+  dá certo, com o resultado `r`. O parser `failure` sempre falha.
+- A expressão `p.run xs` aplica o parser `p` à entrada `xs`.
+:::
+
+```lean
+#eval (pure 1 : Parser Char Nat).run "ab".toList
+#eval (failure : Parser Char Nat).run "ab".toList
+```
+
+:::terse
+- O parser `symbol c` reconhece o símbolo `c` no início da entrada;
+  `token cs`, a lista de símbolos `cs`; `satisfy p`, um símbolo
+  qualquer que tenha a propriedade `p`.
+- Os três são escritos diretamente como funções sobre a entrada.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.3, from "Two very elementary parsers…" to the
+definition of `digit`.
+:::
+::::
+
+```lean
+def symbol {α : Type} [BEq α] (c : α) : Parser α α
+  | x :: xs => if x == c then [(x, xs)] else []
+  | [] => []
+
+def token {α : Type} [BEq α] (cs : List α)
+  : Parser α (List α)
+  | xs =>
+    if cs == xs.take cs.length then
+     [(cs, xs.drop cs.length)]
+    else []
+
+def satisfy {α : Type} (p : α → Bool) : Parser α α
+  | x :: xs => if p x then [(x, xs)] else []
+  | [] => []
+
+def digit : Parser Char Char := satisfy Char.isDigit
+
+#eval (symbol 'a').run "ab".toList
+#eval (token "ab".toList).run "abc".toList
+#eval digit.run "42".toList
+```
+
+::::exercise (rating := 1) (name := "symbol-satisfy")
+Defina `symbol'`, que faz o mesmo que `symbol`, usando `satisfy`.
+
+```lean
+def symbol' {α : Type} [BEq α] (c : α) : Parser α α :=
+  solution!(satisfy (· == c))
+
+theorem symbol'_eq_symbol {α : Type} [BEq α] (c : α)
+    (xs : List α) : symbol' c xs = symbol c xs := by
+  solution!
+   cases xs <;> rfl
+```
+::::
+
+:::terse
+- Os parsers elementares servem para os terminais. Com terminais
+  `String`, a palavra *Alice* é `symbol "Alice"`; com terminais `Char`,
+  é `token "Alice".toList`.
+- Combinadores de parsers são funções que constroem parsers a partir de
+  outros parsers.
+- O combinador `just` filtra as análises: `just p` só aceita as de `p`
+  que consomem a entrada toda.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.3, from "Now, these elementary parsers…" to the
+definition of `just`.
+:::
+::::
+
+```lean
+def just {α β : Type} (p : Parser α β) : Parser α β
+ | xs => (p xs).filter fun (_, ys) => ys.isEmpty
+```
+
+:::terse
+- A escolha é `p <|> q`: todas as análises de `p`, seguidas de todas as
+  de `q`. O `example` mostra que isso é a concatenação das listas.
+- VP → smiled | laughed vira `symbol "smiled" <|> symbol "laughed"`.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.3, from "For parsing one of our grammars…" to
+the parser for VP.
+:::
+::::
+
+```lean
+example {α β : Type} (p q : Parser α β) (xs : List α) :
+    (p <|> q) xs = p xs ++ q xs := rfl
+```
+
+:::terse
+- A sequência é um bloco `do`. Em `let r₁ ← p`, o parser `p` lê o início
+  da entrada e dá o resultado `r₁`; o parser da linha seguinte começa no
+  resto que `p` deixou.
+- Cada análise de `p` continua separadamente. O `example` mostra a
+  operação por trás do `do`, `>>=`: um `flatMap` sobre as análises de
+  `p`.
+- Com isso, a gramática da figura vira uma definição por regra; aqui, o
+  resultado é só a lista das palavras lidas.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.3, from "Next, what to do with rules like
+S → NP VP?" to the definitions of `pS`, …, `pN` and the paragraph
+after them.
+:::
+::::
+
+```lean
+example {α β γ : Type} (p : Parser α β) (q : β → Parser α γ)
+    (xs : List α) :
+    (p >>= q) xs =
+      (p xs).flatMap fun (r, ys) => q r ys := rfl
+
+def pD : Parser String String :=
+  symbol "every" <|> symbol "some" <|> symbol "no"
+
+def pN : Parser String String :=
+  symbol "dwarf" <|> symbol "wizard"
+
+def pVP : Parser String String :=
+  symbol "smiled" <|> symbol "laughed"
+
+def pNP : Parser String (List String) :=
+  (do
+    let w ← symbol "Alice" <|> symbol "Dorothy"
+    return [w]) <|>
+  (do
+    let d ← pD
+    let n ← pN
+    return [d, n])
+
+def pS : Parser String (List String) := do
+  let np ← pNP
+  let vp ← pVP
+  return np ++ [vp]
+
+#eval pS.run ["every", "wizard", "smiled"]
+#eval pS.run ["Alice", "laughed", "loudly"]
+```
+
+:::terse
+- O parser `f <$> p` aplica `f` ao resultado de cada análise de `p`,
+  sem mexer no resto da entrada.
+- O parser `digitize` lê um dígito e devolve o número que ele
+  representa.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.3, from "However, we are not quite there
+yet…" to the definition of `digitize`.
+:::
+::::
+
+```lean
+example {α β γ : Type} (f : β → γ) (p : Parser α β)
+    (xs : List α) :
+    (f <$> p) xs =
+      (p xs).flatMap fun (r, ys) => [(f r, ys)] := rfl
+
+def digitize : Parser Char Nat :=
+  (fun c => c.toNat - '0'.toNat) <$> digit
+
+#eval digitize.run "42".toList
+```
+
+:::terse
+- Agora, parsers que constroem árvores: `Parser α (ParseTree α β)`,
+  com terminais `α` nas folhas e não terminais `β` nos nós.
+- O parser `epsilonT` não lê nada e dá a árvore vazia. O parser
+  `symbolT s` lê o terminal `s` e dá uma folha.
+- A função `collect` aplica uma lista de parsers um depois do outro e
+  junta os resultados numa lista. A função `parseAs` faz disso um nó:
+  `parseAs A ps` é a regra A → B₁ ⋯ Bₙ, com `ps` os parsers de B₁, …,
+  Bₙ, e o nó tem rótulo `A`.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.3, from "We will use <$> for constructing parse
+trees." to the definition of `parseAs` and the paragraph after it.
+:::
+::::
+
+```lean
+def epsilonT {α β : Type} : Parser α (ParseTree α β) :=
+  pure .ep
+
+def symbolT {α β : Type} [BEq α] (s : α) :
+    Parser α (ParseTree α β) :=
+  .leaf <$> symbol s
+
+def collect {α β : Type} :
+    List (Parser α β) → Parser α (List β)
+  | [] => pure []
+  | p :: ps => do
+    let r ← p
+    let rs ← collect ps
+    return r :: rs
+
+def parseAs {α β : Type} (label : β)
+    (ps : List (Parser α (ParseTree α β))) :
+    Parser α (ParseTree α β) :=
+  .branch label <$> collect ps
+```
+
+:::terse
+- A gramática de novo, agora com árvores: um parser por categoria, uma
+  linha por regra.
+:::
+
+```lean
+def det : Parser String (ParseTree String Char) :=
+  symbolT "every" <|> symbolT "some" <|> symbolT "no"
+
+def cn : Parser String (ParseTree String Char) :=
+  symbolT "man" <|> symbolT "woman"
+
+def vp : Parser String (ParseTree String Char) :=
+  symbolT "smiled" <|> symbolT "laughed"
+
+def np : Parser String (ParseTree String Char) :=
+  symbolT "Alice" <|> symbolT "Dorothy"
+  <|> parseAs 'N' [det, cn]
+
+def sent : Parser String (ParseTree String Char) :=
+  parseAs 'S' [np, vp]
+
+#eval (just sent).run ["every", "man", "laughed"] |>.map
+  (toString ·.1)
+```
+
+:::terse
+- Os palíndromos outra vez, agora uma linha por regra da gramática. Não
+  há mais divisão da entrada: cada parser lê o que precisa e deixa o
+  resto para o seguinte.
+- O parser `palindrome` chama a si mesmo, mas sobre um resto da entrada
+  que o Lean não vê: ele está escondido dentro do `StateT`. Por isso a
+  definição é `partial def`. O Lean aceita a definição sem provar que
+  ela termina, mas em troca não conhece a equação que a define: nada
+  que dependa do que `palindrome` faz pode ser provado.
+- Sem `just`, o parser também devolve as análises de prefixos da
+  entrada, com o seu resto.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.3, the sentences introducing the two parsers
+above and the palindrome parser.
+:::
+::::
+
+```lean
+partial def palindrome :
+    Parser Char (ParseTree Char Char) :=
+  epsilonT <|> symbolT 'a' <|> symbolT 'b' <|> symbolT 'c'
+  <|> parseAs 'A' [symbolT 'a', palindrome, symbolT 'a']
+  <|> parseAs 'A' [symbolT 'b', palindrome, symbolT 'b']
+  <|> parseAs 'A' [symbolT 'c', palindrome, symbolT 'c']
+
+#eval (just palindrome).run "abcba".toList |>.map
+  (toString ·.1)
+#eval palindrome.run "aba".toList |>.map fun (t, ys) =>
+  (toString t, String.ofList ys)
+```
+
+:::terse
+- O combinador `many` faz a repetição `{A}` das gramáticas em EBNF:
+  `many p` aplica `p` quantas vezes for possível, inclusive nenhuma. A análise mais longa vem
+  primeiro.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.3, the sentences introducing `many`.
+:::
+::::
+
+```lean
+partial def many {α β : Type} (p : Parser α β) :
+    Parser α (List β) :=
+  (do
+    let r ← p
+    let rs ← many p
+    return r :: rs) <|> pure []
+
+#eval (many (symbol 'a')).run "aab".toList
+```
+
+::::exercise (rating := 1) (name := "parse-many-as")
+Para ter uma árvore, a repetição precisa ficar sob um rótulo. Defina
+`parseManyAs l p`, que aplica `p` quantas vezes for possível e põe as
+árvores obtidas sob um nó com rótulo `l`. Confira o resultado com
+`adjectives`, uma sequência de adjetivos sob o rótulo `J`.
+
+```lean
+def parseManyAs {α β : Type} (l : β)
+    (p : Parser α (ParseTree α β)) :
+    Parser α (ParseTree α β) :=
+  solution!(.branch l <$> many p)
+
+def adjectives : Parser String (ParseTree String Char) :=
+  parseManyAs 'J' (symbolT "happy" <|> symbolT "evil")
+
+theorem adjectives_happy_evil :
+    ((adjectives.run ["happy", "evil", "dwarf"]).map
+      fun (t, ys) => (toString t, ys)) =
+    [("[.J happy evil]", ["dwarf"]),
+     ("[.J happy]", ["evil", "dwarf"]),
+     ("[.J ]", ["happy", "evil", "dwarf"])] := by
+  solution!
+   native_decide
+```
+::::
+
+:::terse
+- Em resumo: um terminal t vira `symbolT t`, um não terminal A vira
+  `parseAs A`, a escolha vira `<|>`, e o lado direito de uma regra vira a
+  lista de parsers passada a `parseAs`.
+- O método não serve para toda gramática livre de contexto. Numa regra
+  recursiva à esquerda, A → A T, o parser de A chama a si mesmo antes de
+  ler qualquer símbolo, sobre a mesma entrada, e nunca para.
+- O parser `leftRec` abaixo é aceito, por ser `partial def`, mas não
+  deve ser rodado: cada chamada abre outra, até esgotar a pilha, e o Lean para
+  com um erro de recursão profunda.
+- O reconhecedor por divisão não tinha esse problema, desde que as
+  divisões com pedaço vazio fossem descartadas: aí cada chamada recebia
+  um pedaço menor da entrada, e o Lean exigia uma prova disso.
+- Há combinadores de parsers que garantem a terminação e aceitam
+  recursão à esquerda; ver {citep Bib.danielsson2010}[].
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.3, the closing summary ("To sum up, …"),
+without the sentence on `parseManyAs`.
+:::
+::::
+
+```lean
+partial def leftRec : Parser Char (ParseTree Char Char) :=
+  parseAs 'A' [leftRec, symbolT 'a'] <|> symbolT 'b'
+```
+
+```lean
+end Parsing
+```
diff --git a/CSwL/Parsing/ParseTrees.lean b/CSwL/Parsing/ParseTrees.lean
new file mode 100644
index 0000000..fb2d4f7
--- /dev/null
+++ b/CSwL/Parsing/ParseTrees.lean
@@ -0,0 +1,430 @@
+import CSwLMeta
+import Bib
+
+open Verso.Genre Manual
+open CSwLMeta
+
+#doc (Manual) "Falando de árvores sintáticas" =>
+%%%
+tag := "parse-trees"
+file := "ParseTrees"
+%%%
+
+```lean
+namespace Parsing
+```
+
+:::terse
+- Uma árvore sintática tem informação lexical nas folhas e informação
+  sintática nos nós internos.
+- O tipo deixa as duas em aberto: `α` para as folhas, `β` para os rótulos
+  dos nós. O construtor `ep` é a árvore vazia.
+- Um `branch` guarda a *lista* das suas subárvores, por isso cada nó pode
+  ter quantas filhas quiser.
+- A função `toText` escreve a árvore entre colchetes, com o rótulo depois
+  de `[.` e as filhas separadas por espaços.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.1, from the start to the example tree.
+:::
+::::
+
+```lean
+inductive ParseTree (α β : Type) where
+  | ep
+  | leaf (a : α)
+  | branch (b : β) (ts : List (ParseTree α β))
+  deriving Repr, BEq
+
+def ParseTree.toText {α β : Type}
+    [ToString α] [ToString β] : ParseTree α β → String
+  | .ep => "[]"
+  | .leaf a => toString a
+  | .branch b ts =>
+    "[." ++ toString b ++ " " ++
+      " ".intercalate (ts.map toText) ++ "]"
+
+instance {α β : Type} [ToString α] [ToString β] :
+    ToString (ParseTree α β) :=
+  ⟨ParseTree.toText⟩
+
+def snowWhite : ParseTree String String :=
+  .branch "S"
+    [.branch "NP" [.leaf "Snow White"],
+     .branch "VP" [.branch "TV" [.leaf "loved"],
+                   .branch "NP" [.leaf "the dwarfs"]]]
+
+#eval IO.println snowWhite
+```
+
+:::terse
+- Uma mesma subárvore pode ocorrer mais de uma vez numa árvore: em
+  *Snow White loved Snow White*, `[NP Snow White]` ocorre duas vezes.
+- Para apontar uma ocorrência usamos uma *posição*: a lista dos índices
+  das filhas no caminho desde a raiz, contando a partir de 0. A raiz é a
+  posição `[]`.
+- A função `pos` lista todas as posições. Como a recursão desce por uma
+  lista de subárvores, ela usa uma função auxiliar local, definida com
+  `let rec`: `posFrom i ts` dá as posições das árvores de `ts`, a
+  primeira com índice `i`.
+- A função `subtree` dá subárvores: `subtree t p` é a de `t` na posição
+  `p`. Numa posição que
+  não existe em `t`, devolve `ep`; isso nunca acontece com as posições
+  de `pos t`.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.1, from "In this first section, we will develop…"
+to the definition of `subtrees`.
+:::
+::::
+
+```lean
+abbrev Pos := List Nat
+
+def pos {α β : Type} (p : ParseTree α β) : List Pos :=
+  let rec posFrom {α β : Type} :
+    Nat → List (ParseTree α β) → List Pos
+   | _, [] => []
+   | i, t :: ts =>
+     (pos t).map (i :: ·) ++ posFrom (i + 1) ts
+  match p with
+  | .ep => [[]]
+  | .leaf _ => [[]]
+  | .branch _ ts => [] :: posFrom 0 ts
+
+#eval pos snowWhite
+
+def subtree {α β : Type} :
+  ParseTree α β → Pos → ParseTree α β
+  | t, [] => t
+  | .branch _ ts, i :: is =>
+    match ts[i]? with
+    | some t => subtree t is
+    | none => .ep
+  | _, _ :: _ => .ep
+
+def subtrees {α β : Type} (t : ParseTree α β)
+  : List (ParseTree α β) :=
+  (pos t).map (subtree t)
+
+#eval IO.println (subtree snowWhite [1])
+```
+
+:::terse
+- Uma posição `p` *domina* `q` quando `p` é prefixo de `q`: a subárvore
+  em `q` está dentro da subárvore em `p`. Toda posição domina a si mesma;
+  a dominância *própria* exclui esse caso.
+- Em Lean, `p <+: q` diz que `p` é prefixo de `q`. É uma proposição
+  decidível, então pode ser usada como `Bool` num `filter`.
+- As relações sobre as posições de uma árvore são listas de pares.
+  A função `posPairs` lista todos os pares de posições; cada relação
+  filtra os que lhe interessam.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.1, from "If p, q are tree positions…" to the
+definition of `dominance`.
+:::
+::::
+
+```lean
+def posPairs {α β : Type} (t : ParseTree α β) :
+    List (Pos × Pos) :=
+  (pos t).flatMap fun p => (pos t).map fun q => (p, q)
+
+def properDominance {α β : Type} (t : ParseTree α β) :
+    List (Pos × Pos) :=
+  (posPairs t).filter fun (p, q) => p ≠ q && p <+: q
+
+def dominance {α β : Type} (t : ParseTree α β) :
+    List (Pos × Pos) :=
+  (posPairs t).filter fun (p, q) => p <+: q
+
+#eval properDominance snowWhite
+```
+
+::::exercise (rating := 2) (name := "imm-dominance")
+A posição `p` *domina imediatamente* `q` quando `p` domina propriamente
+`q` e não há posição `r`, diferente das duas, tal que `p` domina `r` e
+`r` domina `q`. Defina `immDominance` e confira o resultado na árvore
+`snowWhite`.
+
+```lean
+def immDominance {α β : Type} (t : ParseTree α β) :
+    List (Pos × Pos) :=
+  solution!(
+    (properDominance t).filter fun (p, q) =>
+      !(pos t).any fun r =>
+        r != p && r != q && p <+: r && r <+: q)
+
+theorem immDominance_snowWhite :
+    immDominance snowWhite =
+      [([], [0]), ([], [1]), ([0], [0, 0]), ([1], [1, 0]),
+       ([1], [1, 1]), ([1, 0], [1, 0, 0]),
+       ([1, 1], [1, 1, 0])] := by
+  solution!
+   decide
+```
+::::
+
+:::terse
+- Duas posições são *irmãs* quando são filhas diferentes da mesma mãe:
+  coincidem em tudo, menos no último índice.
+- O *c-comando* é a composição de duas relações: `p` c-comanda `q` quando
+  uma irmã de `p` domina `q`.
+- A composição é `relComp`: `relComp r s` liga `x` a `z` quando `r`
+  liga `x` a algum `y` e `s` liga esse `y` a `z`. A função `eraseDups`
+  tira os pares repetidos.
+- Na árvore `snowWhite`, o sujeito `[0]` c-comanda tudo o que está dentro
+  do VP; o objeto `[1, 1]` c-comanda o verbo `[1, 0]`, mas não o sujeito.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.1, from "Two positions p, q are sister positions…"
+to the c-command relation of the example tree.
+:::
+::::
+
+```lean
+def sisters : Pos → Pos → Bool
+  | [i], [j] => i != j
+  | i :: is, j :: js => i == j && sisters is js
+  | _, _ => false
+
+def sisterhood {α β : Type} (t : ParseTree α β) :
+    List (Pos × Pos) :=
+  (posPairs t).filter fun (p, q) => sisters p q
+
+#eval sisterhood snowWhite
+
+def relComp {γ : Type} [BEq γ] (r s : List (γ × γ)) :
+    List (γ × γ) :=
+  (r.flatMap fun (x, y) =>
+    (s.filter fun (w, _) => y == w).map fun (_, z) =>
+      (x, z)).eraseDups
+
+def cCommand {α β : Type} (t : ParseTree α β) :
+    List (Pos × Pos) :=
+  relComp (sisterhood t) (dominance t)
+
+#eval dominance snowWhite
+#eval cCommand snowWhite
+```
+
+:::terse
+- Uma posição *ramifica* quando tem pelo menos duas filhas. Na árvore
+  `snowWhite`, só a raiz e o VP ramificam.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.1, the branching positions.
+:::
+::::
+
+```lean
+def branchingPos {α β : Type} (t : ParseTree α β) :
+    List Pos :=
+  let ps := pos t
+  ps.filter fun p =>
+    ps.contains (p ++ [0]) && ps.contains (p ++ [1])
+
+#eval branchingPos snowWhite
+```
+
+:::terse
+- Os fatos sobre o c-comando valem para quaisquer posições, não só para
+  as de uma árvore. Por isso os teoremas abaixo falam de posições.
+- Dois lemas sobre irmãs: elas têm o mesmo comprimento, e nenhuma é
+  prefixo da outra.
+:::
+
+:::details "Dois lemas sobre posições irmãs"
+```lean
+theorem sisters_length (p r : Pos)
+    (h : sisters p r = true) : p.length = r.length := by
+  induction p generalizing r with
+  | nil => simp [sisters] at h
+  | cons i is ih =>
+    cases r with
+    | nil => simp [sisters] at h
+    | cons j js =>
+      cases is with
+      | nil =>
+        cases js with
+        | nil => rfl
+        | cons k ks => simp [sisters] at h
+      | cons i' is' =>
+        cases js with
+        | nil => simp [sisters] at h
+        | cons k ks =>
+          simp only [sisters, Bool.and_eq_true] at h
+          simp [ih _ h.2]
+
+theorem sisters_not_prefix (p r : Pos)
+    (h : sisters p r = true) : ¬ p <+: r := by
+  induction p generalizing r with
+  | nil => simp [sisters] at h
+  | cons i is ih =>
+    cases r with
+    | nil => simp [sisters] at h
+    | cons j js =>
+      cases is with
+      | nil =>
+        cases js with
+        | nil => simp_all [sisters]
+        | cons k ks => simp_all [sisters]
+      | cons i' is' =>
+        cases js with
+        | nil => simp [sisters] at h
+        | cons k ks =>
+          simp only [sisters, Bool.and_eq_true,
+            beq_iff_eq] at h
+          obtain ⟨rfl, h⟩ := h
+          rw [List.cons_prefix_cons]
+          intro ⟨_, hp⟩
+          exact ih _ h hp
+```
+:::
+
+::::exercise (rating := 3) (name := "c-command-dominance")
+Suponha que `p` c-comanda `q`: uma irmã `r` de `p` domina `q`. Prove que
+`p` não domina `q` e que `q` não domina `p`.
+
+Dica: um prefixo de `q` que não é mais longo do que outro prefixo de `q`
+é prefixo dele (`List.prefix_of_prefix_length_le`), e um prefixo do mesmo
+comprimento é a própria lista (`List.IsPrefix.eq_of_length`).
+
+```lean
+theorem cCommand_not_dominates (p r q : Pos)
+    (hs : sisters p r = true) (hd : r <+: q) :
+    ¬ p <+: q := by
+  solution!
+   intro hp
+   have hl := sisters_length p r hs
+   have h : p <+: r :=
+     List.prefix_of_prefix_length_le hp hd (by omega)
+   exact sisters_not_prefix p r hs h
+
+theorem cCommand_not_dominated (p r q : Pos)
+    (hs : sisters p r = true) (hd : r <+: q) :
+    ¬ q <+: p := by
+  solution!
+   intro hq
+   have hl := sisters_length p r hs
+   have h1 := hd.length_le
+   have h2 := hq.length_le
+   have hqp : q = p := hq.eq_of_length (by omega)
+   have hrq : r = q := hd.eq_of_length (by omega)
+   rw [hrq, hqp] at hs
+   exact sisters_not_prefix p p hs (List.prefix_refl p)
+```
+::::
+
+::::exercise (rating := 2) (name := "mutual-c-command")
+O c-comando não é simétrico, mas o *c-comando mútuo* é: `p` e `q` se
+c-comandam mutuamente quando `p` c-comanda `q` e `q` c-comanda `p`.
+Defina `mutualCCommand` e confira, na árvore `snowWhite`, que ele coincide
+com a relação de irmãs.
+
+```lean
+def mutualCCommand {α β : Type} (t : ParseTree α β) :
+    List (Pos × Pos) :=
+  solution!(
+    (cCommand t).filter fun (p, q) =>
+      (cCommand t).contains (q, p))
+
+theorem mutualCCommand_snowWhite :
+    mutualCCommand snowWhite = sisterhood snowWhite := by
+  solution!
+   decide
+```
+::::
+
+:::terse
+- Uma posição `p` *precede* `q` quando, no primeiro índice em que
+  diferem, o de `p` é menor. Uma posição não precede as que ela domina.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.1, from "A position p in a syntax tree precedes…"
+to the precedence relation of the example tree.
+:::
+::::
+
+```lean
+def precede : Pos → Pos → Bool
+  | i :: is, j :: js => i < j || (i == j && precede is js)
+  | _, _ => false
+
+def precedence {α β : Type} (t : ParseTree α β) :
+    List (Pos × Pos) :=
+  (posPairs t).filter fun (p, q) => precede p q
+
+#eval precedence snowWhite
+```
+
+::::exercise (rating := 2) (name := "imm-precedence")
+Defina a *precedência imediata*, a partir da precedência, do mesmo modo
+que a dominância imediata foi definida a partir da dominância. Confira o
+resultado na árvore `snowWhite`.
+
+```lean
+def immPrecedence {α β : Type} (t : ParseTree α β) :
+    List (Pos × Pos) :=
+  solution!(
+    (precedence t).filter fun (p, q) =>
+      !(pos t).any fun r => precede p r && precede r q)
+
+theorem immPrecedence_snowWhite :
+    immPrecedence snowWhite =
+      [([0], [1]), ([0], [1, 0]), ([0], [1, 0, 0]),
+       ([0, 0], [1]), ([0, 0], [1, 0]),
+       ([0, 0], [1, 0, 0]), ([1, 0], [1, 1]),
+       ([1, 0], [1, 1, 0]), ([1, 0, 0], [1, 1]),
+       ([1, 0, 0], [1, 1, 0])] := by
+  solution!
+   decide
+```
+::::
+
+:::terse
+- O *comando* é uma noção anterior ao c-comando: `p` comanda `q` quando
+  nenhuma das duas domina a outra e o S mais próximo acima de `p` também
+  domina `q`.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.1, the paragraph on command.
+:::
+::::
+
+::::exercise (rating := 2) (name := "command")
+Defina `command` supondo que o S mais próximo é sempre a raiz da árvore.
+Confira o resultado na árvore `snowWhite`.
+
+```lean
+def command {α β : Type} (t : ParseTree α β) :
+    List (Pos × Pos) :=
+  solution!(
+    (posPairs t).filter fun (p, q) =>
+      !(p <+: q) && !(q <+: p))
+
+theorem command_snowWhite :
+    (command snowWhite).length = 28 := by
+  solution!
+   decide
+```
+::::
+
+```lean
+end Parsing
+```
diff --git a/CSwL/Parsing/Recognition.lean b/CSwL/Parsing/Recognition.lean
new file mode 100644
index 0000000..04ab307
--- /dev/null
+++ b/CSwL/Parsing/Recognition.lean
@@ -0,0 +1,387 @@
+import CSwLMeta
+import Bib
+import CSwL.Parsing.ParseTrees
+import Mathlib.Data.List.Palindrome
+
+open Verso.Genre Manual
+open CSwLMeta
+
+#doc (Manual) "Reconhecendo e analisando linguagens livres de contexto" =>
+%%%
+tag := "cf-recognition"
+file := "Recognition"
+%%%
+
+```lean
+namespace Parsing
+```
+
+:::terse
+- *Reconhecer*: dizer se a gramática gera ou não uma sequência.
+  *Analisar* (*parsing*): dizer também como ela é gerada, isto é, dar as
+  suas árvores sintáticas.
+- O exemplo é a gramática dos palíndromos sobre `{a, b, c}`, as palavras
+  iguais à sua inversa:
+  A → ε | a | b | c | aAa | bAb | cAc.
+- A ideia para qualquer gramática livre de contexto: uma regra com `n`
+  símbolos à direita divide a entrada em `n` pedaços, de todos os modos
+  possíveis, e testa cada pedaço contra o seu símbolo.
+- A função `split2` dá todas as divisões de uma lista em duas;
+  `splitN n`, em `n`.
+- Em Lean. `"Jan".toList` dá a lista de caracteres, e `String.ofList` faz o caminho de volta.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.2, from the start to the definition of `splitN`.
+:::
+::::
+
+```lean
+def split2 {α : Type} : List α → List (List α × List α)
+  | [] => [([], [])]
+  | x :: xs =>
+    ([], x :: xs) ::
+      (split2 xs).map fun (ys, zs) => (x :: ys, zs)
+
+#eval split2 "Jan".toList |>.map
+  λ (a, b) ↦ (String.ofList a, String.ofList b)
+
+def splitN {α : Type} : Nat → List α → List (List (List α))
+  | 0, [] => [[]]
+  | 0, _ :: _ => []
+  | 1, xs => [[xs]]
+  | n + 2, xs =>
+    (split2 xs).flatMap fun (ys, zs) =>
+      (splitN (n + 1) zs).map fun rs => ys :: rs
+
+#eval splitN 3 "Jan".toList |>.map
+   (·.map String.ofList)
+```
+
+:::terse
+- O reconhecedor segue a gramática: uma linha por regra. Para A → aAa,
+  ele procura uma divisão em três pedaços `[a]`, `ys`, `[a]` e reconhece
+  `ys`.
+- A função `recognize` chama a si mesma em `ys`. Lean exige que toda função
+  termine, e sozinho ele não vê que `ys` é menor do que `xs`: o padrão
+  `[['a'], ys, ['a']]` não diz de onde a lista veio.
+- A função `attach` junta a cada divisão a prova de que ela está em
+  `splitN 3 xs`. A cláusula `termination_by xs.length` diz o que
+  diminui, e `decreasing_by` prova que diminui, com o lema do bloco
+  acima: os pedaços juntos dão `xs`, então `ys` tem dois elementos a
+  menos.
+- Uma regra recursiva à esquerda, V → V T, também não seria problema,
+  porque V recebe um pedaço menor da entrada, desde que o pedaço de T
+  não seja vazio.
+- Se o pedaço de T puder ser vazio, V recebe a entrada inteira e chama
+  a si mesma sem fim. As divisões com pedaço vazio têm de ser
+  descartadas antes da chamada; sem isso, `decreasing_by` não prova
+  nada e o Lean recusa a definição.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.2, from "Now the function for recognizing…" to
+"…for splitting the input into n substrings."
+:::
+::::
+
+:::details "As divisões juntam-se de volta na entrada"
+```lean
+theorem append_of_mem_split2 {α : Type} :
+    ∀ {xs : List α} {p : List α × List α},
+      p ∈ split2 xs → p.1 ++ p.2 = xs
+  | [], p, h => by
+    simp [split2] at h
+    simp [h]
+  | x :: xs, p, h => by
+    simp only [split2, List.mem_cons, List.mem_map] at h
+    rcases h with rfl | ⟨⟨ys, zs⟩, h, rfl⟩
+    · rfl
+    · simp [← append_of_mem_split2 h]
+
+theorem flatten_of_mem_splitN {α : Type} :
+    ∀ {n : Nat} {xs : List α} {l : List (List α)},
+      l ∈ splitN n xs → l.flatten = xs
+  | 0, [], l, h | 1, _, l, h => by
+    simp [splitN] at h
+    simp [h]
+  | 0, _ :: _, _, h => by simp [splitN] at h
+  | n + 2, xs, l, h => by
+    simp only [splitN, List.mem_flatMap, List.mem_map] at h
+    obtain ⟨⟨ys, zs⟩, h1, rs, h2, rfl⟩ := h
+    simp [flatten_of_mem_splitN h2, append_of_mem_split2 h1]
+```
+:::
+
+```lean
+def recognize (xs : List Char) : Bool :=
+  xs == [] || xs == ['a'] || xs == ['b'] || xs == ['c'] ||
+  (splitN 3 xs).attach.any fun
+    | ⟨[['a'], ys, ['a']], h⟩ => recognize ys
+    | ⟨[['b'], ys, ['b']], h⟩ => recognize ys
+    | ⟨[['c'], ys, ['c']], h⟩ => recognize ys
+    | _ => false
+termination_by xs.length
+decreasing_by
+  all_goals
+    have := congrArg List.length (flatten_of_mem_splitN h)
+    simp at this
+    omega
+
+#eval recognize "aabcbbcbaa".toList
+#eval recognize "aabcbbcba".toList
+```
+
+:::terse
+- A função `gener n` dá as palavras de comprimento `n`; `generUpTo n`,
+  as de comprimento até `n`. As palavras são infinitas, mas uma lista
+  em Lean é finita, por isso a geração para num comprimento dado.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.2, from "From recognition to generation…" to the
+first fifteen palindromes.
+:::
+::::
+
+```lean
+def gener {α : Type} : Nat → List α → List (List α)
+  | 0, _ => [[]]
+  | n + 1, alphabet =>
+    alphabet.flatMap fun x =>
+      (gener n alphabet).map (x :: ·)
+
+def generUpTo {α : Type} (n : Nat) (alphabet : List α) :
+    List (List α) :=
+  (List.range (n + 1)).flatMap fun k => gener k alphabet
+
+#eval ((generUpTo 3 "abc".toList).filter recognize).map
+  String.ofList
+```
+
+:::terse
+- O Mathlib define palíndromo como um predicado indutivo,
+  `List.Palindrome`. Os seus três construtores são as regras da
+  gramática: a lista vazia, uma lista de um elemento, e `x :: (l ++ [x])`
+  para `l` palíndromo.
+- O teorema `recognize_iff_palindrome` diz que `recognize` concorda
+  com essa definição em toda palavra sobre `{a, b, c}`, de qualquer
+  comprimento.
+- A prova é por indução no comprimento da palavra, uma direção de cada
+  vez. Ela só é possível porque `recognize` não é `partial`: o Lean
+  conhece a equação que a define.
+- O teorema `recognize_generUpTo` é o caso das palavras geradas por
+  `generUpTo n`, para todo `n`.
+:::
+
+:::details "O reconhecedor e a definição de palíndromo"
+```lean
+theorem mem_split2_append {α : Type} :
+    ∀ ys zs : List α, (ys, zs) ∈ split2 (ys ++ zs)
+  | [], [] => by simp [split2]
+  | [], z :: zs => by simp [split2]
+  | y :: ys, zs => by
+    simp only [List.cons_append, split2, List.mem_cons,
+      List.mem_map]
+    exact Or.inr ⟨(ys, zs), mem_split2_append ys zs, rfl⟩
+
+theorem mem_splitN_flatten {α : Type} :
+    ∀ l : List (List α), l ∈ splitN l.length l.flatten
+  | [] => by simp [splitN]
+  | [ys] => by simp [splitN]
+  | ys :: zs :: rs => by
+    simp only [List.length_cons, List.flatten_cons]
+    simp only [splitN, List.mem_flatMap, List.mem_map]
+    refine ⟨(ys, (zs :: rs).flatten),
+      by simpa using mem_split2_append ys _,
+      zs :: rs, ?_, rfl⟩
+    simpa using mem_splitN_flatten (zs :: rs)
+
+theorem recognize_sound (n : Nat) :
+    ∀ w : List Char, w.length ≤ n →
+      recognize w → w.Palindrome := by
+  induction n with
+  | zero =>
+    intro w hw hr
+    simp at hw
+    rw [hw]
+    exact .nil
+  | succ n ih =>
+    intro w hw h
+    rw [recognize] at h
+    simp only [Bool.or_eq_true, beq_iff_eq,
+      List.any_eq_true] at h
+    rcases h with (((rfl | rfl) | rfl) | rfl)
+      | ⟨⟨l, hl⟩, _, hm⟩
+    · exact .nil
+    · exact .singleton _
+    · exact .singleton _
+    · exact .singleton _
+    · split at hm <;> (try contradiction) <;>
+      · rename_i ys hys _
+        have he := flatten_of_mem_splitN hys
+        simp at he
+        subst he
+        apply List.Palindrome.cons_concat
+        exact ih ys (by simp at hw; omega) hm
+
+theorem recognize_complete (n : Nat) :
+    ∀ w : List Char, w.length ≤ n → w ⊆ "abc".toList →
+      w.Palindrome → recognize w = true := by
+  induction n with
+  | zero =>
+    intro w hw _ _
+    simp at hw
+    subst hw
+    rw [recognize]
+    simp
+  | succ n ih =>
+    intro w hw ha hp
+    cases hp with
+    | nil =>
+      rw [recognize]
+      simp
+    | singleton x =>
+      have hx : x ∈ "abc".toList := ha (by simp)
+      simp at hx
+      rcases hx with rfl | rfl | rfl <;>
+        (rw [recognize]; simp)
+    | cons_concat x hl =>
+      rename_i l
+      have hx : x ∈ "abc".toList := ha (by simp)
+      have hl' : l ⊆ "abc".toList :=
+        fun c hc => ha (by simp [hc])
+      have ih' := ih l (by simp at hw; omega) hl' hl
+      rw [recognize]
+      simp only [Bool.or_eq_true, beq_iff_eq,
+        List.any_eq_true]
+      right
+      have hmem :
+          [[x], l, [x]] ∈ splitN 3 (x :: (l ++ [x])) := by
+        simpa using mem_splitN_flatten [[x], l, [x]]
+      refine ⟨⟨_, hmem⟩, List.mem_attach _ _, ?_⟩
+      simp at hx
+      rcases hx with rfl | rfl | rfl <;> simpa using ih'
+
+theorem recognize_iff_palindrome (w : List Char)
+    (hw : w ⊆ "abc".toList) :
+    recognize w ↔ w.Palindrome :=
+  ⟨recognize_sound _ w (Nat.le_refl _),
+   recognize_complete _ w (Nat.le_refl _) hw⟩
+
+theorem subset_of_mem_gener {α : Type} (alphabet : List α) :
+    ∀ n w, w ∈ gener n alphabet → w ⊆ alphabet
+  | 0, w, h => by
+    simp [gener] at h
+    simp [h]
+  | n + 1, w, h => by
+    simp only [gener, List.mem_flatMap, List.mem_map] at h
+    obtain ⟨x, hx, v, hv, rfl⟩ := h
+    intro c hc
+    simp at hc
+    rcases hc with rfl | hc
+    · exact hx
+    · exact subset_of_mem_gener alphabet n v hv hc
+
+theorem recognize_generUpTo (n : Nat) :
+    ∀ w ∈ generUpTo n "abc".toList,
+      recognize w = true ↔ w.Palindrome := by
+  intro w hw
+  simp only [generUpTo, List.mem_flatMap] at hw
+  obtain ⟨k, _, hk⟩ := hw
+  exact recognize_iff_palindrome w
+    (subset_of_mem_gener _ k w hk)
+```
+:::
+
+:::terse
+- Analisar é construir as árvores. A entrada é uma `List Char`, e as
+  árvores são do tipo `ParseTree Char Char`: caracteres nas folhas e o
+  rótulo `A` nos nós.
+- Mesma receita do reconhecedor, uma linha por regra; agora cada linha
+  devolve a lista das suas árvores, vazia quando a regra não se aplica.
+- As regras de uma gramática podem valer ao mesmo tempo, por isso as
+  listas de todas as linhas são concatenadas com `++`. Numa gramática
+  ambígua, uma palavra recebe assim mais de uma árvore.
+- A palavra vazia vira a árvore vazia `ep`.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate CSwFP/9.2, from "Parsing with a context-free grammar…"
+to the end of the section.
+:::
+::::
+
+```lean
+def parse (xs : List Char) : List (ParseTree Char Char) :=
+  (if xs == [] then [.ep] else []) ++
+  (if xs == ['a'] then [.leaf 'a'] else []) ++
+  (if xs == ['b'] then [.leaf 'b'] else []) ++
+  (if xs == ['c'] then [.leaf 'c'] else []) ++
+  (splitN 3 xs).attach.flatMap fun
+    | ⟨[['a'], ys, ['a']], _h⟩ =>
+      (parse ys).map fun t =>
+        .branch 'A' [.leaf 'a', t, .leaf 'a']
+    | ⟨[['b'], ys, ['b']], _h⟩ =>
+      (parse ys).map fun t =>
+        .branch 'A' [.leaf 'b', t, .leaf 'b']
+    | ⟨[['c'], ys, ['c']], _h⟩ =>
+      (parse ys).map fun t =>
+        .branch 'A' [.leaf 'c', t, .leaf 'c']
+    | _ => []
+termination_by xs.length
+decreasing_by
+  all_goals
+    have := congrArg List.length (flatten_of_mem_splitN _h)
+    simp at this
+    omega
+
+#eval IO.println (parse "aabaa".toList)
+#eval IO.println (parse "aabbaa".toList)
+#eval IO.println (parse "aabcbbcba".toList)
+```
+
+::::exercise (rating := 2) (name := "split-nonempty")
+Numa gramática sem regras ε, nenhum pedaço da divisão pode ser vazio.
+Defina `split2'` e `splitN'`, que dão só as divisões sem pedaços vazios.
+Confira o resultado em `"Jan"`.
+
+```lean
+def split2' {α : Type} : List α → List (List α × List α)
+  | [] | [_] => []
+  | x :: y :: ys =>
+    solution!(
+      ([x], y :: ys) ::
+        (split2' (y :: ys)).map fun (us, vs) =>
+          (x :: us, vs))
+
+def splitN' {α : Type} : Nat → List α → List (List (List α))
+  | 0, [] => [[]]
+  | 0, _ :: _ => []
+  | 1, [] => []
+  | 1, xs => [[xs]]
+  | n + 2, xs =>
+    solution!(
+      (split2' xs).flatMap fun (ys, zs) =>
+        (splitN' (n + 1) zs).map fun rs => ys :: rs)
+
+theorem split2'_jan :
+    split2' "Jan".toList =
+      [(['J'], ['a', 'n']), (['J', 'a'], ['n'])] := by
+  solution!
+   decide
+
+theorem splitN'_jan :
+    splitN' 3 "Jan".toList = [[['J'], ['a'], ['n']]] := by
+  solution!
+   decide
+```
+::::
+
+```lean
+end Parsing
+```
diff --git a/DEVIATIONS.md b/DEVIATIONS.md
index 5863599..fe587c9 100644
--- a/DEVIATIONS.md
+++ b/DEVIATIONS.md
@@ -212,6 +212,67 @@ syntax and model, so it comes after `ModelChecking`. Being written.
 - 7.2 calls the second argument of a determiner its *body*, where CSwFP/6
   called it its *scope*. Both translate as "escopo".
 
-## Beyond CSwFP/7
+### `Parsing`
 
-Not planned yet.
+CSwFP/8 is skipped for now, and the chapter follows `Composition`.
+
+- 9.1: the tree relations are lists of pairs, as in CSwFP, because the
+  section shows them with `#eval`; Mathlib's `Rel` of `Sets` is a `Prop`
+  and cannot be printed. Dominance uses Lean's `<+:` (`List.IsPrefix`) in
+  place of a helper `prefix`. `pos` is written with a local helper
+  `posFrom` (`let rec`), so that Lean sees the recursion over the list
+  of subtrees as structural. `subtree` returns `ep` at a position the
+  tree does not have, where CSwFP's is undefined. `toText` separates the
+  daughters of a node by spaces, as in the bracket notation of LaTeX's
+  `qtree` (`[.NP Snow White]`); CSwFP's `show` prints them as a list,
+  with a further pair of brackets and commas. Nothing reads the text
+  back: later chapters walk the trees, not their text.
+- Exercise 9.2 becomes two theorems about positions, parts (1) and (2):
+  the relation of c-command is a sister followed by dominance, and neither
+  part depends on the tree. Part (3), on the lowest branching position, is
+  not ported. Exercises 9.1, 9.3, 9.4 and 9.5 ask for a definition checked
+  on the example tree; 9.6 asks for the splitting functions without empty
+  parts.
+- 9.2: `splitN` is defined for every number of pieces, where CSwFP's
+  stops with an error below two: one piece is the input itself, and the
+  empty input has the split into zero pieces. This makes `splitN` serve
+  unary rules too, and lets `mem_splitN_flatten`, the converse of
+  `flatten_of_mem_splitN`, hold for every list of pieces. `splitN'` in
+  exercise 9.6 follows suit.
+- 9.2: `recognize` and `parse` are total. They recurse over
+  `(splitN 3 xs).attach`, which pairs each split with a proof of
+  membership, and `decreasing_by` uses the lemma `flatten_of_mem_splitN`
+  (the pieces of a split concatenate to the input) to show that the
+  middle piece is shorter. The cue on termination says why left
+  recursion is no trouble here, which is exercise 9.7. Generation stops
+  at a given length, since Lean lists are finite. A theorem, in a
+  `:::details` block, proves that `recognize` agrees with Mathlib's
+  `List.Palindrome` on every word over `{a, b, c}`. `parse` gives the
+  empty word the empty tree `ep`, where CSwFP uses a leaf `"[]"`.
+- 9.3: `Parser α β` is `StateT (List α) List β`, which unfolds by
+  definition to CSwFP's `[a] -> [(b,[a])]` (an `example … := rfl` says
+  so). Mathlib's `Monad` and `Alternative` instances for `List` then give
+  `pure`, `failure`, `<|>` and `<$>` with CSwFP's meaning, so `succeed`
+  and `failp` are not defined: they are `pure` and `failure`. CSwFP's
+  sequencing `<*>` and `<:>` become `do` blocks (Lean's `<*>` is the
+  applicative one, with another type), and `collect` is written with
+  `do`. The synonym `PARSER a b` is not ported: as an `abbrev` over
+  `Parser α (ParseTree α β)` it hides the type constructor that `<$>`
+  and `<|>` need to find their instances. Lean's `Std.Internal.Parsec`
+  was considered and rejected: it returns one result, and its `<|>`
+  commits to the first alternative that succeeds.
+- 9.3: `palindrome`, `many` and the left-recursive example are
+  `partial def`. The input they recurse on is the remainder left inside
+  the `StateT`, and proving it shorter would need parsers that carry a
+  proof that their remainder is a suffix of the input. Later sections
+  only run parsers. A cue cites Danielsson's total parser combinators.
+  The left-recursive example is defined but never run: it overflows the
+  stack.
+- 9.3: the Mastermind parser is dropped with Mastermind (see 5.4).
+  `many` stays: 9.6 uses it. `parseManyAs`, which only the Mastermind
+  parser used, becomes the new exercise `parse-many-as`, checked on a
+  sequence of adjectives.
+
+## Beyond CSwFP/9
+
+Not planned yet. CSwFP/8 is skipped for now.
diff --git a/README.md b/README.md
index 7084e83..6e76242 100644
--- a/README.md
+++ b/README.md
@@ -50,7 +50,8 @@ adapts — see [DEVIATIONS.md](DEVIATIONS.md) for why.
 - [~] The composition of meaning — [source](CSwL/Composition.lean)
   (sections in [`CSwL/Composition/`](CSwL/Composition))
 - [ ] Extension and intension
-- [ ] Parsing
+- [~] Parsing — [source](CSwL/Parsing.lean) (sections in
+  [`CSwL/Parsing/`](CSwL/Parsing))
 - [ ] Relations and scope
 - [ ] Semantics in continuation passing style
 - [ ] Discourse representation and context
diff --git a/STYLE-CODE.md b/STYLE-CODE.md
index bc2fd20..5d327f6 100644
--- a/STYLE-CODE.md
+++ b/STYLE-CODE.md
@@ -84,6 +84,7 @@ this way is usually a mistake; see "Known gaps."
 | `InfEngine` | `let rec` | `do`-notation | — |
 | `ModelChecking` | `mutual` over `inductive` types (`Logic/FOL` only uses it over `def`) | guillemet identifiers (`«with»`), pattern-matching `fun \| … => …` (first use outside a solution) | *(none new)* |
 | `Composition` | — | image `f '' A`, `Set.BijOn`, `Set.ncard`, `List.count`, `List.Perm`, Mathlib's `Language` with `ᶜ`, `⊓`, `+` and `∗` | *(none new)* |
+| `Parsing` | `termination_by`, `decreasing_by`, `partial def` | `<+:` (`List.IsPrefix`), Mathlib's `List.Palindrome`, `List.attach` and subtype patterns (`\| ⟨l, h⟩`), `congrArg`, `StateT` with Mathlib's `Monad`/`Alternative List`, `pure`, `failure`, `<\|>`, `<$>`, `>>=`, `.run` | `subst`, `split at`, `try`, `rename_i`, `contradiction`; `rcases` and `Or.inr` (first use outside a solution) |
 
 `ModelChecking` is where `abbrev` and `ToString` instances become the
 dominant idiom, but both arrive earlier; what is genuinely new there is the mutually
@@ -147,7 +148,9 @@ author decision, not a mechanical fix.
   a solution (`Phonemes.lean:309`) and visible only much later, at
   `InfEngine.lean:439`. The pattern-matching `fun` is the same shape again —
   `IntroL.lean:364` and `PL.lean:245`, both in solutions, then ordinary code
-  throughout `ModelChecking`. The rest never surface at all.
+  throughout `ModelChecking`. `rcases` and `Or.inr` surface in the
+  `:::details` proofs of `Parsing/Recognition.lean` (lines 100 and 189).
+  The rest never surface at all.
 
 `IntroCS` is the constraint's one accepted exception: it uses Lean that
 `IntroL` only presents later, deliberately, and the chapter says so where its
diff --git a/scripts/check-cswfp.py b/scripts/check-cswfp.py
index 61352ba..66c9027 100755
--- a/scripts/check-cswfp.py
+++ b/scripts/check-cswfp.py
@@ -31,7 +31,7 @@
 # How many exercises each CSwFP chapter has.
 COUNTS = {"CSwFP/1": 3, "CSwFP/2": 17, "CSwFP/3": 19,
           "CSwFP/4": 24, "CSwFP/5": 32, "CSwFP/6": 7,
-          "CSwFP/7": 28}
+          "CSwFP/7": 28, "CSwFP/9": 16}
 
 EXERCISE = re.compile(r'^:+exercise\b.*\(name := "([^"]+)"\)')
 CITATION = re.compile(r"CSwFP|página \d+|\(p\. \d+|§\s*\d|exemplo \(\d+\.\d+\)"