theorem NLSubsetP.nspace_log_config_graph_poly_time_decidable {Γ : Type} (A : Set (List Γ)) (Q : Type) [DecidableEq Q] (M : SpaceComplexity.NTM Q Γ) (hLang : M.language = A) (g : ℕ → ℕ) (hgBound : SpaceComplexity.IsAsympBoundedBy g LogSpace.log) (hSpace : M.RunsInSpace g) : TuringMachine.InP A

If an NTM M recognizing A runs in O(log n) space (with bound g), then A ∈ P. The proof uses the configuration-graph reachability simulation: since the NTM uses log space, it has polynomially many configurations, so a polynomial-time deterministic decider can search the configuration graph.

theorem NLSubsetP.nl_subset_p {Γ : Type} (A : Set (List Γ)) (hA : LogSpace.InNL A) : TuringMachine.InP A

Sipser, Lecture 20. NL ⊆ P. Every language decided by a nondeterministic log-space TM is also decided by a deterministic polynomial-time TM.