Imports

/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module

public import Geb.Prototypes.Computability.BitTree.BinaryMachine.Execution
public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas

set_option doc.verso true

Linear-time recognition with logarithmic work space

The binary-counter machine decides the unified tree-and-payload grammar using linear time and work space bounded by a constant multiple of the input length's binary size. Each input bit is consumed once. Carry and return steps leave the input head stationary.

Main statements

computableInTimeAndSpace_validBool gives explicit simultaneous time and space bounds in CSLib's finite-state, finite-alphabet machine model.

Implementation notes

The bound counts every visited work-tape cell, including blank cells. The read-only input tape is excluded by CSLib's space definition. Binary size is Nat.size, the number of digits in the binary representation.

Tags

binary tree, bitstring, Turing machine, linear time, logarithmic space

              @[expose] public sectionnamespace Geb.BitTree.BinaryMachineopen Turing MultiTapeTM

After all input macros, one final transition halts the machine.

theorem halts_at (w : List Bool) :
    (machine.configs (machine.initCfg (w.map boolEmb)) (2 + runCost w + 1)).state = none := byw:List Bool⊢ (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w + 1)).state = none
  have h := configs_account w w.length (Nat.le_refl _)w:List Boolh:have cost := 2 + runCost (List.take w.length w);
have now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
have s := account (List.take w.length w);
Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
  ↑now.inputPos = w.length + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w + 1)).state = none
  simp only [List.take_length] at hw:List Boolh:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
    (account w).forks (account w).leaves ∧
  ↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = [] ∧
      ∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w + 1)).state = none
  obtain ⟨hr, hp, _, _⟩ := hw:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []right✝:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w + 1)).state = none
  have hi := inputSymbol_end
    (machine.configs (machine.initCfg (w.map boolEmb)) (2 + runCost w))
    (byw:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []right✝:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ ↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = (List.map (⇑boolEmb) w).length + 1 simpa only [List.length_map] using hpAll goals completed! 🐙)w:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []right✝:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hi:(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputSymbol = none⊢ (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w + 1)).state = none
  rw [configs_succ_eq_step',w:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []right✝:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hi:(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputSymbol = none⊢ (MultiTapeTM.step (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w))).state = none step_end _ _ hr.state hiw:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []right✝:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hi:(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputSymbol = none⊢ { state := none, inputPos := (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos,
      workTapes := (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).workTapes,
      workTapePos := (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).workTapePos }.state =
  none]All goals completed! 🐙

The sole emitted bit is the decision of the unified scanner.

theorem outputString_eq (w : List Bool) :
    machine.outputString (machine.initCfg (w.map boolEmb)) (2 + runCost w + 1) =
      [boolEmb (validBool w)] := byw:List Bool⊢ machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w + 1) = [boolEmb (validBool w)]
  have h := configs_account w w.length (Nat.le_refl _)w:List Boolh:have cost := 2 + runCost (List.take w.length w);
