structure ConfigReachability.ConfigGraph (Q Γ : Type) : Type 1

An abstract directed graph whose vertices are configurations: a Vertex type with an adjacency relation Adj. The configuration graph G_{M,w} of an NTM M on input w is the instance with Vertex = Config Q Γ and Adj = M.step.

• Vertex : Type
• Adj : self.Vertex → self.Vertex → Prop

def ConfigReachability.mkConfigGraph {Q Γ : Type} (M : SpaceComplexity.NTM Q Γ) (_w : List Γ) : ConfigGraph Q Γ

The configuration graph G_{M,w} of NTM M on input w: vertices are TM configurations and edges are single steps M.step.

def ConfigReachability.ConfigGraph.Reachable {Q Γ : Type} (G : ConfigGraph Q Γ) (c₁ c₂ : G.Vertex) : Prop

Reachability in a configuration graph: Reachable c₁ c₂ is the reflexive–transitive closure of the adjacency relation.

theorem ConfigReachability.branch_reachable_of_valid {Q Γ : Type} (M : SpaceComplexity.NTM Q Γ) (w : List Γ) (branch : ℕ → TuringMachine.Config Q Γ) (hvalid : M.IsValidBranch w branch) (k : ℕ) : Relation.ReflTransGen M.step (M.initConfig w) (branch k)

If branch is a valid (nondeterministic) computation branch of M on input w, then for every step index k the configuration branch k is reachable from the initial configuration M.initConfig w via M.step.

theorem ConfigReachability.exists_branch_of_reflTransGen {Q Γ : Type} (M : SpaceComplexity.NTM Q Γ) {a b : TuringMachine.Config Q Γ} (hreach : Relation.ReflTransGen M.step a b) (hhalt_b : M.isHaltConfig b) : ∃ (branch : ℕ → TuringMachine.Config Q Γ) (k : ℕ), branch 0 = a ∧ (∀ (n : ℕ), (¬M.isHaltConfig (branch n) → M.step (branch n) (branch (n + 1))) ∧ (M.isHaltConfig (branch n) → branch (n + 1) = branch n)) ∧ branch k = b

Converse direction: given a reachability path a ⟶* b under M.step and the fact that b is a halting configuration, one can extract an actual computation branch branch : ℕ → Config with branch 0 = a, branch k = b, and the usual NTM branch transition law (steps before halting, stuttering after halting).

theorem ConfigReachability.accepts_of_reflTransGen_accept {Q Γ : Type} (M : SpaceComplexity.NTM Q Γ) (w : List Γ) {c : TuringMachine.Config Q Γ} (hreach : Relation.ReflTransGen M.step (M.initConfig w) c) (haccept : M.isAcceptConfig c) : M.accepts w

If an accept configuration c is reachable from the initial configuration of M on w under M.step, then M accepts w.

theorem ConfigReachability.accepts_iff_configGraph_reachable {Q Γ : Type} (M : SpaceComplexity.NTM Q Γ) (w : List Γ) : M.accepts w ↔ ∃ (c : TuringMachine.Config Q Γ), M.isAcceptConfig c ∧ (mkConfigGraph M w).Reachable (M.initConfig w) c

Claim (Sipser, Lectures 19/20). An NTM M accepts input w if and only if some accept configuration is reachable from the start configuration c_start in the configuration graph G_{M,w}. This is the key bridge between TM acceptance and graph reachability used in the proofs of NL ⊆ P and Savitch's Theorem.