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

set_option doc.verso true

Reading the input and emitting the final verdict

At normalized scanner boundaries the next input symbol is either the next bit or the right end marker. The end marker causes one output bit and halting.

Main statements

inputSymbol_at identifies the next input bit.
step_end and outputSymbol_end specify the final transition.

Tags

Elias delta code, Turing machine, input, halting

              @[expose] public sectionnamespace Geb.BitTree.Elias.Machineopen Turing MultiTapeTM

Initialization installs the four origin markers and leaves one pending root.

theorem configs_start (input : List (Fin 3)) :
    machine.configs (machine.initCfg input) 1 =
      modelCfg input 1 (.tree, 1) [] [] := byinput:List (Fin 3)⊢ configs (initCfg input) 1 = modelCfg input 1 (Scanner.Mode.tree, 1) [] []
  rw [configs_succ_eq_step'input:List (Fin 3)⊢ step (configs (initCfg input) 0) = modelCfg input 1 (Scanner.Mode.tree, 1) [] []]input:List (Fin 3)⊢ step (configs (initCfg input) 0) = modelCfg input 1 (Scanner.Mode.tree, 1) [] []
  rw [Geb.TreeScanner.step_of_state _ _ stInit rflinput:List (Fin 3)⊢ { state := (machine.tr stInit (configs (initCfg input) 0).inputSymbol (configs (initCfg input) 0).workTapeSymbols).q',
    inputPos :=
      moveInputPos (configs (initCfg input) 0).inputPos
        (machine.tr stInit (configs (initCfg input) 0).inputSymbol
            (configs (initCfg input) 0).workTapeSymbols).inputMove,
    workTapes := fun i ↦
      match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
        ((machine.tr stInit (configs (initCfg input) 0).inputSymbol
                (configs (initCfg input) 0).workTapeSymbols).workActions
            i).1 with
      | none => (configs (initCfg input) 0).workTapes i
      | some s =>
        Function.update ((configs (initCfg input) 0).workTapes i) ((configs (initCfg input) 0).workTapePos i) s,
    workTapePos := fun i ↦
      (configs (initCfg input) 0).workTapePos i +
        ↑((machine.tr stInit (configs (initCfg input) 0).inputSymbol
                  (configs (initCfg input) 0).workTapeSymbols).workActions
              i).2 } =
  modelCfg input 1 (Scanner.Mode.tree, 1) [] []]input:List (Fin 3)⊢ { state := (machine.tr stInit (configs (initCfg input) 0).inputSymbol (configs (initCfg input) 0).workTapeSymbols).q',
    inputPos :=
      moveInputPos (configs (initCfg input) 0).inputPos
        (machine.tr stInit (configs (initCfg input) 0).inputSymbol
            (configs (initCfg input) 0).workTapeSymbols).inputMove,
    workTapes := fun i ↦
      match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
        ((machine.tr stInit (configs (initCfg input) 0).inputSymbol
                (configs (initCfg input) 0).workTapeSymbols).workActions
            i).1 with
      | none => (configs (initCfg input) 0).workTapes i
      | some s =>
        Function.update ((configs (initCfg input) 0).workTapes i) ((configs (initCfg input) 0).workTapePos i) s,
    workTapePos := fun i ↦
      (configs (initCfg input) 0).workTapePos i +
        ↑((machine.tr stInit (configs (initCfg input) 0).inputSymbol
                  (configs (initCfg input) 0).workTapeSymbols).workActions
              i).2 } =
  modelCfg input 1 (Scanner.Mode.tree, 1) [] []
  refine Cfg.ext rfl ?_ ?_ ?_refine_1input:List (Fin 3)⊢ { state := (machine.tr stInit (configs (initCfg input) 0).inputSymbol (configs (initCfg input) 0).workTapeSymbols).q',
      inputPos :=
        moveInputPos (configs (initCfg input) 0).inputPos
          (machine.tr stInit (configs (initCfg input) 0).inputSymbol
              (configs (initCfg input) 0).workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
          ((machine.tr stInit (configs (initCfg input) 0).inputSymbol
                  (configs (initCfg input) 0).workTapeSymbols).workActions
              i).1 with
        | none => (configs (initCfg input) 0).workTapes i
        | some s =>
          Function.update ((configs (initCfg input) 0).workTapes i) ((configs (initCfg input) 0).workTapePos i) s,
      workTapePos := fun i ↦
        (configs (initCfg input) 0).workTapePos i +
          ↑((machine.tr stInit (configs (initCfg input) 0).inputSymbol
                    (configs (initCfg input) 0).workTapeSymbols).workActions
                i).2 }.inputPos =
  (modelCfg input 1 (Scanner.Mode.tree, 1) [] []).inputPosrefine_2input:List (Fin 3)⊢ { state := (machine.tr stInit (configs (initCfg input) 0).inputSymbol (configs (initCfg input) 0).workTapeSymbols).q',
      inputPos :=
        moveInputPos (configs (initCfg input) 0).inputPos
          (machine.tr stInit (configs (initCfg input) 0).inputSymbol
              (configs (initCfg input) 0).workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
          ((machine.tr stInit (configs (initCfg input) 0).inputSymbol
                  (configs (initCfg input) 0).workTapeSymbols).workActions
              i).1 with
        | none => (configs (initCfg input) 0).workTapes i
        | some s =>
          Function.update ((configs (initCfg input) 0).workTapes i) ((configs (initCfg input) 0).workTapePos i) s,
      workTapePos := fun i ↦
        (configs (initCfg input) 0).workTapePos i +
          ↑((machine.tr stInit (configs (initCfg input) 0).inputSymbol
                    (configs (initCfg input) 0).workTapeSymbols).workActions
                i).2 }.workTapes =
  (modelCfg input 1 (Scanner.Mode.tree, 1) [] []).workTapesrefine_3input:List (Fin 3)⊢ { state := (machine.tr stInit (configs (initCfg input) 0).inputSymbol (configs (initCfg input) 0).workTapeSymbols).q',
      inputPos :=
        moveInputPos (configs (initCfg input) 0).inputPos
          (machine.tr stInit (configs (initCfg input) 0).inputSymbol
              (configs (initCfg input) 0).workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
          ((machine.tr stInit (configs (initCfg input) 0).inputSymbol
                  (configs (initCfg input) 0).workTapeSymbols).workActions
              i).1 with
        | none => (configs (initCfg input) 0).workTapes i
        | some s =>
          Function.update ((configs (initCfg input) 0).workTapes i) ((configs (initCfg input) 0).workTapePos i) s,
      workTapePos := fun i ↦
        (configs (initCfg input) 0).workTapePos i +
          ↑((machine.tr stInit (configs (initCfg input) 0).inputSymbol
                    (configs (initCfg input) 0).workTapeSymbols).workActions
                i).2 }.workTapePos =
  (modelCfg input 1 (Scanner.Mode.tree, 1) [] []).workTapePos
  ·refine_1input:List (Fin 3)⊢ { state := (machine.tr stInit (configs (initCfg input) 0).inputSymbol (configs (initCfg input) 0).workTapeSymbols).q',
      inputPos :=
        moveInputPos (configs (initCfg input) 0).inputPos
          (machine.tr stInit (configs (initCfg input) 0).inputSymbol
              (configs (initCfg input) 0).workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
          ((machine.tr stInit (configs (initCfg input) 0).inputSymbol
                  (configs (initCfg input) 0).workTapeSymbols).workActions
              i).1 with
        | none => (configs (initCfg input) 0).workTapes i
        | some s =>
          Function.update ((configs (initCfg input) 0).workTapes i) ((configs (initCfg input) 0).workTapePos i) s,
      workTapePos := fun i ↦
        (configs (initCfg input) 0).workTapePos i +
          ↑((machine.tr stInit (configs (initCfg input) 0).inputSymbol
                    (configs (initCfg input) 0).workTapeSymbols).workActions
                i).2 }.inputPos =
  (modelCfg input 1 (Scanner.Mode.tree, 1) [] []).inputPos change moveInputPos (1 : Fin (input.length + 2)) 0 = 1refine_1input:List (Fin 3)⊢ moveInputPos 1 0 = 1
    rw [moveInputPos_zerorefine_1input:List (Fin 3)⊢ 1 = 1]All goals completed! 🐙
  ·refine_2input:List (Fin 3)⊢ { state := (machine.tr stInit (configs (initCfg input) 0).inputSymbol (configs (initCfg input) 0).workTapeSymbols).q',
      inputPos :=
        moveInputPos (configs (initCfg input) 0).inputPos
          (machine.tr stInit (configs (initCfg input) 0).inputSymbol
              (configs (initCfg input) 0).workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
          ((machine.tr stInit (configs (initCfg input) 0).inputSymbol
                  (configs (initCfg input) 0).workTapeSymbols).workActions
              i).1 with
        | none => (configs (initCfg input) 0).workTapes i
        | some s =>
          Function.update ((configs (initCfg input) 0).workTapes i) ((configs (initCfg input) 0).workTapePos i) s,
      workTapePos := fun i ↦
        (configs (initCfg input) 0).workTapePos i +
          ↑((machine.tr stInit (configs (initCfg input) 0).inputSymbol
                    (configs (initCfg input) 0).workTapeSymbols).workActions
                i).2 }.workTapes =
  (modelCfg input 1 (Scanner.Mode.tree, 1) [] []).workTapes funext i zrefine_2input:List (Fin 3)i:Fin 4z:ℤ⊢ { state := (machine.tr stInit (configs (initCfg input) 0).inputSymbol (configs (initCfg input) 0).workTapeSymbols).q',
        inputPos :=
          moveInputPos (configs (initCfg input) 0).inputPos
            (machine.tr stInit (configs (initCfg input) 0).inputSymbol
                (configs (initCfg input) 0).workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
            ((machine.tr stInit (configs (initCfg input) 0).inputSymbol
                    (configs (initCfg input) 0).workTapeSymbols).workActions
                i).1 with
          | none => (configs (initCfg input) 0).workTapes i
          | some s =>
            Function.update ((configs (initCfg input) 0).workTapes i) ((configs (initCfg input) 0).workTapePos i) s,
        workTapePos := fun i ↦
          (configs (initCfg input) 0).workTapePos i +
            ↑((machine.tr stInit (configs (initCfg input) 0).inputSymbol
                      (configs (initCfg input) 0).workTapeSymbols).workActions
                  i).2 }.workTapes
    i z =
  (modelCfg input 1 (Scanner.Mode.tree, 1) [] []).workTapes i z
    change (Function.update (fun _ : ℤ ↦ (none : Option (Fin 3))) 0 (some 2)) z = _refine_2input:List (Fin 3)i:Fin 4z:ℤ⊢ Function.update (fun x ↦ none) 0 (some 2) z = (modelCfg input 1 (Scanner.Mode.tree, 1) [] []).workTapes i z
    by_cases hz : z = 0posinput:List (Fin 3)i:Fin 4z:ℤhz:z = 0⊢ Function.update (fun x ↦ none) 0 (some 2) z = (modelCfg input 1 (Scanner.Mode.tree, 1) [] []).workTapes i zneginput:List (Fin 3)i:Fin 4z:ℤhz:¬z = 0⊢ Function.update (fun x ↦ none) 0 (some 2) z = (modelCfg input 1 (Scanner.Mode.tree, 1) [] []).workTapes i z
    ·posinput:List (Fin 3)i:Fin 4z:ℤhz:z = 0⊢ Function.update (fun x ↦ none) 0 (some 2) z = (modelCfg input 1 (Scanner.Mode.tree, 1) [] []).workTapes i z subst zposinput:List (Fin 3)i:Fin 4⊢ Function.update (fun x ↦ none) 0 (some 2) 0 = (modelCfg input 1 (Scanner.Mode.tree, 1) [] []).workTapes i 0
      simp [modelCfg, scanCfg, wordTape]All goals completed! 🐙
    ·neginput:List (Fin 3)i:Fin 4z:ℤhz:¬z = 0⊢ Function.update (fun x ↦ none) 0 (some 2) z = (modelCfg input 1 (Scanner.Mode.tree, 1) [] []).workTapes i z simp [modelCfg, scanCfg, wordTape, hz]All goals completed! 🐙
  ·refine_3input:List (Fin 3)⊢ { state := (machine.tr stInit (configs (initCfg input) 0).inputSymbol (configs (initCfg input) 0).workTapeSymbols).q',
      inputPos :=
        moveInputPos (configs (initCfg input) 0).inputPos
          (machine.tr stInit (configs (initCfg input) 0).inputSymbol
              (configs (initCfg input) 0).workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
          ((machine.tr stInit (configs (initCfg input) 0).inputSymbol
                  (configs (initCfg input) 0).workTapeSymbols).workActions
              i).1 with
        | none => (configs (initCfg input) 0).workTapes i
        | some s =>
          Function.update ((configs (initCfg input) 0).workTapes i) ((configs (initCfg input) 0).workTapePos i) s,
      workTapePos := fun i ↦
        (configs (initCfg input) 0).workTapePos i +
          ↑((machine.tr stInit (configs (initCfg input) 0).inputSymbol
                    (configs (initCfg input) 0).workTapeSymbols).workActions
                i).2 }.workTapePos =
  (modelCfg input 1 (Scanner.Mode.tree, 1) [] []).workTapePos funext irefine_3input:List (Fin 3)i:Fin 4⊢ { state := (machine.tr stInit (configs (initCfg input) 0).inputSymbol (configs (initCfg input) 0).workTapeSymbols).q',
        inputPos :=
          moveInputPos (configs (initCfg input) 0).inputPos
            (machine.tr stInit (configs (initCfg input) 0).inputSymbol
                (configs (initCfg input) 0).workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
            ((machine.tr stInit (configs (initCfg input) 0).inputSymbol
                    (configs (initCfg input) 0).workTapeSymbols).workActions
                i).1 with
          | none => (configs (initCfg input) 0).workTapes i
          | some s =>
            Function.update ((configs (initCfg input) 0).workTapes i) ((configs (initCfg input) 0).workTapePos i) s,
        workTapePos := fun i ↦
          (configs (initCfg input) 0).workTapePos i +
            ↑((machine.tr stInit (configs (initCfg input) 0).inputSymbol
                      (configs (initCfg input) 0).workTapeSymbols).workActions
                  i).2 }.workTapePos
    i =
  (modelCfg input 1 (Scanner.Mode.tree, 1) [] []).workTapePos i
    exact Fin.cases rfl (Fin.cases rfl (Fin.cases rfl (Fin.cases rfl (fun j ↦ Fin.elim0 j)))) iAll goals completed! 🐙

Initialization does not emit output.

theorem outputString_start (input : List (Fin 3)) :
    machine.outputString (machine.initCfg input) 1 = [] := rfl

Initialization visits only the origin and its immediate right neighbor.

theorem headBound_start (input : List (Fin 3)) (width : ℕ) (hw : 1 ≤ width) :
    ∀ t ≤ 1, HeadBound width (machine.configs (machine.initCfg input) t) := byinput:List (Fin 3)width:ℕhw:1 ≤ width⊢ ∀ t ≤ 1, HeadBound width (configs (initCfg input) t)
  intro t htinput:List (Fin 3)width:ℕhw:1 ≤ widtht:ℕht:t ≤ 1⊢ HeadBound width (configs (initCfg input) t)
  cases t with
  | zero =>zeroinput:List (Fin 3)width:ℕhw:1 ≤ widthht:0 ≤ 1⊢ HeadBound width (configs (initCfg input) 0)
    intro izeroinput:List (Fin 3)width:ℕhw:1 ≤ widthht:0 ≤ 1i:Fin 4⊢ 0 ≤ (configs (initCfg input) 0).workTapePos i ∧ (configs (initCfg input) 0).workTapePos i ≤ ↑width
    change 0 ≤ (0 : ℤ) ∧ 0 ≤ (width : ℤ)zeroinput:List (Fin 3)width:ℕhw:1 ≤ widthht:0 ≤ 1i:Fin 4⊢ 0 ≤ 0 ∧ 0 ≤ ↑width
    exact ⟨Int.le_refl _, Int.natCast_nonneg _⟩All goals completed! 🐙
  | succ t =>succinput:List (Fin 3)width:ℕhw:1 ≤ widtht:ℕht:t + 1 ≤ 1⊢ HeadBound width (configs (initCfg input) (t + 1))
    have he : t = 0 := byinput:List (Fin 3)width:ℕhw:1 ≤ width⊢ ∀ t ≤ 1, HeadBound width (configs (initCfg input) t) omegasuccinput:List (Fin 3)width:ℕhw:1 ≤ widtht:ℕht:t + 1 ≤ 1he:t = 0⊢ HeadBound width (configs (initCfg input) (t + 1))
    subst tsuccinput:List (Fin 3)width:ℕhw:1 ≤ widthht:0 + 1 ≤ 1⊢ HeadBound width (configs (initCfg input) (0 + 1))
    rw [configs_startsuccinput:List (Fin 3)width:ℕhw:1 ≤ widthht:0 + 1 ≤ 1⊢ HeadBound width (modelCfg input 1 (Scanner.Mode.tree, 1) [] [])]succinput:List (Fin 3)width:ℕhw:1 ≤ widthht:0 + 1 ≤ 1⊢ HeadBound width (modelCfg input 1 (Scanner.Mode.tree, 1) [] [])
    exact scanCfg_headBound input 1 stTree 1 0 [] [] width hw (Nat.zero_le _) hw hwAll goals completed! 🐙

The input symbol at an interior position is the corresponding encoded boolean.

theorem inputSymbol_at (w : List Bool) (t : ℕ) (ht : t < w.length)
    (cfg : Cfg 4 (Fin 3) Control (w.map boolEmb)) (hp : cfg.inputPos.val = t + 1) :
    cfg.inputSymbol = some (boolEmb w[t]) := byw:List Boolt:ℕht:t < w.lengthcfg:Cfg 4 (Fin 3) Control (List.map (⇑boolEmb) w)hp:↑cfg.inputPos = t + 1⊢ cfg.inputSymbol = some (boolEmb w[t])
  rw [inputSymbolInner t (byw:List Boolt:ℕht:t < w.lengthcfg:Cfg 4 (Fin 3) Control (List.map (⇑boolEmb) w)hp:↑cfg.inputPos = t + 1⊢ ↑cfg.inputPos = 1 + t omegaAll goals completed! 🐙) (byw:List Boolt:ℕht:t < w.lengthcfg:Cfg 4 (Fin 3) Control (List.map (⇑boolEmb) w)hp:↑cfg.inputPos = t + 1⊢ t < (List.map (⇑boolEmb) w).length simpa only [List.length_map] using htAll goals completed! 🐙),
    List.getElem_mapw:List Boolt:ℕht:t < w.lengthcfg:Cfg 4 (Fin 3) Control (List.map (⇑boolEmb) w)hp:↑cfg.inputPos = t + 1⊢ some (boolEmb w[t]) = some (boolEmb w[t])]All goals completed! 🐙

The right end marker is read as a blank input symbol.

theorem inputSymbol_end {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input)
    (hp : cfg.inputPos.val = input.length + 1) : cfg.inputSymbol = none := byinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputhp:↑cfg.inputPos = input.length + 1⊢ cfg.inputSymbol = none
  unfold Cfg.inputSymbolinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputhp:↑cfg.inputPos = input.length + 1⊢ (if h₁ : cfg.inputPos = 0 then none
  else if h₂ : ↑cfg.inputPos = input.length + 1 then none else some input[↑cfg.inputPos - 1]) =
  none
  split_ifsposinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputhp:↑cfg.inputPos = input.length + 1h✝:cfg.inputPos = 0⊢ none = noneneginput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputhp:↑cfg.inputPos = input.length + 1h✝:¬cfg.inputPos = 0⊢ none = none <;>posinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputhp:↑cfg.inputPos = input.length + 1h✝:cfg.inputPos = 0⊢ none = noneneginput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputhp:↑cfg.inputPos = input.length + 1h✝:¬cfg.inputPos = 0⊢ none = none rflAll goals completed! 🐙

Reading the end marker in a normalized mode halts without changing any tape or head.

theorem step_end {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input)
    (m : Scanner.Mode) (hq : cfg.state = some (modeState m)) (hi : cfg.inputSymbol = none) :
    machine.step cfg = { cfg with state := none } := byinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputm:Scanner.Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ step cfg = { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }
  rw [Geb.TreeScanner.step_of_state _ _ _ hq,input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputm:Scanner.Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (machine.tr (modeState m) cfg.inputSymbol cfg.workTapeSymbols).q',
    inputPos := moveInputPos cfg.inputPos (machine.tr (modeState m) cfg.inputSymbol cfg.workTapeSymbols).inputMove,
    workTapes := fun i ↦
      match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
        ((machine.tr (modeState m) cfg.inputSymbol cfg.workTapeSymbols).workActions i).1 with
      | none => cfg.workTapes i
      | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
    workTapePos := fun i ↦
      cfg.workTapePos i + ↑((machine.tr (modeState m) cfg.inputSymbol cfg.workTapeSymbols).workActions i).2 } =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos } hi,input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputm:Scanner.Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (machine.tr (modeState m) none cfg.workTapeSymbols).q',
    inputPos := moveInputPos cfg.inputPos (machine.tr (modeState m) none cfg.workTapeSymbols).inputMove,
    workTapes := fun i ↦
      match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
        ((machine.tr (modeState m) none cfg.workTapeSymbols).workActions i).1 with
      | none => cfg.workTapes i
      | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
    workTapePos := fun i ↦
      cfg.workTapePos i + ↑((machine.tr (modeState m) none cfg.workTapeSymbols).workActions i).2 } =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos } tr_end _ _ (modeState_read m)input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputm:Scanner.Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (finish (modeState m == stDone)).q',
    inputPos := moveInputPos cfg.inputPos (finish (modeState m == stDone)).inputMove,
    workTapes := fun i ↦
      match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
        ((finish (modeState m == stDone)).workActions i).1 with
      | none => cfg.workTapes i
      | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
    workTapePos := fun i ↦ cfg.workTapePos i + ↑((finish (modeState m == stDone)).workActions i).2 } =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }]input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputm:Scanner.Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (finish (modeState m == stDone)).q',
    inputPos := moveInputPos cfg.inputPos (finish (modeState m == stDone)).inputMove,
    workTapes := fun i ↦
      match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
        ((finish (modeState m == stDone)).workActions i).1 with
      | none => cfg.workTapes i
      | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
    workTapePos := fun i ↦ cfg.workTapePos i + ↑((finish (modeState m == stDone)).workActions i).2 } =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }
  apply Cfg.extstateinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputm:Scanner.Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (finish (modeState m == stDone)).q',
      inputPos := moveInputPos cfg.inputPos (finish (modeState m == stDone)).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
          ((finish (modeState m == stDone)).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((finish (modeState m == stDone)).workActions i).2 }.state =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }.stateinputPosinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputm:Scanner.Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (finish (modeState m == stDone)).q',
      inputPos := moveInputPos cfg.inputPos (finish (modeState m == stDone)).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
          ((finish (modeState m == stDone)).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((finish (modeState m == stDone)).workActions i).2 }.inputPos =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }.inputPosworkTapesinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputm:Scanner.Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (finish (modeState m == stDone)).q',
      inputPos := moveInputPos cfg.inputPos (finish (modeState m == stDone)).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
          ((finish (modeState m == stDone)).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((finish (modeState m == stDone)).workActions i).2 }.workTapes =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }.workTapesworkTapePosinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputm:Scanner.Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (finish (modeState m == stDone)).q',
      inputPos := moveInputPos cfg.inputPos (finish (modeState m == stDone)).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
          ((finish (modeState m == stDone)).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((finish (modeState m == stDone)).workActions i).2 }.workTapePos =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }.workTapePos <;>stateinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputm:Scanner.Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (finish (modeState m == stDone)).q',
      inputPos := moveInputPos cfg.inputPos (finish (modeState m == stDone)).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
          ((finish (modeState m == stDone)).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((finish (modeState m == stDone)).workActions i).2 }.state =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }.stateinputPosinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputm:Scanner.Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (finish (modeState m == stDone)).q',
      inputPos := moveInputPos cfg.inputPos (finish (modeState m == stDone)).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
          ((finish (modeState m == stDone)).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((finish (modeState m == stDone)).workActions i).2 }.inputPos =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }.inputPosworkTapesinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputm:Scanner.Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (finish (modeState m == stDone)).q',
      inputPos := moveInputPos cfg.inputPos (finish (modeState m == stDone)).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
          ((finish (modeState m == stDone)).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((finish (modeState m == stDone)).workActions i).2 }.workTapes =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }.workTapesworkTapePosinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputm:Scanner.Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (finish (modeState m == stDone)).q',
      inputPos := moveInputPos cfg.inputPos (finish (modeState m == stDone)).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
          ((finish (modeState m == stDone)).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((finish (modeState m == stDone)).workActions i).2 }.workTapePos =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }.workTapePos simp [finish, jump]All goals completed! 🐙

