Imports

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

public import Geb.Prototypes.Computability.BitTree.BinaryMachine.Machine
public import Geb.Prototypes.Computability.TreeScanner.Steps

set_option doc.verso true

Input transitions of the binary-counter recognizer

Reading a bit advances the input head and selects the next scan mode or a counter-increment phase. The work tapes are unchanged during this transition.

Main statements

step_read realizes one input transition without changing work tapes.
step_end and outputSymbol_end describe the final emitting transition.
headBound_add combines bounds on consecutive execution segments.

Tags

Turing machine, simulation, binary tree, binary counter

              @[expose] public sectionnamespace Geb.BitTree.BinaryMachineopen Turing MultiTapeTMopen Geb.TreeScanner (step_of_state)

An input transition has the closed form given by consumeCfg.

theorem step_read {input : List (Fin 4)} (cfg : Cfg 3 (Fin 4) (Fin 10) input)
    (m : Mode) (b : Bool) (hq : cfg.state = some (modeState m))
    (hi : cfg.inputSymbol = some (boolEmb b)) :
    machine.step cfg = consumeCfg cfg (postReadState m b) := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modeb:Boolhq:cfg.state = some (modeState m)hi:cfg.inputSymbol = some (boolEmb b)⊢ MultiTapeTM.step cfg = consumeCfg cfg (postReadState m b)
  rw [step_of_state _ _ _ hq,input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modeb:Boolhq:cfg.state = some (modeState m)hi:cfg.inputSymbol = some (boolEmb b)⊢ { 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 4)) → ℤ → Option (Fin 4))
        ((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 } =
  consumeCfg cfg (postReadState m b) hi,input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modeb:Boolhq:cfg.state = some (modeState m)hi:cfg.inputSymbol = some (boolEmb b)⊢ { state := (machine.tr (modeState m) (some (boolEmb b)) cfg.workTapeSymbols).q',
    inputPos := moveInputPos cfg.inputPos (machine.tr (modeState m) (some (boolEmb b)) cfg.workTapeSymbols).inputMove,
    workTapes := fun i ↦
      match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
        ((machine.tr (modeState m) (some (boolEmb b)) 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) (some (boolEmb b)) cfg.workTapeSymbols).workActions i).2 } =
  consumeCfg cfg (postReadState m b) tr_readinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modeb:Boolhq:cfg.state = some (modeState m)hi:cfg.inputSymbol = some (boolEmb b)⊢ { state := (consume (postReadState m b)).q',
    inputPos := moveInputPos cfg.inputPos (consume (postReadState m b)).inputMove,
    workTapes := fun i ↦
      match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
        ((consume (postReadState m b)).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 + ↑((consume (postReadState m b)).workActions i).2 } =
  consumeCfg cfg (postReadState m b)]input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modeb:Boolhq:cfg.state = some (modeState m)hi:cfg.inputSymbol = some (boolEmb b)⊢ { state := (consume (postReadState m b)).q',
    inputPos := moveInputPos cfg.inputPos (consume (postReadState m b)).inputMove,
    workTapes := fun i ↦
      match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
        ((consume (postReadState m b)).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 + ↑((consume (postReadState m b)).workActions i).2 } =
  consumeCfg cfg (postReadState m b)
  apply Cfg.extstateinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modeb:Boolhq:cfg.state = some (modeState m)hi:cfg.inputSymbol = some (boolEmb b)⊢ { state := (consume (postReadState m b)).q',
      inputPos := moveInputPos cfg.inputPos (consume (postReadState m b)).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((consume (postReadState m b)).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 + ↑((consume (postReadState m b)).workActions i).2 }.state =
  (consumeCfg cfg (postReadState m b)).stateinputPosinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modeb:Boolhq:cfg.state = some (modeState m)hi:cfg.inputSymbol = some (boolEmb b)⊢ { state := (consume (postReadState m b)).q',
      inputPos := moveInputPos cfg.inputPos (consume (postReadState m b)).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((consume (postReadState m b)).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 + ↑((consume (postReadState m b)).workActions i).2 }.inputPos =
  (consumeCfg cfg (postReadState m b)).inputPosworkTapesinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modeb:Boolhq:cfg.state = some (modeState m)hi:cfg.inputSymbol = some (boolEmb b)⊢ { state := (consume (postReadState m b)).q',
      inputPos := moveInputPos cfg.inputPos (consume (postReadState m b)).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((consume (postReadState m b)).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 + ↑((consume (postReadState m b)).workActions i).2 }.workTapes =
  (consumeCfg cfg (postReadState m b)).workTapesworkTapePosinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modeb:Boolhq:cfg.state = some (modeState m)hi:cfg.inputSymbol = some (boolEmb b)⊢ { state := (consume (postReadState m b)).q',
      inputPos := moveInputPos cfg.inputPos (consume (postReadState m b)).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((consume (postReadState m b)).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 + ↑((consume (postReadState m b)).workActions i).2 }.workTapePos =
  (consumeCfg cfg (postReadState m b)).workTapePos <;>stateinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modeb:Boolhq:cfg.state = some (modeState m)hi:cfg.inputSymbol = some (boolEmb b)⊢ { state := (consume (postReadState m b)).q',
      inputPos := moveInputPos cfg.inputPos (consume (postReadState m b)).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((consume (postReadState m b)).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 + ↑((consume (postReadState m b)).workActions i).2 }.state =
  (consumeCfg cfg (postReadState m b)).stateinputPosinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modeb:Boolhq:cfg.state = some (modeState m)hi:cfg.inputSymbol = some (boolEmb b)⊢ { state := (consume (postReadState m b)).q',
      inputPos := moveInputPos cfg.inputPos (consume (postReadState m b)).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((consume (postReadState m b)).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 + ↑((consume (postReadState m b)).workActions i).2 }.inputPos =
  (consumeCfg cfg (postReadState m b)).inputPosworkTapesinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modeb:Boolhq:cfg.state = some (modeState m)hi:cfg.inputSymbol = some (boolEmb b)⊢ { state := (consume (postReadState m b)).q',
      inputPos := moveInputPos cfg.inputPos (consume (postReadState m b)).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((consume (postReadState m b)).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 + ↑((consume (postReadState m b)).workActions i).2 }.workTapes =
  (consumeCfg cfg (postReadState m b)).workTapesworkTapePosinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modeb:Boolhq:cfg.state = some (modeState m)hi:cfg.inputSymbol = some (boolEmb b)⊢ { state := (consume (postReadState m b)).q',
      inputPos := moveInputPos cfg.inputPos (consume (postReadState m b)).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((consume (postReadState m b)).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 + ↑((consume (postReadState m b)).workActions i).2 }.workTapePos =
  (consumeCfg cfg (postReadState m b)).workTapePos simp [consume, consumeCfg]All goals completed! 🐙

Input transitions emit nothing.

theorem outputSymbol_read {input : List (Fin 4)} (cfg : Cfg 3 (Fin 4) (Fin 10) input)
    (m : Mode) (b : Bool) (hq : cfg.state = some (modeState m))
    (hi : cfg.inputSymbol = some (boolEmb b)) : machine.outputSymbol cfg = none := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modeb:Boolhq:cfg.state = some (modeState m)hi:cfg.inputSymbol = some (boolEmb b)⊢ outputSymbol cfg = none
  unfold outputSymbolinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modeb:Boolhq:cfg.state = some (modeState m)hi:cfg.inputSymbol = some (boolEmb b)⊢ (match cfg.state with
  | none => none
  | some q => (machine.tr q cfg.inputSymbol cfg.workTapeSymbols).outS) =
  none
  rw [hqinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modeb:Boolhq:cfg.state = some (modeState m)hi:cfg.inputSymbol = some (boolEmb b)⊢ (match some (modeState m) with
  | none => none
  | some q => (machine.tr q cfg.inputSymbol cfg.workTapeSymbols).outS) =
  none]input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modeb:Boolhq:cfg.state = some (modeState m)hi:cfg.inputSymbol = some (boolEmb b)⊢ (match some (modeState m) with
  | none => none
  | some q => (machine.tr q cfg.inputSymbol cfg.workTapeSymbols).outS) =
  none
  dsimp onlyinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modeb:Boolhq:cfg.state = some (modeState m)hi:cfg.inputSymbol = some (boolEmb b)⊢ (machine.tr (modeState m) cfg.inputSymbol cfg.workTapeSymbols).outS = none
  rw [hi,input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modeb:Boolhq:cfg.state = some (modeState m)hi:cfg.inputSymbol = some (boolEmb b)⊢ (machine.tr (modeState m) (some (boolEmb b)) cfg.workTapeSymbols).outS = none tr_readinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modeb:Boolhq:cfg.state = some (modeState m)hi:cfg.inputSymbol = some (boolEmb b)⊢ (consume (postReadState m b)).outS = none]input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modeb:Boolhq:cfg.state = some (modeState m)hi:cfg.inputSymbol = some (boolEmb b)⊢ (consume (postReadState m b)).outS = none
  rflAll goals completed! 🐙

The symbol at an interior input position is its next bit.

theorem inputSymbol_at (w : List Bool) (t : ℕ) (ht : t < w.length)
    (cfg : Cfg 3 (Fin 4) (Fin 10) (w.map boolEmb)) (hp : cfg.inputPos.val = t + 1) :
    cfg.inputSymbol = some (boolEmb w[t]) := byw:List Boolt:ℕht:t < w.lengthcfg:Cfg 3 (Fin 4) (Fin 10) (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 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w)hp:↑cfg.inputPos = t + 1⊢ ↑cfg.inputPos = 1 + t omegaAll goals completed! 🐙) (byw:List Boolt:ℕht:t < w.lengthcfg:Cfg 3 (Fin 4) (Fin 10) (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 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w)hp:↑cfg.inputPos = t + 1⊢ some (boolEmb w[t]) = some (boolEmb w[t])]All goals completed! 🐙

The input symbol at the right end marker is blank.

theorem inputSymbol_end {input : List (Fin 4)} (cfg : Cfg 3 (Fin 4) (Fin 10) input)
    (hp : cfg.inputPos.val = input.length + 1) : cfg.inputSymbol = none := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputhp:↑cfg.inputPos = input.length + 1⊢ cfg.inputSymbol = none
  unfold Cfg.inputSymbolinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) 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 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputhp:↑cfg.inputPos = input.length + 1h✝:cfg.inputPos = 0⊢ none = noneneginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputhp:↑cfg.inputPos = input.length + 1h✝:¬cfg.inputPos = 0⊢ none = none <;>posinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputhp:↑cfg.inputPos = input.length + 1h✝:cfg.inputPos = 0⊢ none = noneneginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputhp:↑cfg.inputPos = input.length + 1h✝:¬cfg.inputPos = 0⊢ none = none rflAll goals completed! 🐙

At the right end marker only the finite control changes to the halting state.

theorem step_end {input : List (Fin 4)} (cfg : Cfg 3 (Fin 4) (Fin 10) input)
    (m : Mode) (hq : cfg.state = some (modeState m)) (hi : cfg.inputSymbol = none) :
    machine.step cfg = { cfg with state := none } := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ MultiTapeTM.step cfg =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }
  rw [step_of_state _ _ _ hq,input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm: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 4)) → ℤ → Option (Fin 4))
        ((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 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm: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 4)) → ℤ → Option (Fin 4))
        ((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_endinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (finish (decide (m = Mode.done))).q',
    inputPos := moveInputPos cfg.inputPos (finish (decide (m = Mode.done))).inputMove,
    workTapes := fun i ↦
      match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
        ((finish (decide (m = Mode.done))).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 (decide (m = Mode.done))).workActions i).2 } =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }]input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (finish (decide (m = Mode.done))).q',
    inputPos := moveInputPos cfg.inputPos (finish (decide (m = Mode.done))).inputMove,
    workTapes := fun i ↦
      match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
        ((finish (decide (m = Mode.done))).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 (decide (m = Mode.done))).workActions i).2 } =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }
  apply Cfg.extstateinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (finish (decide (m = Mode.done))).q',
      inputPos := moveInputPos cfg.inputPos (finish (decide (m = Mode.done))).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((finish (decide (m = Mode.done))).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 (decide (m = Mode.done))).workActions i).2 }.state =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }.stateinputPosinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (finish (decide (m = Mode.done))).q',
      inputPos := moveInputPos cfg.inputPos (finish (decide (m = Mode.done))).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((finish (decide (m = Mode.done))).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 (decide (m = Mode.done))).workActions i).2 }.inputPos =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }.inputPosworkTapesinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (finish (decide (m = Mode.done))).q',
      inputPos := moveInputPos cfg.inputPos (finish (decide (m = Mode.done))).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((finish (decide (m = Mode.done))).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 (decide (m = Mode.done))).workActions i).2 }.workTapes =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }.workTapesworkTapePosinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (finish (decide (m = Mode.done))).q',
      inputPos := moveInputPos cfg.inputPos (finish (decide (m = Mode.done))).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((finish (decide (m = Mode.done))).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 (decide (m = Mode.done))).workActions i).2 }.workTapePos =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }.workTapePos <;>stateinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (finish (decide (m = Mode.done))).q',
      inputPos := moveInputPos cfg.inputPos (finish (decide (m = Mode.done))).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((finish (decide (m = Mode.done))).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 (decide (m = Mode.done))).workActions i).2 }.state =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }.stateinputPosinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (finish (decide (m = Mode.done))).q',
      inputPos := moveInputPos cfg.inputPos (finish (decide (m = Mode.done))).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((finish (decide (m = Mode.done))).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 (decide (m = Mode.done))).workActions i).2 }.inputPos =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }.inputPosworkTapesinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (finish (decide (m = Mode.done))).q',
      inputPos := moveInputPos cfg.inputPos (finish (decide (m = Mode.done))).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((finish (decide (m = Mode.done))).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 (decide (m = Mode.done))).workActions i).2 }.workTapes =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }.workTapesworkTapePosinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ { state := (finish (decide (m = Mode.done))).q',
      inputPos := moveInputPos cfg.inputPos (finish (decide (m = Mode.done))).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((finish (decide (m = Mode.done))).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 (decide (m = Mode.done))).workActions i).2 }.workTapePos =
  { state := none, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }.workTapePos simp [finish]All goals completed! 🐙