have now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
have s := account (List.take w.length w);
Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
  ↑now.inputPos = w.length + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w + 1) = [boolEmb (validBool w)]
  simp only [List.take_length] at hw:List Boolh:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
    (account w).forks (account w).leaves ∧
  ↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = [] ∧
      ∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w + 1) = [boolEmb (validBool w)]
  obtain ⟨hr, hp, ho, _⟩ := hw:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []right✝:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w + 1) = [boolEmb (validBool w)]
  have hi := inputSymbol_end
    (machine.configs (machine.initCfg (w.map boolEmb)) (2 + runCost w))
    (byw:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []right✝:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ ↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = (List.map (⇑boolEmb) w).length + 1 simpa only [List.length_map] using hpAll goals completed! 🐙)w:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []right✝:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hi:(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputSymbol = none⊢ machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w + 1) = [boolEmb (validBool w)]
  have hm : (account w).mode = (scan w).1 := congrArg Prod.fst (account_project w)w:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []right✝:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hi:(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputSymbol = nonehm:(account w).mode = (scan w).1⊢ machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w + 1) = [boolEmb (validBool w)]
  rw [outputString_succ,w:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []right✝:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hi:(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputSymbol = nonehm:(account w).mode = (scan w).1⊢ machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) ++
    (outputSymbol (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w))).toList =
  [boolEmb (validBool w)] ho,w:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []right✝:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hi:(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputSymbol = nonehm:(account w).mode = (scan w).1⊢ [] ++ (outputSymbol (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w))).toList = [boolEmb (validBool w)] outputSymbol_end _ _ hr.state hi,w:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []right✝:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hi:(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputSymbol = nonehm:(account w).mode = (scan w).1⊢ [] ++ (some (boolEmb (decide ((account w).mode = Mode.done)))).toList = [boolEmb (validBool w)] hmw:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []right✝:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hi:(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputSymbol = nonehm:(account w).mode = (scan w).1⊢ [] ++ (some (boolEmb (decide ((scan w).1 = Mode.done)))).toList = [boolEmb (validBool w)]]w:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []right✝:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hi:(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputSymbol = nonehm:(account w).mode = (scan w).1⊢ [] ++ (some (boolEmb (decide ((scan w).1 = Mode.done)))).toList = [boolEmb (validBool w)]
  rflAll goals completed! 🐙

A bounded interval for every work head bounds the total visited work space.

theorem spaceUsed_le_of_headBound {input : List (Fin 4)}
    (cfg : Cfg 3 (Fin 4) (Fin 10) input) (width t : ℕ)
    (h : ∀ u ≤ t, HeadBound width (machine.configs cfg u)) :
    machine.spaceUsed cfg t ≤ 3 * (width + 1) := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)⊢ spaceUsed cfg t ≤ 3 * (width + 1)
  have hsub (i : Fin 3) : machine.visitedByTapeHead cfg t i ⊆
      (Finset.range (width + 1)).image (fun n : ℕ ↦ (n : ℤ)) := by
    intro z hzinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)i:Fin 3z:ℤhz:z ∈ visitedByTapeHead cfg t i⊢ z ∈ Finset.image (fun n ↦ ↑n) (Finset.range (width + 1))
    obtain ⟨u, hu, rfl⟩ := machine.mem_visitedByTapeHead.mp hzinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)i:Fin 3u:ℕhu:u < t + 1hz:(configs cfg u).workTapePos i ∈ visitedByTapeHead cfg t i⊢ (configs cfg u).workTapePos i ∈ Finset.image (fun n ↦ ↑n) (Finset.range (width + 1))
    obtain ⟨hlo, hhi⟩ := h u (byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)i:Fin 3u:ℕhu:u < t + 1hz:(configs cfg u).workTapePos i ∈ visitedByTapeHead cfg t i⊢ u ≤ t omegaAll goals completed! 🐙) iinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)i:Fin 3u:ℕhu:u < t + 1hz:(configs cfg u).workTapePos i ∈ visitedByTapeHead cfg t ihlo:0 ≤ (configs cfg u).workTapePos ihhi:(configs cfg u).workTapePos i ≤ ↑width⊢ (configs cfg u).workTapePos i ∈ Finset.image (fun n ↦ ↑n) (Finset.range (width + 1))
    apply Finset.mem_image.mprinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)i:Fin 3u:ℕhu:u < t + 1hz:(configs cfg u).workTapePos i ∈ visitedByTapeHead cfg t ihlo:0 ≤ (configs cfg u).workTapePos ihhi:(configs cfg u).workTapePos i ≤ ↑width⊢ ∃ a ∈ Finset.range (width + 1), ↑a = (configs cfg u).workTapePos i
    refine ⟨_, Finset.mem_range.mpr ?_, Int.toNat_of_nonneg hlo⟩input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)i:Fin 3u:ℕhu:u < t + 1hz:(configs cfg u).workTapePos i ∈ visitedByTapeHead cfg t ihlo:0 ≤ (configs cfg u).workTapePos ihhi:(configs cfg u).workTapePos i ≤ ↑width⊢ ((configs cfg u).workTapePos i).toNat < width + 1
    omegainput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)hsub:∀ (i : Fin 3), visitedByTapeHead cfg t i ⊆ Finset.image (fun n ↦ ↑n) (Finset.range (width + 1))⊢ spaceUsed cfg t ≤ 3 * (width + 1)
  have hi (i : Fin 3) : machine.spaceUsedByTape cfg t i ≤ width + 1 :=
    (Finset.card_le_card (hsub i)).trans (Finset.card_image_le.trans (byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)hsub:∀ (i : Fin 3), visitedByTapeHead cfg t i ⊆ Finset.image (fun n ↦ ↑n) (Finset.range (width + 1))i:Fin 3⊢ (Finset.range (width + 1)).card ≤ width + 1 simpAll goals completed! 🐙))input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)hsub:∀ (i : Fin 3), visitedByTapeHead cfg t i ⊆ Finset.image (fun n ↦ ↑n) (Finset.range (width + 1))hi:∀ (i : Fin 3), spaceUsedByTape cfg t i ≤ width + 1⊢ spaceUsed cfg t ≤ 3 * (width + 1)
  calc
    machine.spaceUsed cfg t ≤ ∑ _i : Fin 3, (width + 1) :=
      Finset.sum_le_sum (fun i _ ↦ hi i)
    _ = 3 * (width + 1) := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕt:ℕh:∀ u ≤ t, HeadBound width (configs cfg u)hsub:∀ (i : Fin 3), visitedByTapeHead cfg t i ⊆ Finset.image (fun n ↦ ↑n) (Finset.range (width + 1))hi:∀ (i : Fin 3), spaceUsedByTape cfg t i ≤ width + 1⊢ ∑ _i, (width + 1) = 3 * (width + 1) simpAll goals completed! 🐙

