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.Steps
public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas

set_option doc.verso true

Time and space bounds for the single-pass bitstring-tree recognizer

The unary-counter machine takes one transition per input bit, two initialization transitions and a final output transition. Its visited work cells lie between zero and one plus the input length.

Main statements

computableInTimeAndSpace_validBool packages the recognizer in CSLib's finite-alphabet, finite-state machine complexity predicate.

Implementation notes

The space bound counts visited work cells, including blank cells. It excludes the read-only input tape, as specified by CSLib. The bound is for this unary implementation and is not a lower bound on recognition space.

Tags

binary tree, bitstring, time complexity, space complexity, Turing machine

              @[expose] public sectionnamespace Geb.BitTreeopen Turing MultiTapeTMopen Geb.TreeScanner (boolEmb step_of_state)

The final output transition leaves the work head in place.

theorem end_workTapePos (w : List Bool) (s : State) (i : Fin 1) :
    (unaryScanner.step (scanCfg w w.length (byw:List Bools:Statei:Fin 1⊢ w.length ≤ w.length omegaAll goals completed! 🐙) s)).workTapePos i = s.2 := byw:List Bools:Statei:Fin 1⊢ (MultiTapeTM.step (scanCfg w w.length ⋯ s)).workTapePos i = ↑s.2
  rw [step_of_state _ _ (modeState s.1) rfl,w:List Bools:Statei:Fin 1⊢ {
        state :=
          (unaryScanner.tr (modeState s.1) (scanCfg w w.length ⋯ s).inputSymbol
              (scanCfg w w.length ⋯ s).workTapeSymbols).q',
        inputPos :=
          moveInputPos (scanCfg w w.length ⋯ s).inputPos
            (unaryScanner.tr (modeState s.1) (scanCfg w w.length ⋯ s).inputSymbol
                (scanCfg w w.length ⋯ s).workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
            ((unaryScanner.tr (modeState s.1) (scanCfg w w.length ⋯ s).inputSymbol
                    (scanCfg w w.length ⋯ s).workTapeSymbols).workActions
                i).1 with
          | none => (scanCfg w w.length ⋯ s).workTapes i
          | some s_1 =>
            Function.update ((scanCfg w w.length ⋯ s).workTapes i) ((scanCfg w w.length ⋯ s).workTapePos i) s_1,
        workTapePos := fun i ↦
          (scanCfg w w.length ⋯ s).workTapePos i +
            ↑((unaryScanner.tr (modeState s.1) (scanCfg w w.length ⋯ s).inputSymbol
                      (scanCfg w w.length ⋯ s).workTapeSymbols).workActions
                  i).2 }.workTapePos
    i =
  ↑s.2 scanCfg_inputSymbol_endw:List Bools:Statei:Fin 1⊢ { state := (unaryScanner.tr (modeState s.1) none (scanCfg w w.length ⋯ s).workTapeSymbols).q',
        inputPos :=
          moveInputPos (scanCfg w w.length ⋯ s).inputPos
            (unaryScanner.tr (modeState s.1) none (scanCfg w w.length ⋯ s).workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
            ((unaryScanner.tr (modeState s.1) none (scanCfg w w.length ⋯ s).workTapeSymbols).workActions i).1 with
          | none => (scanCfg w w.length ⋯ s).workTapes i
          | some s_1 =>
            Function.update ((scanCfg w w.length ⋯ s).workTapes i) ((scanCfg w w.length ⋯ s).workTapePos i) s_1,
        workTapePos := fun i ↦
          (scanCfg w w.length ⋯ s).workTapePos i +
            ↑((unaryScanner.tr (modeState s.1) none (scanCfg w w.length ⋯ s).workTapeSymbols).workActions
                  i).2 }.workTapePos
    i =
  ↑s.2]w:List Bools:Statei:Fin 1⊢ { state := (unaryScanner.tr (modeState s.1) none (scanCfg w w.length ⋯ s).workTapeSymbols).q',
        inputPos :=
          moveInputPos (scanCfg w w.length ⋯ s).inputPos
            (unaryScanner.tr (modeState s.1) none (scanCfg w w.length ⋯ s).workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
            ((unaryScanner.tr (modeState s.1) none (scanCfg w w.length ⋯ s).workTapeSymbols).workActions i).1 with
          | none => (scanCfg w w.length ⋯ s).workTapes i
          | some s_1 =>
            Function.update ((scanCfg w w.length ⋯ s).workTapes i) ((scanCfg w w.length ⋯ s).workTapePos i) s_1,
        workTapePos := fun i ↦
          (scanCfg w w.length ⋯ s).workTapePos i +
            ↑((unaryScanner.tr (modeState s.1) none (scanCfg w w.length ⋯ s).workTapeSymbols).workActions
                  i).2 }.workTapePos
    i =
  ↑s.2
  rcases s with ⟨m, n⟩w:List Booli:Fin 1m:Moden:ℕ⊢ { state := (unaryScanner.tr (modeState (m, n).1) none (scanCfg w w.length ⋯ (m, n)).workTapeSymbols).q',
        inputPos :=
          moveInputPos (scanCfg w w.length ⋯ (m, n)).inputPos
            (unaryScanner.tr (modeState (m, n).1) none (scanCfg w w.length ⋯ (m, n)).workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
            ((unaryScanner.tr (modeState (m, n).1) none (scanCfg w w.length ⋯ (m, n)).workTapeSymbols).workActions
                i).1 with
          | none => (scanCfg w w.length ⋯ (m, n)).workTapes i
          | some s =>
            Function.update ((scanCfg w w.length ⋯ (m, n)).workTapes i) ((scanCfg w w.length ⋯ (m, n)).workTapePos i) s,
        workTapePos := fun i ↦
          (scanCfg w w.length ⋯ (m, n)).workTapePos i +
            ↑((unaryScanner.tr (modeState (m, n).1) none (scanCfg w w.length ⋯ (m, n)).workTapeSymbols).workActions
                  i).2 }.workTapePos
    i =
  ↑(m, n).2
  cases mtreew:List Booli:Fin 1n:ℕ⊢ { state := (unaryScanner.tr (modeState (Mode.tree, n).1) none (scanCfg w w.length ⋯ (Mode.tree, n)).workTapeSymbols).q',
        inputPos :=
          moveInputPos (scanCfg w w.length ⋯ (Mode.tree, n)).inputPos
            (unaryScanner.tr (modeState (Mode.tree, n).1) none
                (scanCfg w w.length ⋯ (Mode.tree, n)).workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
            ((unaryScanner.tr (modeState (Mode.tree, n).1) none
                    (scanCfg w w.length ⋯ (Mode.tree, n)).workTapeSymbols).workActions
                i).1 with
          | none => (scanCfg w w.length ⋯ (Mode.tree, n)).workTapes i
          | some s =>
            Function.update ((scanCfg w w.length ⋯ (Mode.tree, n)).workTapes i)
              ((scanCfg w w.length ⋯ (Mode.tree, n)).workTapePos i) s,
        workTapePos := fun i ↦
          (scanCfg w w.length ⋯ (Mode.tree, n)).workTapePos i +
            ↑((unaryScanner.tr (modeState (Mode.tree, n).1) none
                      (scanCfg w w.length ⋯ (Mode.tree, n)).workTapeSymbols).workActions
                  i).2 }.workTapePos
    i =
  ↑(Mode.tree, n).2stringw:List Booli:Fin 1n:ℕ⊢ {
        state :=
          (unaryScanner.tr (modeState (Mode.string, n).1) none
              (scanCfg w w.length ⋯ (Mode.string, n)).workTapeSymbols).q',
        inputPos :=
          moveInputPos (scanCfg w w.length ⋯ (Mode.string, n)).inputPos
            (unaryScanner.tr (modeState (Mode.string, n).1) none
                (scanCfg w w.length ⋯ (Mode.string, n)).workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
            ((unaryScanner.tr (modeState (Mode.string, n).1) none
                    (scanCfg w w.length ⋯ (Mode.string, n)).workTapeSymbols).workActions
                i).1 with
          | none => (scanCfg w w.length ⋯ (Mode.string, n)).workTapes i
          | some s =>
            Function.update ((scanCfg w w.length ⋯ (Mode.string, n)).workTapes i)
              ((scanCfg w w.length ⋯ (Mode.string, n)).workTapePos i) s,
        workTapePos := fun i ↦
          (scanCfg w w.length ⋯ (Mode.string, n)).workTapePos i +
            ↑((unaryScanner.tr (modeState (Mode.string, n).1) none
                      (scanCfg w w.length ⋯ (Mode.string, n)).workTapeSymbols).workActions
                  i).2 }.workTapePos
    i =
  ↑(Mode.string, n).2bitw:List Booli:Fin 1n:ℕ⊢ { state := (unaryScanner.tr (modeState (Mode.bit, n).1) none (scanCfg w w.length ⋯ (Mode.bit, n)).workTapeSymbols).q',
        inputPos :=
          moveInputPos (scanCfg w w.length ⋯ (Mode.bit, n)).inputPos
            (unaryScanner.tr (modeState (Mode.bit, n).1) none
                (scanCfg w w.length ⋯ (Mode.bit, n)).workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
            ((unaryScanner.tr (modeState (Mode.bit, n).1) none
                    (scanCfg w w.length ⋯ (Mode.bit, n)).workTapeSymbols).workActions
                i).1 with
          | none => (scanCfg w w.length ⋯ (Mode.bit, n)).workTapes i
          | some s =>
            Function.update ((scanCfg w w.length ⋯ (Mode.bit, n)).workTapes i)
              ((scanCfg w w.length ⋯ (Mode.bit, n)).workTapePos i) s,
        workTapePos := fun i ↦
          (scanCfg w w.length ⋯ (Mode.bit, n)).workTapePos i +
            ↑((unaryScanner.tr (modeState (Mode.bit, n).1) none
                      (scanCfg w w.length ⋯ (Mode.bit, n)).workTapeSymbols).workActions
                  i).2 }.workTapePos
    i =
  ↑(Mode.bit, n).2donew:List Booli:Fin 1n:ℕ⊢ { state := (unaryScanner.tr (modeState (Mode.done, n).1) none (scanCfg w w.length ⋯ (Mode.done, n)).workTapeSymbols).q',
        inputPos :=
          moveInputPos (scanCfg w w.length ⋯ (Mode.done, n)).inputPos
            (unaryScanner.tr (modeState (Mode.done, n).1) none
                (scanCfg w w.length ⋯ (Mode.done, n)).workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
            ((unaryScanner.tr (modeState (Mode.done, n).1) none
                    (scanCfg w w.length ⋯ (Mode.done, n)).workTapeSymbols).workActions
                i).1 with
          | none => (scanCfg w w.length ⋯ (Mode.done, n)).workTapes i
          | some s =>
            Function.update ((scanCfg w w.length ⋯ (Mode.done, n)).workTapes i)
              ((scanCfg w w.length ⋯ (Mode.done, n)).workTapePos i) s,
        workTapePos := fun i ↦
          (scanCfg w w.length ⋯ (Mode.done, n)).workTapePos i +
            ↑((unaryScanner.tr (modeState (Mode.done, n).1) none
                      (scanCfg w w.length ⋯ (Mode.done, n)).workTapeSymbols).workActions
                  i).2 }.workTapePos
    i =
  ↑(Mode.done, n).2deadw:List Booli:Fin 1n:ℕ⊢ { state := (unaryScanner.tr (modeState (Mode.dead, n).1) none (scanCfg w w.length ⋯ (Mode.dead, n)).workTapeSymbols).q',
        inputPos :=
          moveInputPos (scanCfg w w.length ⋯ (Mode.dead, n)).inputPos
            (unaryScanner.tr (modeState (Mode.dead, n).1) none
                (scanCfg w w.length ⋯ (Mode.dead, n)).workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
            ((unaryScanner.tr (modeState (Mode.dead, n).1) none
                    (scanCfg w w.length ⋯ (Mode.dead, n)).workTapeSymbols).workActions
                i).1 with
          | none => (scanCfg w w.length ⋯ (Mode.dead, n)).workTapes i
          | some s =>
            Function.update ((scanCfg w w.length ⋯ (Mode.dead, n)).workTapes i)
              ((scanCfg w w.length ⋯ (Mode.dead, n)).workTapePos i) s,
        workTapePos := fun i ↦
          (scanCfg w w.length ⋯ (Mode.dead, n)).workTapePos i +
            ↑((unaryScanner.tr (modeState (Mode.dead, n).1) none
                      (scanCfg w w.length ⋯ (Mode.dead, n)).workTapeSymbols).workActions
                  i).2 }.workTapePos
    i =
  ↑(Mode.dead, n).2 <;>treew:List Booli:Fin 1n:ℕ⊢ { state := (unaryScanner.tr (modeState (Mode.tree, n).1) none (scanCfg w w.length ⋯ (Mode.tree, n)).workTapeSymbols).q',
        inputPos :=
          moveInputPos (scanCfg w w.length ⋯ (Mode.tree, n)).inputPos
            (unaryScanner.tr (modeState (Mode.tree, n).1) none
                (scanCfg w w.length ⋯ (Mode.tree, n)).workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
            ((unaryScanner.tr (modeState (Mode.tree, n).1) none
                    (scanCfg w w.length ⋯ (Mode.tree, n)).workTapeSymbols).workActions
                i).1 with
          | none => (scanCfg w w.length ⋯ (Mode.tree, n)).workTapes i
          | some s =>
            Function.update ((scanCfg w w.length ⋯ (Mode.tree, n)).workTapes i)
              ((scanCfg w w.length ⋯ (Mode.tree, n)).workTapePos i) s,
        workTapePos := fun i ↦
          (scanCfg w w.length ⋯ (Mode.tree, n)).workTapePos i +
            ↑((unaryScanner.tr (modeState (Mode.tree, n).1) none
                      (scanCfg w w.length ⋯ (Mode.tree, n)).workTapeSymbols).workActions
                  i).2 }.workTapePos
    i =
  ↑(Mode.tree, n).2stringw:List Booli:Fin 1n:ℕ⊢ {
        state :=
          (unaryScanner.tr (modeState (Mode.string, n).1) none
              (scanCfg w w.length ⋯ (Mode.string, n)).workTapeSymbols).q',
        inputPos :=
          moveInputPos (scanCfg w w.length ⋯ (Mode.string, n)).inputPos
            (unaryScanner.tr (modeState (Mode.string, n).1) none
                (scanCfg w w.length ⋯ (Mode.string, n)).workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
            ((unaryScanner.tr (modeState (Mode.string, n).1) none
                    (scanCfg w w.length ⋯ (Mode.string, n)).workTapeSymbols).workActions
                i).1 with
          | none => (scanCfg w w.length ⋯ (Mode.string, n)).workTapes i
          | some s =>
            Function.update ((scanCfg w w.length ⋯ (Mode.string, n)).workTapes i)
              ((scanCfg w w.length ⋯ (Mode.string, n)).workTapePos i) s,
        workTapePos := fun i ↦
          (scanCfg w w.length ⋯ (Mode.string, n)).workTapePos i +
            ↑((unaryScanner.tr (modeState (Mode.string, n).1) none
                      (scanCfg w w.length ⋯ (Mode.string, n)).workTapeSymbols).workActions
                  i).2 }.workTapePos
    i =
  ↑(Mode.string, n).2bitw:List Booli:Fin 1n:ℕ⊢ { state := (unaryScanner.tr (modeState (Mode.bit, n).1) none (scanCfg w w.length ⋯ (Mode.bit, n)).workTapeSymbols).q',
        inputPos :=
          moveInputPos (scanCfg w w.length ⋯ (Mode.bit, n)).inputPos
            (unaryScanner.tr (modeState (Mode.bit, n).1) none
                (scanCfg w w.length ⋯ (Mode.bit, n)).workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
            ((unaryScanner.tr (modeState (Mode.bit, n).1) none
                    (scanCfg w w.length ⋯ (Mode.bit, n)).workTapeSymbols).workActions
                i).1 with
          | none => (scanCfg w w.length ⋯ (Mode.bit, n)).workTapes i
          | some s =>
            Function.update ((scanCfg w w.length ⋯ (Mode.bit, n)).workTapes i)
              ((scanCfg w w.length ⋯ (Mode.bit, n)).workTapePos i) s,
        workTapePos := fun i ↦
          (scanCfg w w.length ⋯ (Mode.bit, n)).workTapePos i +
            ↑((unaryScanner.tr (modeState (Mode.bit, n).1) none
                      (scanCfg w w.length ⋯ (Mode.bit, n)).workTapeSymbols).workActions
                  i).2 }.workTapePos
    i =
  ↑(Mode.bit, n).2donew:List Booli:Fin 1n:ℕ⊢ { state := (unaryScanner.tr (modeState (Mode.done, n).1) none (scanCfg w w.length ⋯ (Mode.done, n)).workTapeSymbols).q',
        inputPos :=
          moveInputPos (scanCfg w w.length ⋯ (Mode.done, n)).inputPos
            (unaryScanner.tr (modeState (Mode.done, n).1) none
                (scanCfg w w.length ⋯ (Mode.done, n)).workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
            ((unaryScanner.tr (modeState (Mode.done, n).1) none
                    (scanCfg w w.length ⋯ (Mode.done, n)).workTapeSymbols).workActions
                i).1 with
          | none => (scanCfg w w.length ⋯ (Mode.done, n)).workTapes i
          | some s =>
            Function.update ((scanCfg w w.length ⋯ (Mode.done, n)).workTapes i)
              ((scanCfg w w.length ⋯ (Mode.done, n)).workTapePos i) s,
        workTapePos := fun i ↦
          (scanCfg w w.length ⋯ (Mode.done, n)).workTapePos i +
            ↑((unaryScanner.tr (modeState (Mode.done, n).1) none
                      (scanCfg w w.length ⋯ (Mode.done, n)).workTapeSymbols).workActions
                  i).2 }.workTapePos
    i =
  ↑(Mode.done, n).2deadw:List Booli:Fin 1n:ℕ⊢ { state := (unaryScanner.tr (modeState (Mode.dead, n).1) none (scanCfg w w.length ⋯ (Mode.dead, n)).workTapeSymbols).q',
        inputPos :=
          moveInputPos (scanCfg w w.length ⋯ (Mode.dead, n)).inputPos
            (unaryScanner.tr (modeState (Mode.dead, n).1) none
                (scanCfg w w.length ⋯ (Mode.dead, n)).workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
            ((unaryScanner.tr (modeState (Mode.dead, n).1) none
                    (scanCfg w w.length ⋯ (Mode.dead, n)).workTapeSymbols).workActions
                i).1 with
          | none => (scanCfg w w.length ⋯ (Mode.dead, n)).workTapes i
          | some s =>
            Function.update ((scanCfg w w.length ⋯ (Mode.dead, n)).workTapes i)
              ((scanCfg w w.length ⋯ (Mode.dead, n)).workTapePos i) s,
        workTapePos := fun i ↦
          (scanCfg w w.length ⋯ (Mode.dead, n)).workTapePos i +
            ↑((unaryScanner.tr (modeState (Mode.dead, n).1) none
                      (scanCfg w w.length ⋯ (Mode.dead, n)).workTapeSymbols).workActions
                  i).2 }.workTapePos
    i =
  ↑(Mode.dead, n).2 simp [unaryScanner, modeState, scanCfg]All goals completed! 🐙

Every visited work-head position is between zero and the input length plus one.

theorem workTapePos_bounds (w : List Bool) (t : ℕ) (ht : t ≤ w.length + 3) (i : Fin 1) :
    0 ≤ (unaryScanner.configs (unaryScanner.initCfg (w.map boolEmb)) t).workTapePos i ∧
      (unaryScanner.configs (unaryScanner.initCfg (w.map boolEmb)) t).workTapePos i ≤
        (w.length + 1 : ℕ) := byw:List Boolt:ℕht:t ≤ w.length + 3i:Fin 1⊢ 0 ≤ (configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos i ∧
  (configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos i ≤ ↑(w.length + 1)
  rcases t with _ | tzerow:List Booli:Fin 1ht:0 ≤ w.length + 3⊢ 0 ≤ (configs (initCfg (List.map (⇑boolEmb) w)) 0).workTapePos i ∧
  (configs (initCfg (List.map (⇑boolEmb) w)) 0).workTapePos i ≤ ↑(w.length + 1)succw:List Booli:Fin 1t:ℕht:t + 1 ≤ w.length + 3⊢ 0 ≤ (configs (initCfg (List.map (⇑boolEmb) w)) (t + 1)).workTapePos i ∧
  (configs (initCfg (List.map (⇑boolEmb) w)) (t + 1)).workTapePos i ≤ ↑(w.length + 1)
  ·zerow:List Booli:Fin 1ht:0 ≤ w.length + 3⊢ 0 ≤ (configs (initCfg (List.map (⇑boolEmb) w)) 0).workTapePos i ∧
  (configs (initCfg (List.map (⇑boolEmb) w)) 0).workTapePos i ≤ ↑(w.length + 1) simpzerow:List Booli:Fin 1ht:0 ≤ w.length + 3⊢ 0 ≤ ↑w.length + 1
    omegaAll goals completed! 🐙
  rcases t with _ | tsucc.zerow:List Booli:Fin 1ht:0 + 1 ≤ w.length + 3⊢ 0 ≤ (configs (initCfg (List.map (⇑boolEmb) w)) (0 + 1)).workTapePos i ∧
  (configs (initCfg (List.map (⇑boolEmb) w)) (0 + 1)).workTapePos i ≤ ↑(w.length + 1)succ.succw:List Booli:Fin 1t:ℕht:t + 1 + 1 ≤ w.length + 3⊢ 0 ≤ (configs (initCfg (List.map (⇑boolEmb) w)) (t + 1 + 1)).workTapePos i ∧
  (configs (initCfg (List.map (⇑boolEmb) w)) (t + 1 + 1)).workTapePos i ≤ ↑(w.length + 1)
  ·succ.zerow:List Booli:Fin 1ht:0 + 1 ≤ w.length + 3⊢ 0 ≤ (configs (initCfg (List.map (⇑boolEmb) w)) (0 + 1)).workTapePos i ∧
  (configs (initCfg (List.map (⇑boolEmb) w)) (0 + 1)).workTapePos i ≤ ↑(w.length + 1) rw [show unaryScanner.configs (unaryScanner.initCfg (w.map boolEmb)) 1 =
        plantCfg w byw:List Boolt:ℕht:t ≤ w.length + 3i:Fin 1⊢ 0 ≤ (configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos i ∧
  (configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos i ≤ ↑(w.length + 1) exact init_step wAll goals completed! 🐙]succ.zerow:List Booli:Fin 1ht:0 + 1 ≤ w.length + 3⊢ 0 ≤ (plantCfg w).workTapePos i ∧ (plantCfg w).workTapePos i ≤ ↑(w.length + 1)
    simp [plantCfg]All goals completed! 🐙
  by_cases h : t ≤ w.lengthposw:List Booli:Fin 1t:ℕht:t + 1 + 1 ≤ w.length + 3h:t ≤ w.length⊢ 0 ≤ (configs (initCfg (List.map (⇑boolEmb) w)) (t + 1 + 1)).workTapePos i ∧
  (configs (initCfg (List.map (⇑boolEmb) w)) (t + 1 + 1)).workTapePos i ≤ ↑(w.length + 1)negw:List Booli:Fin 1t:ℕht:t + 1 + 1 ≤ w.length + 3h:¬t ≤ w.length⊢ 0 ≤ (configs (initCfg (List.map (⇑boolEmb) w)) (t + 1 + 1)).workTapePos i ∧
  (configs (initCfg (List.map (⇑boolEmb) w)) (t + 1 + 1)).workTapePos i ≤ ↑(w.length + 1)
  ·posw:List Booli:Fin 1t:ℕht:t + 1 + 1 ≤ w.length + 3h:t ≤ w.length⊢ 0 ≤ (configs (initCfg (List.map (⇑boolEmb) w)) (t + 1 + 1)).workTapePos i ∧
  (configs (initCfg (List.map (⇑boolEmb) w)) (t + 1 + 1)).workTapePos i ≤ ↑(w.length + 1) rw [(configs_scan w t h).1posw:List Booli:Fin 1t:ℕht:t + 1 + 1 ≤ w.length + 3h:t ≤ w.length⊢ 0 ≤ (scanCfg w t h (scan (List.take t w))).workTapePos i ∧
  (scanCfg w t h (scan (List.take t w))).workTapePos i ≤ ↑(w.length + 1)]posw:List Booli:Fin 1t:ℕht:t + 1 + 1 ≤ w.length + 3h:t ≤ w.length⊢ 0 ≤ (scanCfg w t h (scan (List.take t w))).workTapePos i ∧
  (scanCfg w t h (scan (List.take t w))).workTapePos i ≤ ↑(w.length + 1)
    change 0 ≤ ((scan (w.take t)).2 : ℤ) ∧ _posw:List Booli:Fin 1t:ℕht:t + 1 + 1 ≤ w.length + 3h:t ≤ w.length⊢ 0 ≤ ↑(scan (List.take t w)).2 ∧ (scanCfg w t h (scan (List.take t w))).workTapePos i ≤ ↑(w.length + 1)
    have hc := scan_counter_le (w.take t)posw:List Booli:Fin 1t:ℕht:t + 1 + 1 ≤ w.length + 3h:t ≤ w.lengthhc:(scan (List.take t w)).2 ≤ (List.take t w).length + 1⊢ 0 ≤ ↑(scan (List.take t w)).2 ∧ (scanCfg w t h (scan (List.take t w))).workTapePos i ≤ ↑(w.length + 1)
    simp only [List.length_take] at hcposw:List Booli:Fin 1t:ℕht:t + 1 + 1 ≤ w.length + 3h:t ≤ w.lengthhc:(scan (List.take t w)).2 ≤ min t w.length + 1⊢ 0 ≤ ↑(scan (List.take t w)).2 ∧ (scanCfg w t h (scan (List.take t w))).workTapePos i ≤ ↑(w.length + 1)
    constructorpos.leftw:List Booli:Fin 1t:ℕht:t + 1 + 1 ≤ w.length + 3h:t ≤ w.lengthhc:(scan (List.take t w)).2 ≤ min t w.length + 1⊢ 0 ≤ ↑(scan (List.take t w)).2pos.rightw:List Booli:Fin 1t:ℕht:t + 1 + 1 ≤ w.length + 3h:t ≤ w.lengthhc:(scan (List.take t w)).2 ≤ min t w.length + 1⊢ (scanCfg w t h (scan (List.take t w))).workTapePos i ≤ ↑(w.length + 1)
    ·pos.leftw:List Booli:Fin 1t:ℕht:t + 1 + 1 ≤ w.length + 3h:t ≤ w.lengthhc:(scan (List.take t w)).2 ≤ min t w.length + 1⊢ 0 ≤ ↑(scan (List.take t w)).2 exact Int.natCast_nonneg _All goals completed! 🐙
    ·pos.rightw:List Booli:Fin 1t:ℕht:t + 1 + 1 ≤ w.length + 3h:t ≤ w.lengthhc:(scan (List.take t w)).2 ≤ min t w.length + 1⊢ (scanCfg w t h (scan (List.take t w))).workTapePos i ≤ ↑(w.length + 1) simp only [scanCfg]pos.rightw:List Booli:Fin 1t:ℕht:t + 1 + 1 ≤ w.length + 3h:t ≤ w.lengthhc:(scan (List.take t w)).2 ≤ min t w.length + 1⊢ ↑(scan (List.take t w)).2 ≤ ↑(w.length + 1)
      omegaAll goals completed! 🐙
  ·negw:List Booli:Fin 1t:ℕht:t + 1 + 1 ≤ w.length + 3h:¬t ≤ w.length⊢ 0 ≤ (configs (initCfg (List.map (⇑boolEmb) w)) (t + 1 + 1)).workTapePos i ∧
  (configs (initCfg (List.map (⇑boolEmb) w)) (t + 1 + 1)).workTapePos i ≤ ↑(w.length + 1) have he : t = w.length + 1 := byw:List Boolt:ℕht:t ≤ w.length + 3i:Fin 1⊢ 0 ≤ (configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos i ∧
  (configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos i ≤ ↑(w.length + 1) omeganegw:List Booli:Fin 1t:ℕht:t + 1 + 1 ≤ w.length + 3h:¬t ≤ w.lengthhe:t = w.length + 1⊢ 0 ≤ (configs (initCfg (List.map (⇑boolEmb) w)) (t + 1 + 1)).workTapePos i ∧
  (configs (initCfg (List.map (⇑boolEmb) w)) (t + 1 + 1)).workTapePos i ≤ ↑(w.length + 1)
    subst tnegw:List Booli:Fin 1ht:w.length + 1 + 1 + 1 ≤ w.length + 3h:¬w.length + 1 ≤ w.length⊢ 0 ≤ (configs (initCfg (List.map (⇑boolEmb) w)) (w.length + 1 + 1 + 1)).workTapePos i ∧
  (configs (initCfg (List.map (⇑boolEmb) w)) (w.length + 1 + 1 + 1)).workTapePos i ≤ ↑(w.length + 1)
    rw [show w.length + 1 + 1 + 1 = (w.length + 2) + 1 byw:List Boolt:ℕht:t ≤ w.length + 3i:Fin 1⊢ 0 ≤ (configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos i ∧
  (configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos i ≤ ↑(w.length + 1) omegaAll goals completed! 🐙,
      configs_succ_eq_step',negw:List Booli:Fin 1ht:w.length + 1 + 1 + 1 ≤ w.length + 3h:¬w.length + 1 ≤ w.length⊢ 0 ≤ (MultiTapeTM.step (configs (initCfg (List.map (⇑boolEmb) w)) (w.length + 2))).workTapePos i ∧
  (MultiTapeTM.step (configs (initCfg (List.map (⇑boolEmb) w)) (w.length + 2))).workTapePos i ≤ ↑(w.length + 1) (configs_scan w w.length (byw:List Booli:Fin 1ht:w.length + 1 + 1 + 1 ≤ w.length + 3h:¬w.length + 1 ≤ w.length⊢ w.length ≤ w.length omegaAll goals completed! 🐙)).1, end_workTapePosnegw:List Booli:Fin 1ht:w.length + 1 + 1 + 1 ≤ w.length + 3h:¬w.length + 1 ≤ w.length⊢ 0 ≤ ↑(scan (List.take w.length w)).2 ∧ ↑(scan (List.take w.length w)).2 ≤ ↑(w.length + 1)]negw:List Booli:Fin 1ht:w.length + 1 + 1 + 1 ≤ w.length + 3h:¬w.length + 1 ≤ w.length⊢ 0 ≤ ↑(scan (List.take w.length w)).2 ∧ ↑(scan (List.take w.length w)).2 ≤ ↑(w.length + 1)
    have hc := scan_counter_le wnegw:List Booli:Fin 1ht:w.length + 1 + 1 + 1 ≤ w.length + 3h:¬w.length + 1 ≤ w.lengthhc:(scan w).2 ≤ w.length + 1⊢ 0 ≤ ↑(scan (List.take w.length w)).2 ∧ ↑(scan (List.take w.length w)).2 ≤ ↑(w.length + 1)
    simp only [List.take_length]negw:List Booli:Fin 1ht:w.length + 1 + 1 + 1 ≤ w.length + 3h:¬w.length + 1 ≤ w.lengthhc:(scan w).2 ≤ w.length + 1⊢ 0 ≤ ↑(scan w).2 ∧ ↑(scan w).2 ≤ ↑(w.length + 1)
    exact ⟨Int.natCast_nonneg _, byw:List Booli:Fin 1ht:w.length + 1 + 1 + 1 ≤ w.length + 3h:¬w.length + 1 ≤ w.lengthhc:(scan w).2 ≤ w.length + 1⊢ ↑(scan w).2 ≤ ↑(w.length + 1) exact_mod_cast hcAll goals completed! 🐙⟩

The unary machine visits at most the input length plus two work cells.

theorem spaceUsed_le (w : List Bool) :
    unaryScanner.spaceUsed (unaryScanner.initCfg (w.map boolEmb)) (w.length + 3) ≤
      w.length + 2 := byw:List Bool⊢ spaceUsed (initCfg (List.map (⇑boolEmb) w)) (w.length + 3) ≤ w.length + 2
  have hsub (i : Fin 1) :
      unaryScanner.visitedByTapeHead (unaryScanner.initCfg (w.map boolEmb))
          (w.length + 3) i ⊆ (Finset.range (w.length + 2)).image (fun n : ℕ ↦ (n : ℤ)) := by
    intro z hzw:List Booli:Fin 1z:ℤhz:z ∈ visitedByTapeHead (initCfg (List.map (⇑boolEmb) w)) (w.length + 3) i⊢ z ∈ Finset.image (fun n ↦ ↑n) (Finset.range (w.length + 2))
    obtain ⟨t, ht, rfl⟩ := unaryScanner.mem_visitedByTapeHead.mp hzw:List Booli:Fin 1t:ℕht:t < w.length + 3 + 1hz:(configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos i ∈
  visitedByTapeHead (initCfg (List.map (⇑boolEmb) w)) (w.length + 3) i⊢ (configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos i ∈ Finset.image (fun n ↦ ↑n) (Finset.range (w.length + 2))
    obtain ⟨hlo, hhi⟩ := workTapePos_bounds w t (byw:List Booli:Fin 1t:ℕht:t < w.length + 3 + 1hz:(configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos i ∈
  visitedByTapeHead (initCfg (List.map (⇑boolEmb) w)) (w.length + 3) i⊢ t ≤ w.length + 3 omegaAll goals completed! 🐙) iw:List Booli:Fin 1t:ℕht:t < w.length + 3 + 1hz:(configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos i ∈
  visitedByTapeHead (initCfg (List.map (⇑boolEmb) w)) (w.length + 3) ihlo:0 ≤ (configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos ihhi:(configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos i ≤ ↑(w.length + 1)⊢ (configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos i ∈ Finset.image (fun n ↦ ↑n) (Finset.range (w.length + 2))
    apply Finset.mem_image.mprw:List Booli:Fin 1t:ℕht:t < w.length + 3 + 1hz:(configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos i ∈
  visitedByTapeHead (initCfg (List.map (⇑boolEmb) w)) (w.length + 3) ihlo:0 ≤ (configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos ihhi:(configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos i ≤ ↑(w.length + 1)⊢ ∃ a ∈ Finset.range (w.length + 2), ↑a = (configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos i
    refine ⟨_, Finset.mem_range.mpr ?_, Int.toNat_of_nonneg hlo⟩w:List Booli:Fin 1t:ℕht:t < w.length + 3 + 1hz:(configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos i ∈
  visitedByTapeHead (initCfg (List.map (⇑boolEmb) w)) (w.length + 3) ihlo:0 ≤ (configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos ihhi:(configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos i ≤ ↑(w.length + 1)⊢ ((configs (initCfg (List.map (⇑boolEmb) w)) t).workTapePos i).toNat < w.length + 2
    omegaw:List Boolhsub:∀ (i : Fin 1),
  visitedByTapeHead (initCfg (List.map (⇑boolEmb) w)) (w.length + 3) i ⊆
    Finset.image (fun n ↦ ↑n) (Finset.range (w.length + 2))⊢ spaceUsed (initCfg (List.map (⇑boolEmb) w)) (w.length + 3) ≤ w.length + 2
  change ∑ i : Fin 1, _ ≤ _w:List Boolhsub:∀ (i : Fin 1),
  visitedByTapeHead (initCfg (List.map (⇑boolEmb) w)) (w.length + 3) i ⊆
    Finset.image (fun n ↦ ↑n) (Finset.range (w.length + 2))⊢ ∑ i, spaceUsedByTape (initCfg (List.map (⇑boolEmb) w)) (w.length + 3) i ≤ w.length + 2
  simp only [Finset.univ_unique, Finset.sum_singleton]w:List Boolhsub:∀ (i : Fin 1),
  visitedByTapeHead (initCfg (List.map (⇑boolEmb) w)) (w.length + 3) i ⊆
    Finset.image (fun n ↦ ↑n) (Finset.range (w.length + 2))⊢ spaceUsedByTape (initCfg (List.map (⇑boolEmb) w)) (w.length + 3) default ≤ w.length + 2
  exact (Finset.card_le_card (hsub 0)).trans
    (Finset.card_image_le.trans (byw:List Boolhsub:∀ (i : Fin 1),
  visitedByTapeHead (initCfg (List.map (⇑boolEmb) w)) (w.length + 3) i ⊆
    Finset.image (fun n ↦ ↑n) (Finset.range (w.length + 2))⊢ (Finset.range (w.length + 2)).card ≤ w.length + 2 simpAll goals completed! 🐙))

The unified recognizer runs in input length plus three steps and input length plus two cells.

theorem computableInTimeAndSpace_validBool :
    ComputableInTimeAndSpace (fun w : List Bool ↦ [validBool w])
      (fun n ↦ n + 3) (fun n ↦ n + 2) := by⊢ ComputableInTimeAndSpace (fun w ↦ [validBool w]) (fun n ↦ n + 3) fun n ↦ n + 2
  refine ⟨1, 2, 7, boolEmb, unaryScanner, fun w ↦ ?_⟩w:List Bool⊢ ∃ t' ≤ (fun n ↦ n + 3) w.length,
  ∃ s' ≤ (fun n ↦ n + 2) w.length,
    unaryScanner.ComputesInTimeAndSpace (List.map (⇑boolEmb) w) (List.map (⇑boolEmb) ((fun w ↦ [validBool w]) w)) t' s'
  exact ⟨w.length + 3, le_refl _,
    unaryScanner.spaceUsed (unaryScanner.initCfg (w.map boolEmb)) (w.length + 3),
    spaceUsed_le w, halts_at w, outputString_eq w, rfl⟩All goals completed! 🐙

end Geb.BitTree