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.
Accepting computations of a nondeterministic machine
Definition
Fix a nondeterministic one-tape Turing machine and an input word .
A configuration of is a triple with , head position , and finite-support tape content , just as in Configurations of a deterministic one-tape Turing machine. It is accepting when and rejecting when , as in Initial, accepting, and rejecting configurations.
For configurations and of , write when and there exists an allowed instruction such that is obtained from by the same local rewrite and head-move recipe used in The one-step configuration relation, with .
An accepting computation of on input is a finite list of configurations such that , where is the input tape defined in the same way as for deterministic machines, each for , and is accepting.
We say that accepts if such an accepting computation exists.
Remarks
-
Nondeterministic acceptance is existential: one accepting branch is enough.
-
Other branches may reject, may halt differently, or may continue forever; no global halting requirement is part of acceptance itself.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
13 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)