The final output bit says exactly whether the scanner completed its root.

theorem outputSymbol_end {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input)
    (m : Scanner.Mode) (hq : cfg.state = some (modeState m)) (hi : cfg.inputSymbol = none) :
    machine.outputSymbol cfg = some (boolEmb (decide (m = .done))) := byinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputm:Scanner.Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ outputSymbol cfg = some (boolEmb (decide (m = Scanner.Mode.done)))
  unfold outputSymbolinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputm:Scanner.Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ (match cfg.state with
  | none => none
  | some q => (machine.tr q cfg.inputSymbol cfg.workTapeSymbols).outS) =
  some (boolEmb (decide (m = Scanner.Mode.done)))
  rw [hqinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputm:Scanner.Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ (match some (modeState m) with
  | none => none
  | some q => (machine.tr q cfg.inputSymbol cfg.workTapeSymbols).outS) =
  some (boolEmb (decide (m = Scanner.Mode.done)))]input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputm:Scanner.Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ (match some (modeState m) with
  | none => none
  | some q => (machine.tr q cfg.inputSymbol cfg.workTapeSymbols).outS) =
  some (boolEmb (decide (m = Scanner.Mode.done)))
  dsimp onlyinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputm:Scanner.Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ (machine.tr (modeState m) cfg.inputSymbol cfg.workTapeSymbols).outS = some (boolEmb (decide (m = Scanner.Mode.done)))
  rw [hi,input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputm:Scanner.Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ (machine.tr (modeState m) none cfg.workTapeSymbols).outS = some (boolEmb (decide (m = Scanner.Mode.done))) tr_end _ _ (modeState_read m)input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputm:Scanner.Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ (finish (modeState m == stDone)).outS = some (boolEmb (decide (m = Scanner.Mode.done)))]input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputm:Scanner.Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ (finish (modeState m == stDone)).outS = some (boolEmb (decide (m = Scanner.Mode.done)))
  cases mtreeinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputhi:cfg.inputSymbol = nonehq:cfg.state = some (modeState Scanner.Mode.tree)⊢ (finish (modeState Scanner.Mode.tree == stDone)).outS = some (boolEmb (decide (Scanner.Mode.tree = Scanner.Mode.done)))zerosinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputhi:cfg.inputSymbol = nonecount✝:ℕhq:cfg.state = some (modeState (Scanner.Mode.zeros count✝))⊢ (finish (modeState (Scanner.Mode.zeros count✝) == stDone)).outS =
  some (boolEmb (decide (Scanner.Mode.zeros count✝ = Scanner.Mode.done)))sizeinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputhi:cfg.inputSymbol = noneremaining✝:ℕvalue✝:ℕhq:cfg.state = some (modeState (Scanner.Mode.size remaining✝ value✝))⊢ (finish (modeState (Scanner.Mode.size remaining✝ value✝) == stDone)).outS =
  some (boolEmb (decide (Scanner.Mode.size remaining✝ value✝ = Scanner.Mode.done)))lengthinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputhi:cfg.inputSymbol = noneremaining✝:ℕvalue✝:ℕhq:cfg.state = some (modeState (Scanner.Mode.length remaining✝ value✝))⊢ (finish (modeState (Scanner.Mode.length remaining✝ value✝) == stDone)).outS =
  some (boolEmb (decide (Scanner.Mode.length remaining✝ value✝ = Scanner.Mode.done)))payloadinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputhi:cfg.inputSymbol = noneremaining✝:ℕhq:cfg.state = some (modeState (Scanner.Mode.payload remaining✝))⊢ (finish (modeState (Scanner.Mode.payload remaining✝) == stDone)).outS =
  some (boolEmb (decide (Scanner.Mode.payload remaining✝ = Scanner.Mode.done)))doneinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputhi:cfg.inputSymbol = nonehq:cfg.state = some (modeState Scanner.Mode.done)⊢ (finish (modeState Scanner.Mode.done == stDone)).outS = some (boolEmb (decide (Scanner.Mode.done = Scanner.Mode.done)))deadinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputhi:cfg.inputSymbol = nonehq:cfg.state = some (modeState Scanner.Mode.dead)⊢ (finish (modeState Scanner.Mode.dead == stDone)).outS = some (boolEmb (decide (Scanner.Mode.dead = Scanner.Mode.done))) <;>treeinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputhi:cfg.inputSymbol = nonehq:cfg.state = some (modeState Scanner.Mode.tree)⊢ (finish (modeState Scanner.Mode.tree == stDone)).outS = some (boolEmb (decide (Scanner.Mode.tree = Scanner.Mode.done)))zerosinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputhi:cfg.inputSymbol = nonecount✝:ℕhq:cfg.state = some (modeState (Scanner.Mode.zeros count✝))⊢ (finish (modeState (Scanner.Mode.zeros count✝) == stDone)).outS =
  some (boolEmb (decide (Scanner.Mode.zeros count✝ = Scanner.Mode.done)))sizeinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputhi:cfg.inputSymbol = noneremaining✝:ℕvalue✝:ℕhq:cfg.state = some (modeState (Scanner.Mode.size remaining✝ value✝))⊢ (finish (modeState (Scanner.Mode.size remaining✝ value✝) == stDone)).outS =
  some (boolEmb (decide (Scanner.Mode.size remaining✝ value✝ = Scanner.Mode.done)))lengthinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputhi:cfg.inputSymbol = noneremaining✝:ℕvalue✝:ℕhq:cfg.state = some (modeState (Scanner.Mode.length remaining✝ value✝))⊢ (finish (modeState (Scanner.Mode.length remaining✝ value✝) == stDone)).outS =
  some (boolEmb (decide (Scanner.Mode.length remaining✝ value✝ = Scanner.Mode.done)))payloadinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputhi:cfg.inputSymbol = noneremaining✝:ℕhq:cfg.state = some (modeState (Scanner.Mode.payload remaining✝))⊢ (finish (modeState (Scanner.Mode.payload remaining✝) == stDone)).outS =
  some (boolEmb (decide (Scanner.Mode.payload remaining✝ = Scanner.Mode.done)))doneinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputhi:cfg.inputSymbol = nonehq:cfg.state = some (modeState Scanner.Mode.done)⊢ (finish (modeState Scanner.Mode.done == stDone)).outS = some (boolEmb (decide (Scanner.Mode.done = Scanner.Mode.done)))deadinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputhi:cfg.inputSymbol = nonehq:cfg.state = some (modeState Scanner.Mode.dead)⊢ (finish (modeState Scanner.Mode.dead == stDone)).outS = some (boolEmb (decide (Scanner.Mode.dead = Scanner.Mode.done))) rflAll goals completed! 🐙

end Geb.BitTree.Elias.Machine