noncomputable def TuringMachine.TM.sequentialCompose {Q₁ Q₂ Γ : Type} [DecidableEq Q₁] [DecidableEq Q₂] (M₁ : TM Q₁ Γ) (M₂ : TM Q₂ Γ) : TM ((Q₁ ⊕ Q₂) ⊕ Fin 2) Γ

Sequential composition of two Turing machines M₁ and M₂ sharing the same tape alphabet Γ. The composite machine runs M₁ first; whenever M₁ would halt (accept or reject) it transitions to M₂.q₀ instead and continues with M₂. The composite then accepts iff M₂ accepts and rejects iff M₂ rejects. The state space (Q₁ ⊕ Q₂) ⊕ Fin 2 keeps each machine's states in its own copy and uses the final Fin 2 for the new accept/reject states.

theorem TuringMachine.TM.run_add' {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (c : Config Q Γ) (m n : ℕ) : M.run c (m + n) = M.run (M.run c m) n

Running a TM for m + n steps is the same as running it for m steps followed by n steps. A basic additivity lemma for TM.run.

theorem TuringMachine.sequentialCompose_phase1_run {Q₁ Q₂ Γ : Type} [DecidableEq Q₁] [DecidableEq Q₂] (M₁ : TM Q₁ Γ) (M₂ : TM Q₂ Γ) (c : Config Q₁ Γ) (n : ℕ) (hNotHalt : ∀ (k : ℕ), k < n → ¬M₁.isHaltConfig (M₁.run c k)) : (M₁.sequentialCompose M₂).run { state := Sum.inl (Sum.inl c.state), headPos := c.headPos, tape := c.tape } n = { state := Sum.inl (Sum.inl (M₁.run c n).state), headPos := (M₁.run c n).headPos, tape := (M₁.run c n).tape }

Phase-1 simulation lemma: as long as M₁ has not yet halted, running the composite machine sequentialCompose M₁ M₂ for n steps from a configuration whose state lies in inl ∘ inl mirrors running M₁ itself for n steps, keeping the state, head position and tape in sync.

theorem TuringMachine.sequentialCompose_phase2_run {Q₁ Q₂ Γ : Type} [DecidableEq Q₁] [DecidableEq Q₂] (M₁ : TM Q₁ Γ) (M₂ : TM Q₂ Γ) (c : Config Q₂ Γ) (n : ℕ) (hNotHalt : ∀ (k : ℕ), k < n → ¬M₂.isHaltConfig (M₂.run c k)) : (M₁.sequentialCompose M₂).run { state := Sum.inl (Sum.inr c.state), headPos := c.headPos, tape := c.tape } n = { state := Sum.inl (Sum.inr (M₂.run c n).state), headPos := (M₂.run c n).headPos, tape := (M₂.run c n).tape }

Phase-2 simulation lemma: as long as M₂ has not yet halted, running the composite machine for n steps from a configuration whose state lies in inl ∘ inr mirrors running M₂ itself for n steps.

theorem TuringMachine.sequentialCompose_transition_step {Q₁ Q₂ Γ : Type} [DecidableEq Q₁] [DecidableEq Q₂] (M₁ : TM Q₁ Γ) (M₂ : TM Q₂ Γ) (q₁ : Q₁) (headPos : ℤ) (tape : Tape Γ) (hHalt : q₁ = M₁.qAccept ∨ q₁ = M₁.qReject) : (M₁.sequentialCompose M₂).step { state := Sum.inl (Sum.inl q₁), headPos := headPos, tape := tape } = { state := Sum.inl (Sum.inr M₂.q₀), headPos := headPos + 1, tape := tape }

The "handoff" step: when the composite machine is in a state corresponding to either M₁.qAccept or M₁.qReject, one step transitions to M₂.q₀ (without modifying the tape), moving the head one cell to the right.

noncomputable def TuringMachine.phase2InitConfig {Q₁ Q₂ Γ : Type} [DecidableEq Q₁] (M₁ : TM Q₁ Γ) (M₂ : TM Q₂ Γ) (w : List Γ) (n₁ : ℕ) : Config Q₂ Γ

The starting configuration of M₂ in the composite execution: take the configuration M₁ reaches after n₁ steps on input w, move the head one cell right, and set the state to M₂.q₀.

theorem TuringMachine.sequentialCompose_phase1_from_init {Q₁ Q₂ Γ : Type} [DecidableEq Q₁] [DecidableEq Q₂] (M₁ : TM Q₁ Γ) (M₂ : TM Q₂ Γ) (w : List Γ) (n₁ : ℕ) (hNotHalt₁ : ∀ (k : ℕ), k < n₁ → ¬M₁.isHaltConfig (M₁.runOnInput w k)) : have M₃ := M₁.sequentialCompose M₂; M₃.run (M₃.initConfig w) n₁ = { state := Sum.inl (Sum.inl (M₁.runOnInput w n₁).state), headPos := (M₁.runOnInput w n₁).headPos, tape := (M₁.runOnInput w n₁).tape }

Specialisation of sequentialCompose_phase1_run starting from the composite machine's initial configuration on input w: provided M₁ does not halt in fewer than n₁ steps, after n₁ steps the composite tracks M₁.runOnInput w n₁.

theorem TuringMachine.sequentialCompose_accepts_of_phases {Q₁ Q₂ Γ : Type} [DecidableEq Q₁] [DecidableEq Q₂] (M₁ : TM Q₁ Γ) (M₂ : TM Q₂ Γ) (w : List Γ) (n₁ : ℕ) (hHalt₁ : M₁.isHaltConfig (M₁.runOnInput w n₁)) (hNotHalt₁ : ∀ (k : ℕ), k < n₁ → ¬M₁.isHaltConfig (M₁.runOnInput w k)) (n₂ : ℕ) (hAccept₂ : M₂.isAcceptConfig (M₂.run (phase2InitConfig M₁ M₂ w n₁) n₂)) (hNotHalt₂ : ∀ (k : ℕ), k < n₂ → ¬M₂.isHaltConfig (M₂.run (phase2InitConfig M₁ M₂ w n₁) k)) : (M₁.sequentialCompose M₂).accepts w

Acceptance of the sequential composition: if M₁ halts after exactly n₁ steps on w, and M₂ started in phase2InitConfig M₁ M₂ w n₁ halts in the accept state after exactly n₂ steps, then sequentialCompose M₁ M₂ accepts w (in n₁ + 1 + n₂ + 1 steps).

theorem TuringMachine.sequentialCompose_rejects_of_phases {Q₁ Q₂ Γ : Type} [DecidableEq Q₁] [DecidableEq Q₂] (M₁ : TM Q₁ Γ) (M₂ : TM Q₂ Γ) (w : List Γ) (n₁ : ℕ) (hHalt₁ : M₁.isHaltConfig (M₁.runOnInput w n₁)) (hNotHalt₁ : ∀ (k : ℕ), k < n₁ → ¬M₁.isHaltConfig (M₁.runOnInput w k)) (n₂ : ℕ) (hReject₂ : M₂.isRejectConfig (M₂.run (phase2InitConfig M₁ M₂ w n₁) n₂)) (hNotHalt₂ : ∀ (k : ℕ), k < n₂ → ¬M₂.isHaltConfig (M₂.run (phase2InitConfig M₁ M₂ w n₁) k)) : (M₁.sequentialCompose M₂).rejects w

Rejection of the sequential composition: if M₁ halts after n₁ steps on w and M₂ started in phase2InitConfig M₁ M₂ w n₁ halts in the reject state after n₂ steps, then sequentialCompose M₁ M₂ rejects w.