All work-head positions remain within the chosen binary width, including the halt step.

theorem headBound_run (w : List Bool) :
    ∀ u ≤ 2 + runCost w + 1, HeadBound (w.length + 2).size
      (machine.configs (machine.initCfg (w.map boolEmb)) u) := byw:List Bool⊢ ∀ u ≤ 2 + runCost w + 1, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
  have h := configs_account w w.length (Nat.le_refl _)w:List Boolh:have cost := 2 + runCost (List.take w.length w);
have now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
have s := account (List.take w.length w);
Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
  ↑now.inputPos = w.length + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ ∀ u ≤ 2 + runCost w + 1, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
  simp only [List.take_length] at hw:List Boolh:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
    (account w).forks (account w).leaves ∧
  ↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = [] ∧
      ∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ ∀ u ≤ 2 + runCost w + 1, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
  obtain ⟨hr, hp, _, hh⟩ := hw:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []hh:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ ∀ u ≤ 2 + runCost w + 1, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
  intro u huw:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []hh:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)u:ℕhu:u ≤ 2 + runCost w + 1⊢ HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
  by_cases he : u ≤ 2 + runCost wposw:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []hh:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)u:ℕhu:u ≤ 2 + runCost w + 1he:u ≤ 2 + runCost w⊢ HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)negw:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []hh:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)u:ℕhu:u ≤ 2 + runCost w + 1he:¬u ≤ 2 + runCost w⊢ HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
  ·posw:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []hh:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)u:ℕhu:u ≤ 2 + runCost w + 1he:u ≤ 2 + runCost w⊢ HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u) exact hh u heAll goals completed! 🐙
  ·negw:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []hh:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)u:ℕhu:u ≤ 2 + runCost w + 1he:¬u ≤ 2 + runCost w⊢ HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u) have hu' : u = 2 + runCost w + 1 := byw:List Bool⊢ ∀ u ≤ 2 + runCost w + 1, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u) omeganegw:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []hh:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)u:ℕhu:u ≤ 2 + runCost w + 1he:¬u ≤ 2 + runCost whu':u = 2 + runCost w + 1⊢ HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
    subst unegw:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []hh:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hu:2 + runCost w + 1 ≤ 2 + runCost w + 1he:¬2 + runCost w + 1 ≤ 2 + runCost w⊢ HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w + 1))
    have hi := inputSymbol_end
      (machine.configs (machine.initCfg (w.map boolEmb)) (2 + runCost w))
      (byw:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []hh:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hu:2 + runCost w + 1 ≤ 2 + runCost w + 1he:¬2 + runCost w + 1 ≤ 2 + runCost w⊢ ↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = (List.map (⇑boolEmb) w).length + 1 simpa only [List.length_map] using hpAll goals completed! 🐙)negw:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []hh:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hu:2 + runCost w + 1 ≤ 2 + runCost w + 1he:¬2 + runCost w + 1 ≤ 2 + runCost whi:(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputSymbol = none⊢ HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w + 1))
    rw [configs_succ_eq_step',negw:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []hh:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hu:2 + runCost w + 1 ≤ 2 + runCost w + 1he:¬2 + runCost w + 1 ≤ 2 + runCost whi:(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputSymbol = none⊢ HeadBound (w.length + 2).size (MultiTapeTM.step (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w))) step_end _ _ hr.state hinegw:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []hh:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hu:2 + runCost w + 1 ≤ 2 + runCost w + 1he:¬2 + runCost w + 1 ≤ 2 + runCost whi:(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputSymbol = none⊢ HeadBound (w.length + 2).size
  { state := none, inputPos := (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos,
    workTapes := (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).workTapes,
    workTapePos := (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).workTapePos }]negw:List Boolhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)) (modeState (account w).mode)
  (account w).forks (account w).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos = w.length + 1left✝:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w) = []hh:∀ u ≤ 2 + runCost w, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hu:2 + runCost w + 1 ≤ 2 + runCost w + 1he:¬2 + runCost w + 1 ≤ 2 + runCost whi:(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputSymbol = none⊢ HeadBound (w.length + 2).size
  { state := none, inputPos := (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).inputPos,
    workTapes := (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).workTapes,
    workTapePos := (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost w)).workTapePos }
    exact hr.headBoundAll goals completed! 🐙

