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.

✓ 3 results · all verified · 1 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Turing Machines, Configurations, and Computation: Examples and Counterexamples

1 · Prerequisites

2 · Summary

These examples make the page's machine semantics concrete: one explicit accepting history check, one configuration-graph witness for existential nondeterministic acceptance, and one immediate-rejection counterexample to the claim that rejection means divergence.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-12Open item page →

Checking a short accepting history for a unary increment machine

Example

Consider the deterministic machine with states $q_{0}, q_{a c c}, q_{r e j}$ , input alphabet ${I}$ , tape alphabet ${I, ⊔}$ , and transition rules $δ (q_{0}, I) = (q_{0}, I, R), δ (q_{0}, ⊔) = (q_{a c c}, I, R) .$ On input $I I I$ it scans right across the unary block, writes one extra I in the first blank cell, and halts.

Using the configuration-word convention with B for the blank symbol, a candidate accepting history is $q_{0} I I I, I q_{0} I I, I I q_{0} I, I I I q_{0} B, I I I I q_{a c c} B .$

Facts & Assumptions

Given: The machine and input above, together with the displayed candidate history.

[L1]

For a fixed machine and input, encoded accepting computation histories form a decidable language by local checks on the start configuration, successive one-step moves, and the final accepting state, by For a fixed machine and input, valid accepting computation histories form a decidable language.

[L2]

A halting computation history is a finite list beginning at the initial configuration and following the one-step relation at each stage, by Finite computation histories, halting computations, and divergence.

Verification

technique · direct

1.1given

The first configuration word $q_{0} I I I$ is the canonical initial configuration on input $I I I$ : the head is at the leftmost I, the state is $q_{0}$ , and the last displayed cell is the last nonblank input cell.

1.2given

Each of the first three transitions just moves the head one cell to the right while leaving the scanned I unchanged, so $q_{0} I I I \to I q_{0} I I \to I I q_{0} I \to I I I q_{0} B$ is legal. The last transition uses $δ (q_{0}, ⊔) = (q_{a c c}, I, R)$ , so the machine writes I in the scanned blank cell and then moves right onto the next blank cell. Therefore $I I I q_{0} B \to I I I I q_{a c c} B$ is legal as well.

2.1L1L2step 1.1step 1.2∎

The final configuration word has state $q_{a c c}$ , so it is accepting. Therefore the displayed list is an accepting computation history in the sense of [L2], exactly the sort of object whose validity [L1] decides.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-12Open item page →

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

Example

Use the nondeterministic machine from FALSE: nondeterministic acceptance requires every branch to halt on input $w = 1$ . Its initial configuration $C_{0}$ has two outgoing arcs:

one to the accepting configuration $C_{a c c}$ reached by the move $(q_{a c c}, 1, R)$ ,
one to the looping configuration $C_{L}$ reached by the move $(q_{L}, 1, L)$ .

From $C_{L}$ there is an arc back to $C_{L}$ again, because the machine stays in state $q_{L}$ , rewrites 1 by 1, and the left-boundary rule keeps the head at cell $0$ .

Facts & Assumptions

Given: The machine and input just described, with vertices $C_{0}, C_{a c c}, C_{L}$ in its configuration graph.

[L1]

A machine accepts an input if and only if some accepting configuration is reachable from the initial configuration in its configuration graph, by Acceptance is reachability of an accepting configuration.

Verification

technique · direct

1.1given

The arc $C_{0} \to C_{a c c}$ is a directed path of length $1$ from the initial configuration to an accepting configuration.

1.2given

The arc $C_{0} \to C_{L}$ followed by the loop $C_{L} \to C_{L}$ shows that the graph also contains a nonhalting branch.

2.1L1step 1.1step 1.2∎

By [L1] and step 1.1, the existence of the length- $1$ path already proves acceptance of the input, regardless of the looping branch from step 1.2.

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-12Open item page →

Immediate rejection is a halting computation, not a divergence

Statement refuted

The statement "rejection is divergence" is false.

Facts & Assumptions

Given: The machine and input from FALSE: rejection is divergence: states $q_{0}, q_{a c c}, q_{r e j}$ , tape rule $δ (q_{0}, 1) = (q_{r e j}, 1, R),$ and input word $w = 1$ .

[A1]

The statement refuted is: rejecting an input means diverging on that input.

[L1]

A configuration is rejecting exactly when its state is $q_{r e j}$ , by Initial, accepting, and rejecting configurations.

Counterexample

technique · direct

1.1given

Starting from the initial configuration on input $1$ , one legal step sends the machine to a configuration with state $q_{r e j}$ .

2.1L1step 1.1

By [L1], that next configuration is rejecting, so the computation halts after one step. Hence the input is rejected and does not diverge.

3.1A1step 2.1∎

Therefore this machine on input $1$ is a counterexample to [A1].

Turing Machines, Configurations, and Computation: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

Checking a short accepting history for a unary increment machine

Example

Facts & Assumptions

Verification

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

Example

Facts & Assumptions

Verification

Immediate rejection is a halting computation, not a divergence

Statement refuted

Facts & Assumptions

Counterexample

Sources