The existing conditional machine and its run theorem

Machine declarations are moved from their original module without changing programs or resource formulas. Higher computability-calculus theorems remain in the original facade.

noncomputable def Turing.MultiTapeTM.iteTM {k₀ k₁ k₂ : ℕ} {Symbol : Type u_1} {S₀ : Type u_2} {S₁ : Type u_3} {S₂ : Type u_4} (tmc : MultiTapeTM k₀ Symbol S₀) (tm₁ : MultiTapeTM k₁ Symbol S₁) (tm₂ : MultiTapeTM k₂ Symbol S₂) : MultiTapeTM (max k₀ (max k₁ k₂) + 1) Symbol ((S₀ ⊕ RewindWorkState) ⊕ Option (S₁ ⊕ S₂) ⊕ Unit ⊕ RewindWorkState)

Run tmc with its output on a new last work tape, then tm₁ if that word is non-empty and tm₂ otherwise, and clear the tape. All three machines are padded to max k₀ (max k₁ k₂) work tapes.

theorem Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.ite {k₀ k₁ k₂ : ℕ} {Symbol : Type u_1} {S₀ : Type u_2} {S₁ : Type u_3} {S₂ : Type u_4} {tmc : MultiTapeTM k₀ Symbol S₀} {tm₁ : MultiTapeTM k₁ Symbol S₁} {tm₂ : MultiTapeTM k₂ Symbol S₂} {x w y : List Symbol} {tc sc t₁ s₁ t₂ s₂ : ℕ} (hc : tmc.ComputesTidilyInTimeAndSpace x w tc sc) (h₁ : w ≠ [] → tm₁.ComputesTidilyInTimeAndSpace x y t₁ s₁) (h₂ : w = [] → tm₂.ComputesTidilyInTimeAndSpace x y t₂ s₂) : (tmc.iteTM tm₁ tm₂).ComputesTidilyInTimeAndSpace x y ((tc + if w = [] then t₂ else t₁) + 4 * w.length + 6) ((sc + if w = [] then s₂ else s₁) + 3 * w.length + 5 * max k₀ (max k₁ k₂) + 10)

If tmc computes w from x tidily, tm₁ computes y from x tidily when w is non-empty and tm₂ does when w is empty, then iteTM tmc tm₁ tm₂ computes y from x tidily, within the bounds of tmc plus those of the machine that runs.

def Turing.MultiTapeTM.encTest : Bool ↪ List Bool

The test word of a condition: empty exactly for false.

theorem Turing.MultiTapeTM.encTest_true : encTest true = [true]

theorem Turing.MultiTapeTM.encTest_false : encTest false = []

def Turing.MultiTapeTM.eqWordT (w : List Bool) : Transducer Bool (Option { v : List Bool // v ∈ w.tails })

Emits [true] on the word w and nothing on every other word. Its state is the rest of w still to be read, or none once the input differs from w.

theorem Turing.MultiTapeTM.eqWordT_step (w : List Bool) (q : Option { v : List Bool // v ∈ w.tails }) (a : Bool) : (eqWordT w).step q a = match q with | some ⟨b :: v, h⟩ => (if a = b then some ⟨v, ⋯⟩ else none, []) | x => (none, [])

theorem Turing.MultiTapeTM.eqWordT_final (w : List Bool) (q : Option { v : List Bool // v ∈ w.tails }) : (eqWordT w).final q = if Option.map Subtype.val q = some [] then [true] else []

theorem Turing.MultiTapeTM.eqWordT_run_q₀ (w u : List Bool) : (eqWordT w).run (eqWordT w).q₀ u = if u = w then [true] else []