Recognition takes linear time and logarithmic work space simultaneously.

theorem computableInTimeAndSpace_validBool :
    ComputableInTimeAndSpace (fun w : List Bool ↦ [validBool w])
      (fun n ↦ 6 * n + 5) (fun n ↦ 3 * ((n + 2).size + 1)) := by⊢ ComputableInTimeAndSpace (fun w ↦ [validBool w]) (fun n ↦ 6 * n + 5) fun n ↦ 3 * ((n + 2).size + 1)
  refine ⟨3, 4, 10, boolEmb, machine, fun w ↦ ?_⟩w:List Bool⊢ ∃ t' ≤ (fun n ↦ 6 * n + 5) w.length,
  ∃ s' ≤ (fun n ↦ 3 * ((n + 2).size + 1)) w.length,
    machine.ComputesInTimeAndSpace (List.map (⇑boolEmb) w) (List.map (⇑boolEmb) ((fun w ↦ [validBool w]) w)) t' s'
  refine ⟨2 + runCost w + 1, ?_,
    machine.spaceUsed (machine.initCfg (w.map boolEmb)) (2 + runCost w + 1),
    spaceUsed_le_of_headBound _ _ _ (headBound_run w),
    halts_at w, outputString_eq w, rfl⟩w:List Bool⊢ 2 + runCost w + 1 ≤ (fun n ↦ 6 * n + 5) w.length
  change 2 + runCost w + 1 ≤ 6 * w.length + 5w:List Bool⊢ 2 + runCost w + 1 ≤ 6 * w.length + 5
  have h := runCost_le ww:List Boolh:runCost w ≤ 6 * w.length + 2⊢ 2 + runCost w + 1 ≤ 6 * w.length + 5
  omegaAll goals completed! 🐙

end Geb.BitTree.BinaryMachine