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.Machine
public import Geb.Prototypes.Computability.TreeScanner.Steps

set_option doc.verso true

Simulation of the bitstring-tree scanner

Each input bit takes one machine transition after initialization. The simulation relates machine configurations to prefixes of the pure scan.

Main statements

configs_scan identifies every scanning configuration and its empty output.
halts_at and outputString_eq give termination and the decision bit.

Implementation notes

The correspondence uses CSLib's input-symbol and execution APIs, which depend on classical choice. The scanner's data and transition function are constructive.

Tags

Turing machine, simulation, binary tree, recognizer

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

The first initialization step positions the counter head at one.

theorem init_step (w : List Bool) :
    unaryScanner.step (unaryScanner.initCfg (w.map boolEmb)) = plantCfg w := byw:List Bool⊢ MultiTapeTM.step (initCfg (List.map (⇑boolEmb) w)) = plantCfg w
  rw [step_of_state _ _ 0 rflw:List Bool⊢ {
    state :=
      (unaryScanner.tr 0 (initCfg (List.map (⇑boolEmb) w)).inputSymbol
          (initCfg (List.map (⇑boolEmb) w)).workTapeSymbols).q',
    inputPos :=
      moveInputPos (initCfg (List.map (⇑boolEmb) w)).inputPos
        (unaryScanner.tr 0 (initCfg (List.map (⇑boolEmb) w)).inputSymbol
            (initCfg (List.map (⇑boolEmb) w)).workTapeSymbols).inputMove,
    workTapes := fun i ↦
      match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
        ((unaryScanner.tr 0 (initCfg (List.map (⇑boolEmb) w)).inputSymbol
                (initCfg (List.map (⇑boolEmb) w)).workTapeSymbols).workActions
            i).1 with
      | none => (initCfg (List.map (⇑boolEmb) w)).workTapes i
      | some s =>
        Function.update ((initCfg (List.map (⇑boolEmb) w)).workTapes i)
          ((initCfg (List.map (⇑boolEmb) w)).workTapePos i) s,
    workTapePos := fun i ↦
      (initCfg (List.map (⇑boolEmb) w)).workTapePos i +
        ↑((unaryScanner.tr 0 (initCfg (List.map (⇑boolEmb) w)).inputSymbol
                  (initCfg (List.map (⇑boolEmb) w)).workTapeSymbols).workActions
              i).2 } =
  plantCfg w]w:List Bool⊢ {
    state :=
      (unaryScanner.tr 0 (initCfg (List.map (⇑boolEmb) w)).inputSymbol
          (initCfg (List.map (⇑boolEmb) w)).workTapeSymbols).q',
    inputPos :=
      moveInputPos (initCfg (List.map (⇑boolEmb) w)).inputPos
        (unaryScanner.tr 0 (initCfg (List.map (⇑boolEmb) w)).inputSymbol
            (initCfg (List.map (⇑boolEmb) w)).workTapeSymbols).inputMove,
    workTapes := fun i ↦
      match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
        ((unaryScanner.tr 0 (initCfg (List.map (⇑boolEmb) w)).inputSymbol
                (initCfg (List.map (⇑boolEmb) w)).workTapeSymbols).workActions
            i).1 with
      | none => (initCfg (List.map (⇑boolEmb) w)).workTapes i
      | some s =>
        Function.update ((initCfg (List.map (⇑boolEmb) w)).workTapes i)
          ((initCfg (List.map (⇑boolEmb) w)).workTapePos i) s,
    workTapePos := fun i ↦
      (initCfg (List.map (⇑boolEmb) w)).workTapePos i +
        ↑((unaryScanner.tr 0 (initCfg (List.map (⇑boolEmb) w)).inputSymbol
                  (initCfg (List.map (⇑boolEmb) w)).workTapeSymbols).workActions
              i).2 } =
  plantCfg w
  rflAll goals completed! 🐙

The second initialization step installs the completion marker.

