PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-30

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The published prefix automata extend canonically to DFAs for factor-avoidance languages

Statement

Let $Σ$ be a finite alphabet and let $B$ be a finite nonempty set of nonempty words over $Σ$ . Starting from the published prefix automaton on $S_{B}$ , adjoin a new sink state $⊥$ , send every previously rejected letter to $⊥$ , let $⊥$ loop on every letter, and declare every state in $S_{B}$ accepting while $⊥$ is rejecting.

The resulting machine is a DFA over $Σ$ , and it recognizes exactly the language of words over $Σ$ that avoid every factor in $B$ .

Facts & Assumptions

Given: A finite alphabet $Σ$ and a finite nonempty set $B$ of nonempty words over $Σ$ .

[L1]

The set $S_{B}$ consists of the words that avoid $B$ and are proper prefixes of words in $B$ ; it is finite, and $ε \in S_{B}$ , by Finite words, contiguous factors, avoidance and proper-prefix states.

[L2]

In the published prefix automaton, if $s a$ still avoids $B$ then the edge labelled $a$ from $s$ goes to the longest suffix of $s a$ that lies in $S_{B}$ ; if $s a$ contains a forbidden factor, the letter $a$ is rejected, by The longest-suffix prefix automaton for a finite set of forbidden factors.

[L3]

A word is accepted by a DFA exactly when the final state lies in the accepting set, by Acceptance of a word by a DFA and the recognized language.

Proof

technique · direct

1.1

Define $D_{B}$ to have state set $S_{B} \cup {⊥}$ , start state $ε$ , accepting set $S_{B}$ , and transition rule $δ (s, a) = {\begin{cases} the published longest-suffix state for s a, & if s a avoids B, \\ ⊥, & if s a contains a factor in B, \end{cases} δ (⊥, a) = ⊥ .$ By [L1] and [L2], this is a total transition function on a finite state set, so $D_{B}$ is a DFA.

L1L2construct

2.1

We prove by induction on the length of a word $w$ that the run of $D_{B}$ from $ε$ behaves as follows: if $w$ avoids $B$ , the final state is the longest suffix of $w$ belonging to $S_{B}$ ; if $w$ contains a forbidden factor, the final state is $⊥$ . The induction step is exactly the two cases built into the definition of $δ$ in step 1.1.

step 1.1induction

3.1

If $w$ avoids $B$ , then step 2.1 places the run in a state of $S_{B}$ , hence [L3] says that $D_{B}$ accepts $w$ . If $w$ contains a factor in $B$ , then step 2.1 places the run in $⊥$ , so [L3] says that $D_{B}$ rejects $w$ .

L3step 2.1

4.1

Therefore $L (D_{B})$ is exactly the language of words over $Σ$ that avoid every forbidden factor in $B$ .

step 3.1∎

Depends on

Used by

Adding a sink turns the published prefix automaton for avoiding `11` into a DFA Example

Dependency tree · two levels

12 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

R. P. Stanley, Enumerative Combinatorics, vol. 1, 2nd ed., Example 4.7.7 and Proposition 4.7.8 (standard reference, not scraped)