def TuringMachine.Config.readTape {Γ Q : Type} (c : Config Q Γ) (n : ℕ) : List Γ

Read the first n cells of the tape of configuration c as a list.

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

A function f : Σ* → Σ* is (Turing-)computable if there is a TM F that, on every input w, halts with the string f w written as the prefix of its tape.

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

Mapping reducibility A ≤ₘ B: there is a computable function f with w ∈ A ↔ f w ∈ B (Sipser, Lecture 9).

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

Notation A ≤ₘ B for mapping reducibility.

theorem TuringMachine.transducerRecognizerComposition {Γ : Type} (f : List Γ → List Γ) (hf : IsComputableFunction f) {QR : Type} [DecidableEq QR] (R : TM QR Γ) : ∃ (QS : Type), ∃ (x : DecidableEq QS), ∃ (S : TM QS Γ), ∀ (w : List Γ), S.accepts w ↔ R.accepts (f w)

Given a transducer for the computable function f and a recognizer R for some language, there exists a single TM S whose acceptance behavior on input w mirrors R's behavior on f w. (Composition of TMs.)

theorem TuringMachine.isTuringRecognizable_of_mappingReducible {Γ : Type} {A B : Set (List Γ)} (hAB : MappingReducible A B) (hB : IsTuringRecognizable B) : IsTuringRecognizable A

Sipser, Lecture 9. If A ≤ₘ B and B is Turing-recognizable, then A is Turing-recognizable.

theorem TuringMachine.not_isTuringRecognizable_of_mappingReducible {Γ : Type} {A B : Set (List Γ)} (hAB : MappingReducible A B) (hA : ¬IsTuringRecognizable A) : ¬IsTuringRecognizable B

Sipser, Corollary in Lecture 9. If A ≤ₘ B and A is T-unrecognizable, then so is B. Contrapositive form of isTuringRecognizable_of_mappingReducible.