The final transition emits exactly the accepting-mode decision.

theorem outputSymbol_end {input : List (Fin 4)} (cfg : Cfg 3 (Fin 4) (Fin 10) input)
    (m : Mode) (hq : cfg.state = some (modeState m)) (hi : cfg.inputSymbol = none) :
    machine.outputSymbol cfg = some (boolEmb (decide (m = .done))) := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ outputSymbol cfg = some (boolEmb (decide (m = Mode.done)))
  unfold outputSymbolinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm: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 = Mode.done)))
  rw [hqinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm: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 = Mode.done)))]input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm: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 = Mode.done)))
  dsimp onlyinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ (machine.tr (modeState m) cfg.inputSymbol cfg.workTapeSymbols).outS = some (boolEmb (decide (m = Mode.done)))
  rw [hi,input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ (machine.tr (modeState m) none cfg.workTapeSymbols).outS = some (boolEmb (decide (m = Mode.done))) tr_endinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ (finish (decide (m = Mode.done))).outS = some (boolEmb (decide (m = Mode.done)))]input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputm:Modehq:cfg.state = some (modeState m)hi:cfg.inputSymbol = none⊢ (finish (decide (m = Mode.done))).outS = some (boolEmb (decide (m = Mode.done)))
  rflAll goals completed! 🐙

