LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-09-12

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.

Acceptance is reachability of an accepting configuration

Statement

Let $N$ be either a deterministic one-tape Turing machine or a nondeterministic one-tape Turing machine, and fix an input word $w$ . Then $N$ accepts $w$ if and only if, in the configuration graph $G_{N} (w)$ , some accepting configuration is reachable from the initial configuration.

Facts & Assumptions

Given: A machine $N$ of one of the two stated kinds, an input word $w$ , and its configuration graph $G_{N} (w)$ .

[L1]

In the deterministic case, an accepting computation history on $w$ is a finite list of configurations beginning at the initial configuration, ending at an accepting configuration, and following the one-step relation at each stage, by Finite computation histories, halting computations, and divergence.

[L2]

In the nondeterministic case, an accepting computation on $w$ is likewise a finite list of configurations beginning at the initial configuration, ending at an accepting configuration, and following the nondeterministic one-step relation at each stage, by Accepting computations of a nondeterministic machine.

[L3]

The configuration graph has exactly those legal one-step moves as its arcs, by The configuration graph of a machine on an input.

Proof

technique · direct

1.1

Suppose first that $N$ accepts $w$ . By [L1] in the deterministic case and by [L2] in the nondeterministic case, there is a finite accepting computation $C_{0}, \dots, C_{n}$ from the initial configuration to an accepting configuration. By [L3], each consecutive pair is an arc of $G_{N} (w)$ , so this finite vertex list witnesses that an accepting configuration is reachable from the initial configuration.

L1L2L3given

1.2

Conversely, suppose there is a finite vertex list $C_{0}, \dots, C_{n}$ in $G_{N} (w)$ whose first term is the initial configuration, whose last term is accepting, and whose consecutive pairs are arcs. By [L3], each consecutive pair satisfies the legal one-step relation. Therefore [L1] or [L2], according to the kind of machine $N$ , makes $C_{0}, \dots, C_{n}$ an accepting computation of $N$ on $w$ .

L1L2L3given

2.1

Steps 1.1 and 1.2 prove that $N$ accepts $w$ if and only if some accepting configuration is reachable from the initial configuration in $G_{N} (w)$ .

step 1.1step 1.2∎

Depends on

Used by

A branching configuration graph with one accepting path and one looping path Example

Dependency tree · two levels

10 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

John E. Savage, Models of Computation: Exploring the Power of Computing, Chapter 5 (standard reference, not scraped)
Michael Sipser, MIT 18.404J Theory of Computation, Lecture 10: The Computation History Method (standard reference, not scraped)