theorem plant_step (w : List Bool) :
    unaryScanner.step (plantCfg w) = scanCfg w 0 (byw:List Bool⊢ 0 ≤ w.length omegaAll goals completed! 🐙) (.tree, 1) := byw:List Bool⊢ MultiTapeTM.step (plantCfg w) = scanCfg w 0 ⋯ (Mode.tree, 1)
  rw [step_of_state _ _ 1 rflw:List Bool⊢ { state := (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).q',
    inputPos :=
      moveInputPos (plantCfg w).inputPos
        (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).inputMove,
    workTapes := fun i ↦
      match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
        ((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).1 with
      | none => (plantCfg w).workTapes i
      | some s => Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) s,
    workTapePos := fun i ↦
      (plantCfg w).workTapePos i +
        ↑((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).2 } =
  scanCfg w 0 ⋯ (Mode.tree, 1)]w:List Bool⊢ { state := (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).q',
    inputPos :=
      moveInputPos (plantCfg w).inputPos
        (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).inputMove,
    workTapes := fun i ↦
      match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
        ((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).1 with
      | none => (plantCfg w).workTapes i
      | some s => Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) s,
    workTapePos := fun i ↦
      (plantCfg w).workTapePos i +
        ↑((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).2 } =
  scanCfg w 0 ⋯ (Mode.tree, 1)
  apply Cfg.extstatew:List Bool⊢ { state := (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).q',
      inputPos :=
        moveInputPos (plantCfg w).inputPos
          (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
          ((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).1 with
        | none => (plantCfg w).workTapes i
        | some s => Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) s,
      workTapePos := fun i ↦
        (plantCfg w).workTapePos i +
          ↑((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).2 }.state =
  (scanCfg w 0 ⋯ (Mode.tree, 1)).stateinputPosw:List Bool⊢ { state := (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).q',
      inputPos :=
        moveInputPos (plantCfg w).inputPos
          (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
          ((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).1 with
        | none => (plantCfg w).workTapes i
        | some s => Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) s,
      workTapePos := fun i ↦
        (plantCfg w).workTapePos i +
          ↑((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).2 }.inputPos =
  (scanCfg w 0 ⋯ (Mode.tree, 1)).inputPosworkTapesw:List Bool⊢ { state := (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).q',
      inputPos :=
        moveInputPos (plantCfg w).inputPos
          (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
          ((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).1 with
        | none => (plantCfg w).workTapes i
        | some s => Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) s,
      workTapePos := fun i ↦
        (plantCfg w).workTapePos i +
          ↑((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).2 }.workTapes =
  (scanCfg w 0 ⋯ (Mode.tree, 1)).workTapesworkTapePosw:List Bool⊢ { state := (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).q',
      inputPos :=
        moveInputPos (plantCfg w).inputPos
          (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
          ((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).1 with
        | none => (plantCfg w).workTapes i
        | some s => Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) s,
      workTapePos := fun i ↦
        (plantCfg w).workTapePos i +
          ↑((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).2 }.workTapePos =
  (scanCfg w 0 ⋯ (Mode.tree, 1)).workTapePos
  ·statew:List Bool⊢ { state := (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).q',
      inputPos :=
        moveInputPos (plantCfg w).inputPos
          (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
          ((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).1 with
        | none => (plantCfg w).workTapes i
        | some s => Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) s,
      workTapePos := fun i ↦
        (plantCfg w).workTapePos i +
          ↑((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).2 }.state =
  (scanCfg w 0 ⋯ (Mode.tree, 1)).state rflAll goals completed! 🐙
  ·inputPosw:List Bool⊢ { state := (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).q',
      inputPos :=
        moveInputPos (plantCfg w).inputPos
          (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
          ((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).1 with
        | none => (plantCfg w).workTapes i
        | some s => Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) s,
      workTapePos := fun i ↦
        (plantCfg w).workTapePos i +
          ↑((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).2 }.inputPos =
  (scanCfg w 0 ⋯ (Mode.tree, 1)).inputPos rflAll goals completed! 🐙
  ·workTapesw:List Bool⊢ { state := (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).q',
      inputPos :=
        moveInputPos (plantCfg w).inputPos
          (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
          ((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).1 with
        | none => (plantCfg w).workTapes i
        | some s => Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) s,
      workTapePos := fun i ↦
        (plantCfg w).workTapePos i +
          ↑((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).2 }.workTapes =
  (scanCfg w 0 ⋯ (Mode.tree, 1)).workTapes funext i zworkTapesw:List Booli:Fin 1z:ℤ⊢ { state := (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).q',
        inputPos :=
          moveInputPos (plantCfg w).inputPos
            (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
            ((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).1 with
          | none => (plantCfg w).workTapes i
          | some s => Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) s,
        workTapePos := fun i ↦
          (plantCfg w).workTapePos i +
            ↑((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).2 }.workTapes
    i z =
  (scanCfg w 0 ⋯ (Mode.tree, 1)).workTapes i z
    simp [unaryScanner, plantCfg, scanCfg, Function.update_apply]All goals completed! 🐙
  ·workTapePosw:List Bool⊢ { state := (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).q',
      inputPos :=
        moveInputPos (plantCfg w).inputPos
          (unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
          ((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).1 with
        | none => (plantCfg w).workTapes i
        | some s => Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) s,
      workTapePos := fun i ↦
        (plantCfg w).workTapePos i +
          ↑((unaryScanner.tr 1 (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).workActions i).2 }.workTapePos =
  (scanCfg w 0 ⋯ (Mode.tree, 1)).workTapePos rflAll goals completed! 🐙

The scanned prefix determines the next input symbol.

theorem scanCfg_inputSymbol (w : List Bool) (t : ℕ) (h : t < w.length) (s : State) :
    (scanCfg w t (byw:List Boolt:ℕh:t < w.lengths:State⊢ t ≤ w.length omegaAll goals completed! 🐙) s).inputSymbol = some (boolEmb w[t]) := byw:List Boolt:ℕh:t < w.lengths:State⊢ (scanCfg w t ⋯ s).inputSymbol = some (boolEmb w[t])
  rw [inputSymbolInner t (byw:List Boolt:ℕh:t < w.lengths:State⊢ ↑(scanCfg w t ⋯ s).inputPos = 1 + t simp [scanCfg, Nat.add_comm]All goals completed! 🐙)
    (byw:List Boolt:ℕh:t < w.lengths:State⊢ t < (List.map (⇑boolEmb) w).length simpa only [List.length_map] using hAll goals completed! 🐙), List.getElem_mapw:List Boolt:ℕh:t < w.lengths:State⊢ some (boolEmb w[t]) = some (boolEmb w[t])]All goals completed! 🐙

A complete scan reads the right end marker.

theorem scanCfg_inputSymbol_end (w : List Bool) (s : State) :
    (scanCfg w w.length (byw:List Bools:State⊢ w.length ≤ w.length omegaAll goals completed! 🐙) s).inputSymbol = none := byw:List Bools:State⊢ (scanCfg w w.length ⋯ s).inputSymbol = none
  unfold Cfg.inputSymbolw:List Bools:State⊢ (if h₁ : (scanCfg w w.length ⋯ s).inputPos = 0 then none
  else
    if h₂ : ↑(scanCfg w w.length ⋯ s).inputPos = (List.map (⇑boolEmb) w).length + 1 then none
    else some (List.map (⇑boolEmb) w)[↑(scanCfg w w.length ⋯ s).inputPos - 1]) =
  none
  split_ifsposw:List Bools:Stateh✝:(scanCfg w w.length ⋯ s).inputPos = 0⊢ none = noneposw:List Bools:Stateh✝¹:¬(scanCfg w w.length ⋯ s).inputPos = 0h✝:↑(scanCfg w w.length ⋯ s).inputPos = (List.map (⇑boolEmb) w).length + 1⊢ none = nonenegw:List Bools:Stateh✝¹:¬(scanCfg w w.length ⋯ s).inputPos = 0h✝:¬↑(scanCfg w w.length ⋯ s).inputPos = (List.map (⇑boolEmb) w).length + 1⊢ False <;>posw:List Bools:Stateh✝:(scanCfg w w.length ⋯ s).inputPos = 0⊢ none = noneposw:List Bools:Stateh✝¹:¬(scanCfg w w.length ⋯ s).inputPos = 0h✝:↑(scanCfg w w.length ⋯ s).inputPos = (List.map (⇑boolEmb) w).length + 1⊢ none = nonenegw:List Bools:Stateh✝¹:¬(scanCfg w w.length ⋯ s).inputPos = 0h✝:¬↑(scanCfg w w.length ⋯ s).inputPos = (List.map (⇑boolEmb) w).length + 1⊢ False simp_all [scanCfg]All goals completed! 🐙

A scanning transition consumes one bit and updates exactly the pure state.

theorem scanCfg_step (w : List Bool) (t : ℕ) (h : t < w.length) (s : State)
    (hs : s.1 = .string → 0 < s.2) :
    unaryScanner.step (scanCfg w t (byw:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2⊢ t ≤ w.length omegaAll goals completed! 🐙) s) =
      scanCfg w (t + 1) h (step s w[t]) := byw:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2⊢ MultiTapeTM.step (scanCfg w t ⋯ s) = scanCfg w (t + 1) h (step s w[t])
  have hw : (scanCfg w t (byw:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2⊢ t ≤ w.length omegaAll goals completed! 🐙) s).workTapeSymbols =
      fun _ ↦ if s.2 = 1 then some 0 else none := by
    funext iw:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2i:Fin 1⊢ (scanCfg w t ⋯ s).workTapeSymbols i = if s.2 = 1 then some 0 else none
    simp [Cfg.workTapeSymbols, scanCfg]w:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2hw:(scanCfg w t ⋯ s).workTapeSymbols = fun x ↦ if s.2 = 1 then some 0 else none⊢ MultiTapeTM.step (scanCfg w t ⋯ s) = scanCfg w (t + 1) h (step s w[t])
  rw [step_of_state _ _ (modeState s.1) rfl,w:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2hw:(scanCfg w t ⋯ s).workTapeSymbols = fun x ↦ if s.2 = 1 then some 0 else none⊢ { state := (unaryScanner.tr (modeState s.1) (scanCfg w t ⋯ s).inputSymbol (scanCfg w t ⋯ s).workTapeSymbols).q',
    inputPos :=
      moveInputPos (scanCfg w t ⋯ s).inputPos
        (unaryScanner.tr (modeState s.1) (scanCfg w t ⋯ s).inputSymbol (scanCfg w t ⋯ s).workTapeSymbols).inputMove,
    workTapes := fun i ↦
      match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
        ((unaryScanner.tr (modeState s.1) (scanCfg w t ⋯ s).inputSymbol (scanCfg w t ⋯ s).workTapeSymbols).workActions
            i).1 with
      | none => (scanCfg w t ⋯ s).workTapes i
      | some s_1 => Function.update ((scanCfg w t ⋯ s).workTapes i) ((scanCfg w t ⋯ s).workTapePos i) s_1,
    workTapePos := fun i ↦
      (scanCfg w t ⋯ s).workTapePos i +
        ↑((unaryScanner.tr (modeState s.1) (scanCfg w t ⋯ s).inputSymbol (scanCfg w t ⋯ s).workTapeSymbols).workActions
              i).2 } =
  scanCfg w (t + 1) h (step s w[t]) scanCfg_inputSymbol w t h,w:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2hw:(scanCfg w t ⋯ s).workTapeSymbols = fun x ↦ if s.2 = 1 then some 0 else none⊢ { state := (unaryScanner.tr (modeState s.1) (some (boolEmb w[t])) (scanCfg w t ⋯ s).workTapeSymbols).q',
    inputPos :=
      moveInputPos (scanCfg w t ⋯ s).inputPos
        (unaryScanner.tr (modeState s.1) (some (boolEmb w[t])) (scanCfg w t ⋯ s).workTapeSymbols).inputMove,
    workTapes := fun i ↦
      match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
        ((unaryScanner.tr (modeState s.1) (some (boolEmb w[t])) (scanCfg w t ⋯ s).workTapeSymbols).workActions i).1 with
      | none => (scanCfg w t ⋯ s).workTapes i
      | some s_1 => Function.update ((scanCfg w t ⋯ s).workTapes i) ((scanCfg w t ⋯ s).workTapePos i) s_1,
    workTapePos := fun i ↦
      (scanCfg w t ⋯ s).workTapePos i +
        ↑((unaryScanner.tr (modeState s.1) (some (boolEmb w[t])) (scanCfg w t ⋯ s).workTapeSymbols).workActions i).2 } =
  scanCfg w (t + 1) h (step s w[t])
    hw,w:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2hw:(scanCfg w t ⋯ s).workTapeSymbols = fun x ↦ if s.2 = 1 then some 0 else none⊢ { state := (unaryScanner.tr (modeState s.1) (some (boolEmb w[t])) fun x ↦ if s.2 = 1 then some 0 else none).q',
    inputPos :=
      moveInputPos (scanCfg w t ⋯ s).inputPos
        (unaryScanner.tr (modeState s.1) (some (boolEmb w[t])) fun x ↦ if s.2 = 1 then some 0 else none).inputMove,
    workTapes := fun i ↦
      match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
        ((unaryScanner.tr (modeState s.1) (some (boolEmb w[t])) fun x ↦ if s.2 = 1 then some 0 else none).workActions
            i).1 with
      | none => (scanCfg w t ⋯ s).workTapes i
      | some s_1 => Function.update ((scanCfg w t ⋯ s).workTapes i) ((scanCfg w t ⋯ s).workTapePos i) s_1,
    workTapePos := fun i ↦
      (scanCfg w t ⋯ s).workTapePos i +
        ↑((unaryScanner.tr (modeState s.1) (some (boolEmb w[t])) fun x ↦ if s.2 = 1 then some 0 else none).workActions
              i).2 } =
  scanCfg w (t + 1) h (step s w[t]) tr_scanw:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2hw:(scanCfg w t ⋯ s).workTapeSymbols = fun x ↦ if s.2 = 1 then some 0 else none⊢ { state := (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).q',
    inputPos :=
      moveInputPos (scanCfg w t ⋯ s).inputPos
        (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).inputMove,
    workTapes := fun i ↦
      match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
        ((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).1 with
      | none => (scanCfg w t ⋯ s).workTapes i
      | some s_1 => Function.update ((scanCfg w t ⋯ s).workTapes i) ((scanCfg w t ⋯ s).workTapePos i) s_1,
    workTapePos := fun i ↦
      (scanCfg w t ⋯ s).workTapePos i +
        ↑((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).2 } =
  scanCfg w (t + 1) h (step s w[t])]w:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2hw:(scanCfg w t ⋯ s).workTapeSymbols = fun x ↦ if s.2 = 1 then some 0 else none⊢ { state := (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).q',
    inputPos :=
      moveInputPos (scanCfg w t ⋯ s).inputPos
        (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).inputMove,
    workTapes := fun i ↦
      match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
        ((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).1 with
      | none => (scanCfg w t ⋯ s).workTapes i
      | some s_1 => Function.update ((scanCfg w t ⋯ s).workTapes i) ((scanCfg w t ⋯ s).workTapePos i) s_1,
    workTapePos := fun i ↦
      (scanCfg w t ⋯ s).workTapePos i +
        ↑((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).2 } =
  scanCfg w (t + 1) h (step s w[t])
  apply Cfg.extstatew:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2hw:(scanCfg w t ⋯ s).workTapeSymbols = fun x ↦ if s.2 = 1 then some 0 else none⊢ { state := (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).q',
      inputPos :=
        moveInputPos (scanCfg w t ⋯ s).inputPos
          (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
          ((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).1 with
        | none => (scanCfg w t ⋯ s).workTapes i
        | some s_1 => Function.update ((scanCfg w t ⋯ s).workTapes i) ((scanCfg w t ⋯ s).workTapePos i) s_1,
      workTapePos := fun i ↦
        (scanCfg w t ⋯ s).workTapePos i +
          ↑((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).2 }.state =
  (scanCfg w (t + 1) h (step s w[t])).stateinputPosw:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2hw:(scanCfg w t ⋯ s).workTapeSymbols = fun x ↦ if s.2 = 1 then some 0 else none⊢ { state := (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).q',
      inputPos :=
        moveInputPos (scanCfg w t ⋯ s).inputPos
          (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
          ((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).1 with
        | none => (scanCfg w t ⋯ s).workTapes i
        | some s_1 => Function.update ((scanCfg w t ⋯ s).workTapes i) ((scanCfg w t ⋯ s).workTapePos i) s_1,
      workTapePos := fun i ↦
        (scanCfg w t ⋯ s).workTapePos i +
          ↑((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).2 }.inputPos =
  (scanCfg w (t + 1) h (step s w[t])).inputPosworkTapesw:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2hw:(scanCfg w t ⋯ s).workTapeSymbols = fun x ↦ if s.2 = 1 then some 0 else none⊢ { state := (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).q',
      inputPos :=
        moveInputPos (scanCfg w t ⋯ s).inputPos
          (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
          ((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).1 with
        | none => (scanCfg w t ⋯ s).workTapes i
        | some s_1 => Function.update ((scanCfg w t ⋯ s).workTapes i) ((scanCfg w t ⋯ s).workTapePos i) s_1,
      workTapePos := fun i ↦
        (scanCfg w t ⋯ s).workTapePos i +
          ↑((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).2 }.workTapes =
  (scanCfg w (t + 1) h (step s w[t])).workTapesworkTapePosw:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2hw:(scanCfg w t ⋯ s).workTapeSymbols = fun x ↦ if s.2 = 1 then some 0 else none⊢ { state := (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).q',
      inputPos :=
        moveInputPos (scanCfg w t ⋯ s).inputPos
          (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
          ((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).1 with
        | none => (scanCfg w t ⋯ s).workTapes i
        | some s_1 => Function.update ((scanCfg w t ⋯ s).workTapes i) ((scanCfg w t ⋯ s).workTapePos i) s_1,
      workTapePos := fun i ↦
        (scanCfg w t ⋯ s).workTapePos i +
          ↑((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).2 }.workTapePos =
  (scanCfg w (t + 1) h (step s w[t])).workTapePos
  ·statew:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2hw:(scanCfg w t ⋯ s).workTapeSymbols = fun x ↦ if s.2 = 1 then some 0 else none⊢ { state := (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).q',
      inputPos :=
        moveInputPos (scanCfg w t ⋯ s).inputPos
          (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
          ((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).1 with
        | none => (scanCfg w t ⋯ s).workTapes i
        | some s_1 => Function.update ((scanCfg w t ⋯ s).workTapes i) ((scanCfg w t ⋯ s).workTapePos i) s_1,
      workTapePos := fun i ↦
        (scanCfg w t ⋯ s).workTapePos i +
          ↑((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).2 }.state =
  (scanCfg w (t + 1) h (step s w[t])).state rflAll goals completed! 🐙
  ·inputPosw:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2hw:(scanCfg w t ⋯ s).workTapeSymbols = fun x ↦ if s.2 = 1 then some 0 else none⊢ { state := (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).q',
      inputPos :=
        moveInputPos (scanCfg w t ⋯ s).inputPos
          (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
          ((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).1 with
        | none => (scanCfg w t ⋯ s).workTapes i
        | some s_1 => Function.update ((scanCfg w t ⋯ s).workTapes i) ((scanCfg w t ⋯ s).workTapePos i) s_1,
      workTapePos := fun i ↦
        (scanCfg w t ⋯ s).workTapePos i +
          ↑((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).2 }.inputPos =
  (scanCfg w (t + 1) h (step s w[t])).inputPos change moveInputPos _ SignType.pos = _inputPosw:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2hw:(scanCfg w t ⋯ s).workTapeSymbols = fun x ↦ if s.2 = 1 then some 0 else none⊢ moveInputPos (scanCfg w t ⋯ s).inputPos SignType.pos = (scanCfg w (t + 1) h (step s w[t])).inputPos
    rw [moveInputPos_pos_of_ne_right (scanCfg w t (byw:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2hw:(scanCfg w t ⋯ s).workTapeSymbols = fun x ↦ if s.2 = 1 then some 0 else none⊢ t ≤ w.length omegaAll goals completed! 🐙) s).inputPos
      (byw:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2hw:(scanCfg w t ⋯ s).workTapeSymbols = fun x ↦ if s.2 = 1 then some 0 else none⊢ ↑(scanCfg w t ⋯ s).inputPos ≠ (List.map (⇑boolEmb) w).length + 1 simp [scanCfg]w:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2hw:(scanCfg w t ⋯ s).workTapeSymbols = fun x ↦ if s.2 = 1 then some 0 else none⊢ ¬t = w.length; omegaAll goals completed! 🐙)]inputPosw:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2hw:(scanCfg w t ⋯ s).workTapeSymbols = fun x ↦ if s.2 = 1 then some 0 else none⊢ ⟨↑(scanCfg w t ⋯ s).inputPos + 1, ⋯⟩ = (scanCfg w (t + 1) h (step s w[t])).inputPos
    rflAll goals completed! 🐙
  ·workTapesw:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2hw:(scanCfg w t ⋯ s).workTapeSymbols = fun x ↦ if s.2 = 1 then some 0 else none⊢ { state := (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).q',
      inputPos :=
        moveInputPos (scanCfg w t ⋯ s).inputPos
          (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
          ((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).1 with
        | none => (scanCfg w t ⋯ s).workTapes i
        | some s_1 => Function.update ((scanCfg w t ⋯ s).workTapes i) ((scanCfg w t ⋯ s).workTapePos i) s_1,
      workTapePos := fun i ↦
        (scanCfg w t ⋯ s).workTapePos i +
          ↑((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).2 }.workTapes =
  (scanCfg w (t + 1) h (step s w[t])).workTapes rflAll goals completed! 🐙
  ·workTapePosw:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2hw:(scanCfg w t ⋯ s).workTapeSymbols = fun x ↦ if s.2 = 1 then some 0 else none⊢ { state := (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).q',
      inputPos :=
        moveInputPos (scanCfg w t ⋯ s).inputPos
          (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
          ((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).1 with
        | none => (scanCfg w t ⋯ s).workTapes i
        | some s_1 => Function.update ((scanCfg w t ⋯ s).workTapes i) ((scanCfg w t ⋯ s).workTapePos i) s_1,
      workTapePos := fun i ↦
        (scanCfg w t ⋯ s).workTapePos i +
          ↑((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).2 }.workTapePos =
  (scanCfg w (t + 1) h (step s w[t])).workTapePos funext iworkTapePosw:List Boolt:ℕh:t < w.lengths:Statehs:s.1 = Mode.string → 0 < s.2hw:(scanCfg w t ⋯ s).workTapeSymbols = fun x ↦ if s.2 = 1 then some 0 else nonei:Fin 1⊢ { state := (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).q',
        inputPos :=
          moveInputPos (scanCfg w t ⋯ s).inputPos
            (consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 2)) → ℤ → Option (Fin 2))
            ((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).1 with
          | none => (scanCfg w t ⋯ s).workTapes i
          | some s_1 => Function.update ((scanCfg w t ⋯ s).workTapes i) ((scanCfg w t ⋯ s).workTapePos i) s_1,
        workTapePos := fun i ↦
          (scanCfg w t ⋯ s).workTapePos i +
            ↑((consume (modeState (step (s.1, s.2) w[t]).1) (counterMove s.1 w[t])).workActions i).2 }.workTapePos
    i =
  (scanCfg w (t + 1) h (step s w[t])).workTapePos i
    exact counterMove_add s.1 s.2 w[t] hsAll goals completed! 🐙

Scanning a bit emits no output.

theorem outputSymbol_scanCfg (w : List Bool) (t : ℕ) (h : t < w.length) (s : State) :
    unaryScanner.outputSymbol (scanCfg w t (byw:List Boolt:ℕh:t < w.lengths:State⊢ t ≤ w.length omegaAll goals completed! 🐙) s) = none := byw:List Boolt:ℕh:t < w.lengths:State⊢ outputSymbol (scanCfg w t ⋯ s) = none
  unfold outputSymbolw:List Boolt:ℕh:t < w.lengths:State⊢ (match (scanCfg w t ⋯ s).state with
  | none => none
  | some q => (unaryScanner.tr q (scanCfg w t ⋯ s).inputSymbol (scanCfg w t ⋯ s).workTapeSymbols).outS) =
  none
  change (unaryScanner.tr (modeState s.1) _ _).outS = nonew:List Boolt:ℕh:t < w.lengths:State⊢ (unaryScanner.tr (modeState s.1) (scanCfg w t ⋯ s).inputSymbol (scanCfg w t ⋯ s).workTapeSymbols).outS = none
  rw [scanCfg_inputSymbol w t hw:List Boolt:ℕh:t < w.lengths:State⊢ (unaryScanner.tr (modeState s.1) (some (boolEmb w[t])) (scanCfg w t ⋯ s).workTapeSymbols).outS = none]w:List Boolt:ℕh:t < w.lengths:State⊢ (unaryScanner.tr (modeState s.1) (some (boolEmb w[t])) (scanCfg w t ⋯ s).workTapeSymbols).outS = none
  rcases s with ⟨m, n⟩w:List Boolt:ℕh:t < w.lengthm:Moden:ℕ⊢ (unaryScanner.tr (modeState (m, n).1) (some (boolEmb w[t])) (scanCfg w t ⋯ (m, n)).workTapeSymbols).outS = none
  cases mtreew:List Boolt:ℕh:t < w.lengthn:ℕ⊢ (unaryScanner.tr (modeState (Mode.tree, n).1) (some (boolEmb w[t]))
      (scanCfg w t ⋯ (Mode.tree, n)).workTapeSymbols).outS =
  nonestringw:List Boolt:ℕh:t < w.lengthn:ℕ⊢ (unaryScanner.tr (modeState (Mode.string, n).1) (some (boolEmb w[t]))
      (scanCfg w t ⋯ (Mode.string, n)).workTapeSymbols).outS =
  nonebitw:List Boolt:ℕh:t < w.lengthn:ℕ⊢ (unaryScanner.tr (modeState (Mode.bit, n).1) (some (boolEmb w[t])) (scanCfg w t ⋯ (Mode.bit, n)).workTapeSymbols).outS =
  nonedonew:List Boolt:ℕh:t < w.lengthn:ℕ⊢ (unaryScanner.tr (modeState (Mode.done, n).1) (some (boolEmb w[t]))
      (scanCfg w t ⋯ (Mode.done, n)).workTapeSymbols).outS =
  nonedeadw:List Boolt:ℕh:t < w.lengthn:ℕ⊢ (unaryScanner.tr (modeState (Mode.dead, n).1) (some (boolEmb w[t]))
      (scanCfg w t ⋯ (Mode.dead, n)).workTapeSymbols).outS =
  none <;>treew:List Boolt:ℕh:t < w.lengthn:ℕ⊢ (unaryScanner.tr (modeState (Mode.tree, n).1) (some (boolEmb w[t]))
      (scanCfg w t ⋯ (Mode.tree, n)).workTapeSymbols).outS =
  nonestringw:List Boolt:ℕh:t < w.lengthn:ℕ⊢ (unaryScanner.tr (modeState (Mode.string, n).1) (some (boolEmb w[t]))
      (scanCfg w t ⋯ (Mode.string, n)).workTapeSymbols).outS =
  nonebitw:List Boolt:ℕh:t < w.lengthn:ℕ⊢ (unaryScanner.tr (modeState (Mode.bit, n).1) (some (boolEmb w[t])) (scanCfg w t ⋯ (Mode.bit, n)).workTapeSymbols).outS =
  nonedonew:List Boolt:ℕh:t < w.lengthn:ℕ⊢ (unaryScanner.tr (modeState (Mode.done, n).1) (some (boolEmb w[t]))
      (scanCfg w t ⋯ (Mode.done, n)).workTapeSymbols).outS =
  nonedeadw:List Boolt:ℕh:t < w.lengthn:ℕ⊢ (unaryScanner.tr (modeState (Mode.dead, n).1) (some (boolEmb w[t]))
      (scanCfg w t ⋯ (Mode.dead, n)).workTapeSymbols).outS =
  none simp [unaryScanner, modeState, consume]All goals completed! 🐙 <;>treew:List Boolt:ℕh:t < w.lengthn:ℕ⊢ (if boolEmb w[t] = 0 then { inputMove := 1, workActions := fun x ↦ (none, 0), outS := none, q' := some 3 }
    else { inputMove := 1, workActions := fun x ↦ (none, 1), outS := none, q' := some 2 }).outS =
  nonestringw:List Boolt:ℕh:t < w.lengthn:ℕ⊢ (if boolEmb w[t] = 0 then
      { inputMove := 1, workActions := fun x ↦ (none, -1), outS := none,
        q' := some (if (scanCfg w t ⋯ (Mode.string, n)).workTapeSymbols 0 = some 0 then 5 else 2) }
    else { inputMove := 1, workActions := fun x ↦ (none, 0), outS := none, q' := some 4 }).outS =
  none split_ifsposw:List Boolt:ℕh:t < w.lengthn:ℕh✝¹:boolEmb w[t] = 0h✝:(scanCfg w t ⋯ (Mode.string, n)).workTapeSymbols 0 = some 0⊢ { inputMove := 1, workActions := fun x ↦ (none, -1), outS := none, q' := some 5 }.outS = nonenegw:List Boolt:ℕh:t < w.lengthn:ℕh✝¹:boolEmb w[t] = 0h✝:¬(scanCfg w t ⋯ (Mode.string, n)).workTapeSymbols 0 = some 0⊢ { inputMove := 1, workActions := fun x ↦ (none, -1), outS := none, q' := some 2 }.outS = nonenegw:List Boolt:ℕh:t < w.lengthn:ℕh✝:¬boolEmb w[t] = 0⊢ { inputMove := 1, workActions := fun x ↦ (none, 0), outS := none, q' := some 4 }.outS = none <;>posw:List Boolt:ℕh:t < w.lengthn:ℕh✝:boolEmb w[t] = 0⊢ { inputMove := 1, workActions := fun x ↦ (none, 0), outS := none, q' := some 3 }.outS = nonenegw:List Boolt:ℕh:t < w.lengthn:ℕh✝:¬boolEmb w[t] = 0⊢ { inputMove := 1, workActions := fun x ↦ (none, 1), outS := none, q' := some 2 }.outS = noneposw:List Boolt:ℕh:t < w.lengthn:ℕh✝¹:boolEmb w[t] = 0h✝:(scanCfg w t ⋯ (Mode.string, n)).workTapeSymbols 0 = some 0⊢ { inputMove := 1, workActions := fun x ↦ (none, -1), outS := none, q' := some 5 }.outS = nonenegw:List Boolt:ℕh:t < w.lengthn:ℕh✝¹:boolEmb w[t] = 0h✝:¬(scanCfg w t ⋯ (Mode.string, n)).workTapeSymbols 0 = some 0⊢ { inputMove := 1, workActions := fun x ↦ (none, -1), outS := none, q' := some 2 }.outS = nonenegw:List Boolt:ℕh:t < w.lengthn:ℕh✝:¬boolEmb w[t] = 0⊢ { inputMove := 1, workActions := fun x ↦ (none, 0), outS := none, q' := some 4 }.outS = none rflAll goals completed! 🐙

At the right end marker the machine halts.

theorem scanCfg_halts (w : List Bool) (s : State) :
    (unaryScanner.step (scanCfg w w.length (byw:List Bools:State⊢ w.length ≤ w.length omegaAll goals completed! 🐙) s)).state = none := byw:List Bools:State⊢ (MultiTapeTM.step (scanCfg w w.length ⋯ s)).state = none
  rw [step_of_state _ _ (modeState s.1) rfl,w:List Bools:State⊢ {
      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 }.state =
  none scanCfg_inputSymbol_endw:List Bools:State⊢ { 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 }.state =
  none]w:List Bools:State⊢ { 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 }.state =
  none
  rcases s with ⟨m, n⟩w:List Boolm: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 }.state =
  none
  cases mtreew:List Booln:ℕ⊢ { 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 }.state =
  nonestringw:List Booln:ℕ⊢ {
      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 }.state =
  nonebitw:List Booln:ℕ⊢ { 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 }.state =
  nonedonew:List Booln:ℕ⊢ { 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 }.state =
  nonedeadw:List Booln:ℕ⊢ { 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 }.state =
  none <;>treew:List Booln:ℕ⊢ { 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 }.state =
  nonestringw:List Booln:ℕ⊢ {
      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 }.state =
  nonebitw:List Booln:ℕ⊢ { 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 }.state =
  nonedonew:List Booln:ℕ⊢ { 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 }.state =
  nonedeadw:List Booln:ℕ⊢ { 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 }.state =
  none rflAll goals completed! 🐙

The right end marker emits the decision of the pure scanner state.

theorem outputSymbol_scanCfg_end (w : List Bool) (s : State) :
    unaryScanner.outputSymbol (scanCfg w w.length (byw:List Bools:State⊢ w.length ≤ w.length omegaAll goals completed! 🐙) s) =
      some (boolEmb (decide (s.1 = .done))) := byw:List Bools:State⊢ outputSymbol (scanCfg w w.length ⋯ s) = some (boolEmb (decide (s.1 = Mode.done)))
  unfold outputSymbolw:List Bools:State⊢ (match (scanCfg w w.length ⋯ s).state with
  | none => none
  | some q => (unaryScanner.tr q (scanCfg w w.length ⋯ s).inputSymbol (scanCfg w w.length ⋯ s).workTapeSymbols).outS) =
  some (boolEmb (decide (s.1 = Mode.done)))
  change (unaryScanner.tr (modeState s.1) _ _).outS = _w:List Bools:State⊢ (unaryScanner.tr (modeState s.1) (scanCfg w w.length ⋯ s).inputSymbol (scanCfg w w.length ⋯ s).workTapeSymbols).outS =
  some (boolEmb (decide (s.1 = Mode.done)))
  rw [scanCfg_inputSymbol_endw:List Bools:State⊢ (unaryScanner.tr (modeState s.1) none (scanCfg w w.length ⋯ s).workTapeSymbols).outS =
  some (boolEmb (decide (s.1 = Mode.done)))]w:List Bools:State⊢ (unaryScanner.tr (modeState s.1) none (scanCfg w w.length ⋯ s).workTapeSymbols).outS =
  some (boolEmb (decide (s.1 = Mode.done)))
  rcases s with ⟨m, n⟩w:List Boolm:Moden:ℕ⊢ (unaryScanner.tr (modeState (m, n).1) none (scanCfg w w.length ⋯ (m, n)).workTapeSymbols).outS =
  some (boolEmb (decide ((m, n).1 = Mode.done)))
  cases mtreew:List Booln:ℕ⊢ (unaryScanner.tr (modeState (Mode.tree, n).1) none (scanCfg w w.length ⋯ (Mode.tree, n)).workTapeSymbols).outS =
  some (boolEmb (decide ((Mode.tree, n).1 = Mode.done)))stringw:List Booln:ℕ⊢ (unaryScanner.tr (modeState (Mode.string, n).1) none (scanCfg w w.length ⋯ (Mode.string, n)).workTapeSymbols).outS =
  some (boolEmb (decide ((Mode.string, n).1 = Mode.done)))bitw:List Booln:ℕ⊢ (unaryScanner.tr (modeState (Mode.bit, n).1) none (scanCfg w w.length ⋯ (Mode.bit, n)).workTapeSymbols).outS =
  some (boolEmb (decide ((Mode.bit, n).1 = Mode.done)))donew:List Booln:ℕ⊢ (unaryScanner.tr (modeState (Mode.done, n).1) none (scanCfg w w.length ⋯ (Mode.done, n)).workTapeSymbols).outS =
  some (boolEmb (decide ((Mode.done, n).1 = Mode.done)))deadw:List Booln:ℕ⊢ (unaryScanner.tr (modeState (Mode.dead, n).1) none (scanCfg w w.length ⋯ (Mode.dead, n)).workTapeSymbols).outS =
  some (boolEmb (decide ((Mode.dead, n).1 = Mode.done))) <;>treew:List Booln:ℕ⊢ (unaryScanner.tr (modeState (Mode.tree, n).1) none (scanCfg w w.length ⋯ (Mode.tree, n)).workTapeSymbols).outS =
  some (boolEmb (decide ((Mode.tree, n).1 = Mode.done)))stringw:List Booln:ℕ⊢ (unaryScanner.tr (modeState (Mode.string, n).1) none (scanCfg w w.length ⋯ (Mode.string, n)).workTapeSymbols).outS =
  some (boolEmb (decide ((Mode.string, n).1 = Mode.done)))bitw:List Booln:ℕ⊢ (unaryScanner.tr (modeState (Mode.bit, n).1) none (scanCfg w w.length ⋯ (Mode.bit, n)).workTapeSymbols).outS =
  some (boolEmb (decide ((Mode.bit, n).1 = Mode.done)))donew:List Booln:ℕ⊢ (unaryScanner.tr (modeState (Mode.done, n).1) none (scanCfg w w.length ⋯ (Mode.done, n)).workTapeSymbols).outS =
  some (boolEmb (decide ((Mode.done, n).1 = Mode.done)))deadw:List Booln:ℕ⊢ (unaryScanner.tr (modeState (Mode.dead, n).1) none (scanCfg w w.length ⋯ (Mode.dead, n)).workTapeSymbols).outS =
  some (boolEmb (decide ((Mode.dead, n).1 = Mode.done))) rflAll goals completed! 🐙

Initialization takes two steps and emits nothing.

theorem init_run (w : List Bool) :
    unaryScanner.configs (unaryScanner.initCfg (w.map boolEmb)) 2 =
        scanCfg w 0 (byw:List Bool⊢ 0 ≤ w.length omegaAll goals completed! 🐙) (.tree, 1) ∧
      unaryScanner.outputString (unaryScanner.initCfg (w.map boolEmb)) 2 = [] := byw:List Bool⊢ configs (initCfg (List.map (⇑boolEmb) w)) 2 = scanCfg w 0 ⋯ (Mode.tree, 1) ∧
  unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) 2 = []
  constructorleftw:List Bool⊢ configs (initCfg (List.map (⇑boolEmb) w)) 2 = scanCfg w 0 ⋯ (Mode.tree, 1)rightw:List Bool⊢ unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) 2 = []
  ·leftw:List Bool⊢ configs (initCfg (List.map (⇑boolEmb) w)) 2 = scanCfg w 0 ⋯ (Mode.tree, 1) change unaryScanner.configs (unaryScanner.initCfg (w.map boolEmb)) (0 + 1 + 1) = _leftw:List Bool⊢ configs (initCfg (List.map (⇑boolEmb) w)) (0 + 1 + 1) = scanCfg w 0 ⋯ (Mode.tree, 1)
    rw [configs_succ_eq_step',leftw:List Bool⊢ MultiTapeTM.step (configs (initCfg (List.map (⇑boolEmb) w)) 1) = scanCfg w 0 ⋯ (Mode.tree, 1) configs_succ_eq_step',leftw:List Bool⊢ MultiTapeTM.step (MultiTapeTM.step (configs (initCfg (List.map (⇑boolEmb) w)) 0)) = scanCfg w 0 ⋯ (Mode.tree, 1)
      configs_zero,leftw:List Bool⊢ MultiTapeTM.step (MultiTapeTM.step (initCfg (List.map (⇑boolEmb) w))) = scanCfg w 0 ⋯ (Mode.tree, 1) init_step,leftw:List Bool⊢ MultiTapeTM.step (plantCfg w) = scanCfg w 0 ⋯ (Mode.tree, 1) plant_stepleftw:List Bool⊢ scanCfg w 0 ⋯ (Mode.tree, 1) = scanCfg w 0 ⋯ (Mode.tree, 1)]All goals completed! 🐙
  ·rightw:List Bool⊢ unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) 2 = [] rflAll goals completed! 🐙

At every prefix boundary the machine realizes the pure scanner without output.

theorem configs_scan (w : List Bool) :
    ∀ t, ∀ h : t ≤ w.length,
      unaryScanner.configs (unaryScanner.initCfg (w.map boolEmb)) (t + 2) =
          scanCfg w t h (scan (w.take t)) ∧
        unaryScanner.outputString (unaryScanner.initCfg (w.map boolEmb)) (t + 2) = [] := byw:List Bool⊢ ∀ (t : ℕ) (h : t ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t h (scan (List.take t w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []
  refine Nat.rec ?_ ?_refine_1w:List Bool⊢ ∀ (h : Nat.zero ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (Nat.zero + 2) = scanCfg w Nat.zero h (scan (List.take Nat.zero w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (Nat.zero + 2) = []refine_2w:List Bool⊢ ∀ (n : ℕ),
  (∀ (h : n ≤ w.length),
      configs (initCfg (List.map (⇑boolEmb) w)) (n + 2) = scanCfg w n h (scan (List.take n w)) ∧
        unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (n + 2) = []) →
    ∀ (h : n.succ ≤ w.length),
      configs (initCfg (List.map (⇑boolEmb) w)) (n.succ + 2) = scanCfg w n.succ h (scan (List.take n.succ w)) ∧
        unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (n.succ + 2) = []
  ·refine_1w:List Bool⊢ ∀ (h : Nat.zero ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (Nat.zero + 2) = scanCfg w Nat.zero h (scan (List.take Nat.zero w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (Nat.zero + 2) = [] intro hrefine_1w:List Boolh:Nat.zero ≤ w.length⊢ configs (initCfg (List.map (⇑boolEmb) w)) (Nat.zero + 2) = scanCfg w Nat.zero h (scan (List.take Nat.zero w)) ∧
  unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (Nat.zero + 2) = []
    exact init_run wAll goals completed! 🐙
  ·refine_2w:List Bool⊢ ∀ (n : ℕ),
  (∀ (h : n ≤ w.length),
      configs (initCfg (List.map (⇑boolEmb) w)) (n + 2) = scanCfg w n h (scan (List.take n w)) ∧
        unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (n + 2) = []) →
    ∀ (h : n.succ ≤ w.length),
      configs (initCfg (List.map (⇑boolEmb) w)) (n.succ + 2) = scanCfg w n.succ h (scan (List.take n.succ w)) ∧
        unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (n.succ + 2) = [] intro t ih hrefine_2w:List Boolt:ℕih:∀ (h : t ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t h (scan (List.take t w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []h:t.succ ≤ w.length⊢ configs (initCfg (List.map (⇑boolEmb) w)) (t.succ + 2) = scanCfg w t.succ h (scan (List.take t.succ w)) ∧
  unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t.succ + 2) = []
    obtain ⟨hc, ho⟩ := ih (byw:List Boolt:ℕih:∀ (h : t ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t h (scan (List.take t w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []h:t.succ ≤ w.length⊢ t ≤ w.length omegaAll goals completed! 🐙)refine_2w:List Boolt:ℕih:∀ (h : t ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t h (scan (List.take t w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []h:t.succ ≤ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t ⋯ (scan (List.take t w))ho:unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []⊢ configs (initCfg (List.map (⇑boolEmb) w)) (t.succ + 2) = scanCfg w t.succ h (scan (List.take t.succ w)) ∧
  unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t.succ + 2) = []
    have ht : t < w.length := byw:List Bool⊢ ∀ (t : ℕ) (h : t ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t h (scan (List.take t w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = [] omegarefine_2w:List Boolt:ℕih:∀ (h : t ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t h (scan (List.take t w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []h:t.succ ≤ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t ⋯ (scan (List.take t w))ho:unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []ht:t < w.length⊢ configs (initCfg (List.map (⇑boolEmb) w)) (t.succ + 2) = scanCfg w t.succ h (scan (List.take t.succ w)) ∧
  unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t.succ + 2) = []
    rw [show t + 1 + 2 = (t + 2) + 1 byw:List Bool⊢ ∀ (t : ℕ) (h : t ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t h (scan (List.take t w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = [] omegaAll goals completed! 🐙]refine_2w:List Boolt:ℕih:∀ (h : t ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t h (scan (List.take t w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []h:t.succ ≤ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t ⋯ (scan (List.take t w))ho:unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []ht:t < w.length⊢ configs (initCfg (List.map (⇑boolEmb) w)) (t + 2 + 1) = scanCfg w t.succ h (scan (List.take t.succ w)) ∧
  unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2 + 1) = []
    constructorrefine_2.leftw:List Boolt:ℕih:∀ (h : t ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t h (scan (List.take t w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []h:t.succ ≤ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t ⋯ (scan (List.take t w))ho:unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []ht:t < w.length⊢ configs (initCfg (List.map (⇑boolEmb) w)) (t + 2 + 1) = scanCfg w t.succ h (scan (List.take t.succ w))refine_2.rightw:List Boolt:ℕih:∀ (h : t ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t h (scan (List.take t w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []h:t.succ ≤ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t ⋯ (scan (List.take t w))ho:unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []ht:t < w.length⊢ unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2 + 1) = []
    ·refine_2.leftw:List Boolt:ℕih:∀ (h : t ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t h (scan (List.take t w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []h:t.succ ≤ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t ⋯ (scan (List.take t w))ho:unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []ht:t < w.length⊢ configs (initCfg (List.map (⇑boolEmb) w)) (t + 2 + 1) = scanCfg w t.succ h (scan (List.take t.succ w)) rw [configs_succ_eq_step',refine_2.leftw:List Boolt:ℕih:∀ (h : t ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t h (scan (List.take t w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []h:t.succ ≤ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t ⋯ (scan (List.take t w))ho:unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []ht:t < w.length⊢ MultiTapeTM.step (configs (initCfg (List.map (⇑boolEmb) w)) (t + 2)) = scanCfg w t.succ h (scan (List.take t.succ w)) hc,refine_2.leftw:List Boolt:ℕih:∀ (h : t ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t h (scan (List.take t w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []h:t.succ ≤ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t ⋯ (scan (List.take t w))ho:unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []ht:t < w.length⊢ MultiTapeTM.step (scanCfg w t ⋯ (scan (List.take t w))) = scanCfg w t.succ h (scan (List.take t.succ w)) scanCfg_step w t ht _
        (fun hs ↦ scan_active_pos _ (Or.inr (Or.inl hs))),refine_2.leftw:List Boolt:ℕih:∀ (h : t ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t h (scan (List.take t w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []h:t.succ ≤ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t ⋯ (scan (List.take t w))ho:unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []ht:t < w.length⊢ scanCfg w (t + 1) ht (step (scan (List.take t w)) w[t]) = scanCfg w t.succ h (scan (List.take t.succ w)) ← scan_take_succ w t htrefine_2.leftw:List Boolt:ℕih:∀ (h : t ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t h (scan (List.take t w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []h:t.succ ≤ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t ⋯ (scan (List.take t w))ho:unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []ht:t < w.length⊢ scanCfg w (t + 1) ht (scan (List.take (t + 1) w)) = scanCfg w t.succ h (scan (List.take t.succ w))]All goals completed! 🐙
    ·refine_2.rightw:List Boolt:ℕih:∀ (h : t ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t h (scan (List.take t w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []h:t.succ ≤ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t ⋯ (scan (List.take t w))ho:unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []ht:t < w.length⊢ unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2 + 1) = [] rw [outputString_succ,refine_2.rightw:List Boolt:ℕih:∀ (h : t ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t h (scan (List.take t w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []h:t.succ ≤ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t ⋯ (scan (List.take t w))ho:unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []ht:t < w.length⊢ unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) ++
    (outputSymbol (configs (initCfg (List.map (⇑boolEmb) w)) (t + 2))).toList =
  [] ho,refine_2.rightw:List Boolt:ℕih:∀ (h : t ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t h (scan (List.take t w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []h:t.succ ≤ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t ⋯ (scan (List.take t w))ho:unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []ht:t < w.length⊢ [] ++ (outputSymbol (configs (initCfg (List.map (⇑boolEmb) w)) (t + 2))).toList = [] hc,refine_2.rightw:List Boolt:ℕih:∀ (h : t ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t h (scan (List.take t w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []h:t.succ ≤ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t ⋯ (scan (List.take t w))ho:unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []ht:t < w.length⊢ [] ++ (outputSymbol (scanCfg w t ⋯ (scan (List.take t w)))).toList = [] outputSymbol_scanCfg w t htrefine_2.rightw:List Boolt:ℕih:∀ (h : t ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t h (scan (List.take t w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []h:t.succ ≤ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t ⋯ (scan (List.take t w))ho:unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []ht:t < w.length⊢ [] ++ none.toList = []]refine_2.rightw:List Boolt:ℕih:∀ (h : t ≤ w.length),
  configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t h (scan (List.take t w)) ∧
    unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []h:t.succ ≤ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (t + 2) = scanCfg w t ⋯ (scan (List.take t w))ho:unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (t + 2) = []ht:t < w.length⊢ [] ++ none.toList = []
      rflAll goals completed! 🐙

The recognizer halts after one transition per bit and three fixed transitions.

theorem halts_at (w : List Bool) :
    (unaryScanner.configs (unaryScanner.initCfg (w.map boolEmb))
      (w.length + 3)).state = none := byw:List Bool⊢ (configs (initCfg (List.map (⇑boolEmb) w)) (w.length + 3)).state = none
  rw [show w.length + 3 = (w.length + 2) + 1 byw:List Bool⊢ (configs (initCfg (List.map (⇑boolEmb) w)) (w.length + 3)).state = none omegaAll goals completed! 🐙, configs_succ_eq_step',w:List Bool⊢ (MultiTapeTM.step (configs (initCfg (List.map (⇑boolEmb) w)) (w.length + 2))).state = none
    (configs_scan w w.length (byw:List Bool⊢ w.length ≤ w.length omegaAll goals completed! 🐙)).1]w:List Bool⊢ (MultiTapeTM.step (scanCfg w w.length ⋯ (scan (List.take w.length w)))).state = none
  exact scanCfg_halts w _All goals completed! 🐙

The sole output is the scanner's decision bit.

theorem outputString_eq (w : List Bool) :
    unaryScanner.outputString (unaryScanner.initCfg (w.map boolEmb)) (w.length + 3) =
      [boolEmb (validBool w)] := byw:List Bool⊢ unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (w.length + 3) = [boolEmb (validBool w)]
  rw [show w.length + 3 = (w.length + 2) + 1 byw:List Bool⊢ unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (w.length + 3) = [boolEmb (validBool w)] omegaAll goals completed! 🐙, outputString_succ,w:List Bool⊢ unaryScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (w.length + 2) ++
    (outputSymbol (configs (initCfg (List.map (⇑boolEmb) w)) (w.length + 2))).toList =
  [boolEmb (validBool w)]
    (configs_scan w w.length (byw:List Bool⊢ w.length ≤ w.length omegaAll goals completed! 🐙)).1, (configs_scan w w.length (byw:List Bool⊢ w.length ≤ w.length omegaAll goals completed! 🐙)).2,
    outputSymbol_scanCfg_endw:List Bool⊢ [] ++ (some (boolEmb (decide ((scan (List.take w.length w)).1 = Mode.done)))).toList = [boolEmb (validBool w)]]w:List Bool⊢ [] ++ (some (boolEmb (decide ((scan (List.take w.length w)).1 = Mode.done)))).toList = [boolEmb (validBool w)]
  simp [validBool]All goals completed! 🐙

end Geb.BitTree