def TuringMachine.NTM.step {Q Γ : Type} [DecidableEq Q] (M : NTM Q Γ) (c₁ c₂ : Config Q Γ) : Prop

A single nondeterministic step of M: c₂ is a possible successor of c₁, selected from the set of transitions δ c₁.state (read symbol). Halting configurations are fixed points.

def TuringMachine.NTM.accepts {Q Γ : Type} [DecidableEq Q] (M : NTM Q Γ) (w : List Γ) : Prop

NTM acceptance: M accepts w iff there is some finite computation branch of length n + 1 starting from M.initConfig w, with each step a valid nondeterministic transition, ending in an accepting configuration.

def TuringMachine.NTM.language {Q Γ : Type} [DecidableEq Q] (M : NTM Q Γ) : Set (List Γ)

The language recognized by NTM M: the set of strings it accepts.

def TuringMachine.NTM.isDecider {Q Γ : Type} [DecidableEq Q] (M : NTM Q Γ) : Prop

An NTM is a decider if every computation branch on every input halts in finitely many steps.

def TuringMachine.NTM.decides {Q Γ : Type} [DecidableEq Q] (M : NTM Q Γ) (A : Set (List Γ)) : Prop

M decides A iff it is a decider and its language equals A.

def TuringMachine.TM.runsInTime {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (t : ℕ → ℕ) : Prop

A deterministic TM runs in time t if it halts on every input w within t (|w|) steps.

def TuringMachine.NTM.runsInTime {Q Γ : Type} [DecidableEq Q] (M : NTM Q Γ) (t : ℕ → ℕ) : Prop

An NTM runs in time t if every branch of length at most t (|w|) reaches a halting configuration on input w.

def TuringMachine.IsBigO (f g : ℕ → ℕ) : Prop

f = O(g): there exist constants c > 0 and n₀ such that f n ≤ c · g n for all n ≥ n₀.

def TuringMachine.InTIME (t : ℕ → ℕ) {Γ : Type} (A : Set (List Γ)) : Prop

A ∈ TIME(t): some deterministic TM decides A in time O(t).

def TuringMachine.InNTIME (t : ℕ → ℕ) {Γ : Type} (A : Set (List Γ)) : Prop

A ∈ NTIME(t): some nondeterministic TM decides A in time O(t).

def TuringMachine.InP {Γ : Type} (A : Set (List Γ)) : Prop

The complexity class P: A ∈ P iff A ∈ TIME(n^k) for some k.

def TuringMachine.InNP {Γ : Type} (A : Set (List Γ)) : Prop

The complexity class NP: A ∈ NP iff A ∈ NTIME(n^k) for some k.

def TuringMachine.InEXPTIME {Γ : Type} (A : Set (List Γ)) : Prop

The complexity class EXPTIME: deciders running in time 2^{n^k} for some k.

def TuringMachine.IsPolyTimeComputableFunction {Γ : Type} (f : List Γ → List Γ) : Prop

A function f : Σ* → Σ* is polynomial-time computable: there exists a deterministic TM F that, on input w, halts within |w|^k steps with f w written on the prefix of its tape.

def TuringMachine.PolyReducible {Γ : Type} (A B : Set (List Γ)) : Prop

Polynomial-time mapping reducibility A ≤ₚ B: there is a polynomial-time computable f with w ∈ A ↔ f w ∈ B.

def TuringMachine.«term_≤ₚ_» : Lean.TrailingParserDescr

Notation A ≤ₚ B for polynomial-time mapping reducibility.

def TuringMachine.InCoNP {Γ : Type} (A : Set (List Γ)) : Prop

The complexity class coNP: A ∈ coNP iff Aᶜ ∈ NP.

theorem TuringMachine.IsBigO.trans {f g h : ℕ → ℕ} (hfg : IsBigO f g) (hgh : IsBigO g h) : IsBigO f h

O(·) is transitive: if f = O(g) and g = O(h) then f = O(h).

noncomputable def TuringMachine.composedTM {Γ Q_F Q_B : Type} [DecidableEq Q_F] [DecidableEq Q_B] (F : TM Q_F Γ) (M_B : TM Q_B Γ) : TM ((Q_F ⊕ Q_B) ⊕ Fin 2) Γ

Sequential composition of TMs: run F to completion, then transfer control to M_B, finally collapsing M_B's accept/reject states to fresh accept/reject states of the composed machine. Used to reduce one decision problem to another.

theorem TuringMachine.inP_preimage_of_isPolyTimeComputableFunction {Γ : Type} (f : List Γ → List Γ) (B : Set (List Γ)) (hf : IsPolyTimeComputableFunction f) (hB : InP B) : InP {w : List Γ | f w ∈ B}

If f is polynomial-time computable and B ∈ P, then {w | f w ∈ B} ∈ P. This is the key technical lemma behind A ≤ₚ B ∧ B ∈ P → A ∈ P.

theorem TuringMachine.inP_of_polyReducible_inP {Γ : Type} {A B : Set (List Γ)} (hAB : PolyReducible A B) (hB : InP B) : InP A

Sipser, Lecture 14. If A ≤ₚ B and B ∈ P, then A ∈ P.

def TuringMachine.IsNPHard {Γ : Type} (B : Set (List Γ)) : Prop

B is NP-hard: every A ∈ NP polynomial-time reduces to B.

def TuringMachine.IsNPComplete {Γ : Type} (B : Set (List Γ)) : Prop

B is NP-complete: B ∈ NP and B is NP-hard.