Bounds on consecutive execution segments combine into a bound on their concatenation.

theorem headBound_add {input : List (Fin 4)} (cfg : Cfg 3 (Fin 4) (Fin 10) input)
    (width a b : ℕ)
    (ha : ∀ t ≤ a, HeadBound width (machine.configs cfg t))
    (hb : ∀ t ≤ b, HeadBound width (machine.configs (machine.configs cfg a) t)) :
    ∀ t ≤ a + b, HeadBound width (machine.configs cfg t) := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕha:∀ t ≤ a, HeadBound width (configs cfg t)hb:∀ t ≤ b, HeadBound width (configs (configs cfg a) t)⊢ ∀ t ≤ a + b, HeadBound width (configs cfg t)
  intro t htinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕha:∀ t ≤ a, HeadBound width (configs cfg t)hb:∀ t ≤ b, HeadBound width (configs (configs cfg a) t)t:ℕht:t ≤ a + b⊢ HeadBound width (configs cfg t)
  by_cases h : t ≤ aposinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕha:∀ t ≤ a, HeadBound width (configs cfg t)hb:∀ t ≤ b, HeadBound width (configs (configs cfg a) t)t:ℕht:t ≤ a + bh:t ≤ a⊢ HeadBound width (configs cfg t)neginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕha:∀ t ≤ a, HeadBound width (configs cfg t)hb:∀ t ≤ b, HeadBound width (configs (configs cfg a) t)t:ℕht:t ≤ a + bh:¬t ≤ a⊢ HeadBound width (configs cfg t)
  ·posinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕha:∀ t ≤ a, HeadBound width (configs cfg t)hb:∀ t ≤ b, HeadBound width (configs (configs cfg a) t)t:ℕht:t ≤ a + bh:t ≤ a⊢ HeadBound width (configs cfg t) exact ha t hAll goals completed! 🐙
  ·neginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕha:∀ t ≤ a, HeadBound width (configs cfg t)hb:∀ t ≤ b, HeadBound width (configs (configs cfg a) t)t:ℕht:t ≤ a + bh:¬t ≤ a⊢ HeadBound width (configs cfg t) rw [show t = a + (t - a) byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕha:∀ t ≤ a, HeadBound width (configs cfg t)hb:∀ t ≤ b, HeadBound width (configs (configs cfg a) t)⊢ ∀ t ≤ a + b, HeadBound width (configs cfg t) omegaAll goals completed! 🐙, configs_addneginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕha:∀ t ≤ a, HeadBound width (configs cfg t)hb:∀ t ≤ b, HeadBound width (configs (configs cfg a) t)t:ℕht:t ≤ a + bh:¬t ≤ a⊢ HeadBound width (configs (configs cfg a) (t - a))]neginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕha:∀ t ≤ a, HeadBound width (configs cfg t)hb:∀ t ≤ b, HeadBound width (configs (configs cfg a) t)t:ℕht:t ≤ a + bh:¬t ≤ a⊢ HeadBound width (configs (configs cfg a) (t - a))
    exact hb (t - a) (byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕha:∀ t ≤ a, HeadBound width (configs cfg t)hb:∀ t ≤ b, HeadBound width (configs (configs cfg a) t)t:ℕht:t ≤ a + bh:¬t ≤ a⊢ t - a ≤ b omegaAll goals completed! 🐙)

end Geb.BitTree.BinaryMachine