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.MachineRead
public import Geb.Prototypes.Computability.BitTree.Elias.MachineCounter

set_option doc.verso true

Head bounds for the simple decoder phases

Tree tags, unary header bits, and already completed or rejected scans take only one or two transitions per input bit. Their direct configuration equations give bounds for every prefix.

Tags

Elias delta code, Turing machine, space bound

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

One transition between bounded configurations stays bounded at both possible prefixes.

theorem configs_one_headBound {input : List (Fin 3)}
    (cfg next : Cfg 4 (Fin 3) Control input) (width : ℕ)
    (hs : machine.step cfg = next) (hcfg : HeadBound width cfg) (hnext : HeadBound width next)
    (t : ℕ) (ht : t ≤ 1) : HeadBound width (machine.configs cfg t) := byinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputnext:Cfg 4 (Fin 3) Control inputwidth:ℕhs:step cfg = nexthcfg:HeadBound width cfghnext:HeadBound width nextt:ℕht:t ≤ 1⊢ HeadBound width (configs cfg t)
  apply headBound_succ cfg 0 width hcfg ?_ t htinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputnext:Cfg 4 (Fin 3) Control inputwidth:ℕhs:step cfg = nexthcfg:HeadBound width cfghnext:HeadBound width nextt:ℕht:t ≤ 1⊢ ∀ t ≤ 0, HeadBound width (configs (step cfg) t)
  intro r hrinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputnext:Cfg 4 (Fin 3) Control inputwidth:ℕhs:step cfg = nexthcfg:HeadBound width cfghnext:HeadBound width nextt:ℕht:t ≤ 1r:ℕhr:r ≤ 0⊢ HeadBound width (configs (step cfg) r)
  have he : r = 0 := byinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputnext:Cfg 4 (Fin 3) Control inputwidth:ℕhs:step cfg = nexthcfg:HeadBound width cfghnext:HeadBound width nextt:ℕht:t ≤ 1⊢ HeadBound width (configs cfg t) omegainput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputnext:Cfg 4 (Fin 3) Control inputwidth:ℕhs:step cfg = nexthcfg:HeadBound width cfghnext:HeadBound width nextt:ℕht:t ≤ 1r:ℕhr:r ≤ 0he:r = 0⊢ HeadBound width (configs (step cfg) r)
  subst rinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputnext:Cfg 4 (Fin 3) Control inputwidth:ℕhs:step cfg = nexthcfg:HeadBound width cfghnext:HeadBound width nextt:ℕht:t ≤ 1hr:0 ≤ 0⊢ HeadBound width (configs (step cfg) 0)
  rw [configs_zero,input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputnext:Cfg 4 (Fin 3) Control inputwidth:ℕhs:step cfg = nexthcfg:HeadBound width cfghnext:HeadBound width nextt:ℕht:t ≤ 1hr:0 ≤ 0⊢ HeadBound width (step cfg) hsinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputnext:Cfg 4 (Fin 3) Control inputwidth:ℕhs:step cfg = nexthcfg:HeadBound width cfghnext:HeadBound width nextt:ℕht:t ≤ 1hr:0 ≤ 0⊢ HeadBound width next]input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputnext:Cfg 4 (Fin 3) Control inputwidth:ℕhs:step cfg = nexthcfg:HeadBound width cfghnext:HeadBound width nextt:ℕht:t ≤ 1hr:0 ≤ 0⊢ HeadBound width next
  exact hnextAll goals completed! 🐙

A tree tag uses at most one additional pending position or payload-field cell.

theorem configs_tree_headBound (input : List (Fin 3)) (pos : Fin (input.length + 2))
    (pending : ℕ) (bs cs : List Bool) (b : Bool) (width : ℕ)
    (hp : pending + 1 ≤ width) (hb : bs.length + 2 ≤ width) (hc : cs.length + 2 ≤ width)
    (hin : (scanCfg input pos stTree pending 0 bs cs).inputSymbol = some (boolEmb b))
    (t : ℕ) (ht : t ≤ 1) :
    HeadBound width (machine.configs (scanCfg input pos stTree pending 0 bs cs) t) := byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:pending + 1 ≤ widthhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widthhin:(scanCfg input pos stTree pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ 1⊢ HeadBound width (configs (scanCfg input pos stTree pending 0 bs cs) t)
  apply configs_one_headBound _ _ width (step_tree input pos pending 0 bs cs b hin)
    (scanCfg_headBound _ _ _ _ _ _ _ _ (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:pending + 1 ≤ widthhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widthhin:(scanCfg input pos stTree pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ 1⊢ pending ≤ width omegaAll goals completed! 🐙) (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:pending + 1 ≤ widthhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widthhin:(scanCfg input pos stTree pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ 1⊢ 0 ≤ width omegaAll goals completed! 🐙) (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:pending + 1 ≤ widthhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widthhin:(scanCfg input pos stTree pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ 1⊢ bs.length + 1 ≤ width omegaAll goals completed! 🐙) (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:pending + 1 ≤ widthhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widthhin:(scanCfg input pos stTree pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ 1⊢ cs.length + 1 ≤ width omegaAll goals completed! 🐙)) ?_ t ht
  cases bfalseinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolwidth:ℕhp:pending + 1 ≤ widthhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕht:t ≤ 1hin:(scanCfg input pos stTree pending 0 bs cs).inputSymbol = some (boolEmb false)⊢ HeadBound width
  (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) 0 bs cs
  else scanCfg input (moveInputPos pos 1) stZeros pending 0 bs (true :: cs))trueinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolwidth:ℕhp:pending + 1 ≤ widthhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕht:t ≤ 1hin:(scanCfg input pos stTree pending 0 bs cs).inputSymbol = some (boolEmb true)⊢ HeadBound width
  (if true = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) 0 bs cs
  else scanCfg input (moveInputPos pos 1) stZeros pending 0 bs (true :: cs))
  ·falseinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolwidth:ℕhp:pending + 1 ≤ widthhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕht:t ≤ 1hin:(scanCfg input pos stTree pending 0 bs cs).inputSymbol = some (boolEmb false)⊢ HeadBound width
  (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) 0 bs cs
  else scanCfg input (moveInputPos pos 1) stZeros pending 0 bs (true :: cs)) exact scanCfg_headBound _ _ _ _ _ _ _ _ (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolwidth:ℕhp:pending + 1 ≤ widthhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕht:t ≤ 1hin:(scanCfg input pos stTree pending 0 bs cs).inputSymbol = some (boolEmb false)⊢ pending ≤ width omegaAll goals completed! 🐙) (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolwidth:ℕhp:pending + 1 ≤ widthhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕht:t ≤ 1hin:(scanCfg input pos stTree pending 0 bs cs).inputSymbol = some (boolEmb false)⊢ 0 ≤ width omegaAll goals completed! 🐙) (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolwidth:ℕhp:pending + 1 ≤ widthhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕht:t ≤ 1hin:(scanCfg input pos stTree pending 0 bs cs).inputSymbol = some (boolEmb false)⊢ bs.length + 1 ≤ width omegaAll goals completed! 🐙)
      (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolwidth:ℕhp:pending + 1 ≤ widthhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕht:t ≤ 1hin:(scanCfg input pos stTree pending 0 bs cs).inputSymbol = some (boolEmb false)⊢ (true :: cs).length + 1 ≤ width simpa only [List.length_cons] using hcAll goals completed! 🐙)
  ·trueinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolwidth:ℕhp:pending + 1 ≤ widthhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕht:t ≤ 1hin:(scanCfg input pos stTree pending 0 bs cs).inputSymbol = some (boolEmb true)⊢ HeadBound width
  (if true = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) 0 bs cs
  else scanCfg input (moveInputPos pos 1) stZeros pending 0 bs (true :: cs)) exact scanCfg_headBound _ _ _ _ _ _ _ _ hp (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolwidth:ℕhp:pending + 1 ≤ widthhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕht:t ≤ 1hin:(scanCfg input pos stTree pending 0 bs cs).inputSymbol = some (boolEmb true)⊢ 0 ≤ width omegaAll goals completed! 🐙) (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolwidth:ℕhp:pending + 1 ≤ widthhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕht:t ≤ 1hin:(scanCfg input pos stTree pending 0 bs cs).inputSymbol = some (boolEmb true)⊢ bs.length + 1 ≤ width omegaAll goals completed! 🐙) (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolwidth:ℕhp:pending + 1 ≤ widthhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕht:t ≤ 1hin:(scanCfg input pos stTree pending 0 bs cs).inputSymbol = some (boolEmb true)⊢ cs.length + 1 ≤ width omegaAll goals completed! 🐙)

A unary header zero uses one additional unary counter position.

theorem configs_zeros_false_headBound (input : List (Fin 3)) (pos : Fin (input.length + 2))
    (pending zeros : ℕ) (bs cs : List Bool) (width : ℕ)
    (hp : pending ≤ width) (hz : zeros + 1 ≤ width)
    (hb : bs.length + 1 ≤ width) (hc : cs.length + 1 ≤ width)
    (hin : (scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb false))
    (t : ℕ) (ht : t ≤ 1) :
    HeadBound width (machine.configs (scanCfg input pos stZeros pending zeros bs cs) t) := byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolwidth:ℕhp:pending ≤ widthhz:zeros + 1 ≤ widthhb:bs.length + 1 ≤ widthhc:cs.length + 1 ≤ widthhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb false)t:ℕht:t ≤ 1⊢ HeadBound width (configs (scanCfg input pos stZeros pending zeros bs cs) t)
  apply configs_one_headBound _ _ width (step_zeros input pos pending zeros bs cs false hin)
    (scanCfg_headBound _ _ _ _ _ _ _ _ hp (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolwidth:ℕhp:pending ≤ widthhz:zeros + 1 ≤ widthhb:bs.length + 1 ≤ widthhc:cs.length + 1 ≤ widthhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb false)t:ℕht:t ≤ 1⊢ zeros ≤ width omegaAll goals completed! 🐙) hb hc) ?_ t ht
  exact scanCfg_headBound _ _ _ _ _ _ _ _ hp hz hb hcAll goals completed! 🐙

A nonempty unary header ends by initializing the width field and testing its unary count.

theorem configs_zeros_true_headBound (input : List (Fin 3)) (pos : Fin (input.length + 2))
    (pending zeros width : ℕ) (hz : 0 < zeros) (hpw : pending ≤ width)
    (hzw : zeros ≤ width) (hw : 2 ≤ width)
    (hin : (scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true))
    (t : ℕ) (ht : t ≤ 2) :
    HeadBound width (machine.configs (scanCfg input pos stZeros pending zeros [] [true]) t) := byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕwidth:ℕhz:0 < zeroshpw:pending ≤ widthhzw:zeros ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 2⊢ HeadBound width (configs (scanCfg input pos stZeros pending zeros [] [true]) t)
  have hs := step_zeros input pos pending zeros [] [true] true hininput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕwidth:ℕhz:0 < zeroshpw:pending ≤ widthhzw:zeros ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 2hs:step (scanCfg input pos stZeros pending zeros [] [true]) =
  if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]
  else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) [] [true]⊢ HeadBound width (configs (scanCfg input pos stZeros pending zeros [] [true]) t)
  simp only [ite_true] at hsinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕwidth:ℕhz:0 < zeroshpw:pending ≤ widthhzw:zeros ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 2hs:step (scanCfg input pos stZeros pending zeros [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]⊢ HeadBound width (configs (scanCfg input pos stZeros pending zeros [] [true]) t)
  have hc := step_sizeCheck input (moveInputPos pos 1) pending zeros [true] [true]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕwidth:ℕhz:0 < zeroshpw:pending ≤ widthhzw:zeros ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 2hs:step (scanCfg input pos stZeros pending zeros [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]) =
  scanCfg input (moveInputPos pos 1) (if zeros = 0 then stDecrement false else stSizeBit) pending zeros [true] [true]⊢ HeadBound width (configs (scanCfg input pos stZeros pending zeros [] [true]) t)
  rw [ite_eq_right (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕwidth:ℕhz:0 < zeroshpw:pending ≤ widthhzw:zeros ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 2hs:step (scanCfg input pos stZeros pending zeros [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]) =
  scanCfg input (moveInputPos pos 1) (if zeros = 0 then stDecrement false else stSizeBit) pending zeros [true] [true]⊢ zeros ≠ 0 omegaAll goals completed! 🐙 : zeros ≠ 0)] at hcinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕwidth:ℕhz:0 < zeroshpw:pending ≤ widthhzw:zeros ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 2hs:step (scanCfg input pos stZeros pending zeros [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true]⊢ HeadBound width (configs (scanCfg input pos stZeros pending zeros [] [true]) t)
  apply headBound_succ _ 1 width
    (scanCfg_headBound _ _ _ _ _ _ _ _ hpw hzw (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕwidth:ℕhz:0 < zeroshpw:pending ≤ widthhzw:zeros ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 2hs:step (scanCfg input pos stZeros pending zeros [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true]⊢ [].length + 1 ≤ width simpinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕwidth:ℕhz:0 < zeroshpw:pending ≤ widthhzw:zeros ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 2hs:step (scanCfg input pos stZeros pending zeros [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true]⊢ 1 ≤ width; omegaAll goals completed! 🐙) (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕwidth:ℕhz:0 < zeroshpw:pending ≤ widthhzw:zeros ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 2hs:step (scanCfg input pos stZeros pending zeros [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true]⊢ [true].length + 1 ≤ width simpa using hwAll goals completed! 🐙)) ?_ t ht
  rw [hsinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕwidth:ℕhz:0 < zeroshpw:pending ≤ widthhzw:zeros ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 2hs:step (scanCfg input pos stZeros pending zeros [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true]⊢ ∀ t ≤ 1, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]) t)]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕwidth:ℕhz:0 < zeroshpw:pending ≤ widthhzw:zeros ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 2hs:step (scanCfg input pos stZeros pending zeros [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true]⊢ ∀ t ≤ 1, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]) t)
  intro r hrinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕwidth:ℕhz:0 < zeroshpw:pending ≤ widthhzw:zeros ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 2hs:step (scanCfg input pos stZeros pending zeros [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true]r:ℕhr:r ≤ 1⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]) r)
  apply configs_one_headBound _ _ width hc
    (scanCfg_headBound _ _ _ _ _ _ _ _ hpw hzw (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕwidth:ℕhz:0 < zeroshpw:pending ≤ widthhzw:zeros ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 2hs:step (scanCfg input pos stZeros pending zeros [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true]r:ℕhr:r ≤ 1⊢ [true].length + 1 ≤ width simpa using hwAll goals completed! 🐙) (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕwidth:ℕhz:0 < zeroshpw:pending ≤ widthhzw:zeros ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 2hs:step (scanCfg input pos stZeros pending zeros [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true]r:ℕhr:r ≤ 1⊢ [true].length + 1 ≤ width simpa using hwAll goals completed! 🐙))
    (scanCfg_headBound _ _ _ _ _ _ _ _ hpw hzw (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕwidth:ℕhz:0 < zeroshpw:pending ≤ widthhzw:zeros ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 2hs:step (scanCfg input pos stZeros pending zeros [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true]r:ℕhr:r ≤ 1⊢ [true].length + 1 ≤ width simpa using hwAll goals completed! 🐙) (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕwidth:ℕhz:0 < zeroshpw:pending ≤ widthhzw:zeros ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 2hs:step (scanCfg input pos stZeros pending zeros [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true]r:ℕhr:r ≤ 1⊢ [true].length + 1 ≤ width simpa using hwAll goals completed! 🐙)) r hr

Bits after completion or rejection leave all work-tape head positions unchanged.

theorem configs_terminal_headBound {input : List (Fin 3)}
    (cfg : Cfg 4 (Fin 3) Control input) (q : Control) (b : Bool) (width : ℕ)
    (hq : cfg.state = some q) (htm : q = stDone ∨ q = stDead)
    (hin : cfg.inputSymbol = some (boolEmb b)) (hcfg : HeadBound width cfg)
    (t : ℕ) (ht : t ≤ 1) : HeadBound width (machine.configs cfg t) := byinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputq:Controlb:Boolwidth:ℕhq:cfg.state = some qhtm:q = stDone ∨ q = stDeadhin:cfg.inputSymbol = some (boolEmb b)hcfg:HeadBound width cfgt:ℕht:t ≤ 1⊢ HeadBound width (configs cfg t)
  apply configs_one_headBound cfg (machine.step cfg) width rfl hcfg ?_ t htinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputq:Controlb:Boolwidth:ℕhq:cfg.state = some qhtm:q = stDone ∨ q = stDeadhin:cfg.inputSymbol = some (boolEmb b)hcfg:HeadBound width cfgt:ℕht:t ≤ 1⊢ HeadBound width (step cfg)
  intro iinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputq:Controlb:Boolwidth:ℕhq:cfg.state = some qhtm:q = stDone ∨ q = stDeadhin:cfg.inputSymbol = some (boolEmb b)hcfg:HeadBound width cfgt:ℕht:t ≤ 1i:Fin 4⊢ 0 ≤ (step cfg).workTapePos i ∧ (step cfg).workTapePos i ≤ ↑width
  have hread : q = stTree ∨ q = stZeros ∨ q = stSizeBit ∨ q = stLengthBit ∨
      q = stPayloadBit ∨ q = stDone ∨ q = stDead :=
    Or.inr (Or.inr (Or.inr (Or.inr (Or.inr htm))))input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputq:Controlb:Boolwidth:ℕhq:cfg.state = some qhtm:q = stDone ∨ q = stDeadhin:cfg.inputSymbol = some (boolEmb b)hcfg:HeadBound width cfgt:ℕht:t ≤ 1i:Fin 4hread:q = stTree ∨ q = stZeros ∨ q = stSizeBit ∨ q = stLengthBit ∨ q = stPayloadBit ∨ q = stDone ∨ q = stDead⊢ 0 ≤ (step cfg).workTapePos i ∧ (step cfg).workTapePos i ≤ ↑width
  rw [step_read cfg q b hq hin hreadinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputq:Controlb:Boolwidth:ℕhq:cfg.state = some qhtm:q = stDone ∨ q = stDeadhin:cfg.inputSymbol = some (boolEmb b)hcfg:HeadBound width cfgt:ℕht:t ≤ 1i:Fin 4hread:q = stTree ∨ q = stZeros ∨ q = stSizeBit ∨ q = stLengthBit ∨ q = stPayloadBit ∨ q = stDone ∨ q = stDead⊢ 0 ≤
    { state := (read q (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1,
          workTapes := fun i ↦
            match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read q (boolEmb 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 + ↑((read q (boolEmb b)).workActions i).2 }.workTapePos
      i ∧
  { state := (read q (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1,
          workTapes := fun i ↦
            match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read q (boolEmb 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 + ↑((read q (boolEmb b)).workActions i).2 }.workTapePos
      i ≤
    ↑width]input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputq:Controlb:Boolwidth:ℕhq:cfg.state = some qhtm:q = stDone ∨ q = stDeadhin:cfg.inputSymbol = some (boolEmb b)hcfg:HeadBound width cfgt:ℕht:t ≤ 1i:Fin 4hread:q = stTree ∨ q = stZeros ∨ q = stSizeBit ∨ q = stLengthBit ∨ q = stPayloadBit ∨ q = stDone ∨ q = stDead⊢ 0 ≤
    { state := (read q (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1,
          workTapes := fun i ↦
            match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read q (boolEmb 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 + ↑((read q (boolEmb b)).workActions i).2 }.workTapePos
      i ∧
  { state := (read q (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1,
          workTapes := fun i ↦
            match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read q (boolEmb 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 + ↑((read q (boolEmb b)).workActions i).2 }.workTapePos
      i ≤
    ↑width
  rcases htm with rfl | rflinlinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputb:Boolwidth:ℕhin:cfg.inputSymbol = some (boolEmb b)hcfg:HeadBound width cfgt:ℕht:t ≤ 1i:Fin 4hq:cfg.state = some stDonehread:stDone = stTree ∨
  stDone = stZeros ∨
    stDone = stSizeBit ∨ stDone = stLengthBit ∨ stDone = stPayloadBit ∨ stDone = stDone ∨ stDone = stDead⊢ 0 ≤
    { state := (read stDone (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1,
          workTapes := fun i ↦
            match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
              ((read stDone (boolEmb 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 + ↑((read stDone (boolEmb b)).workActions i).2 }.workTapePos
      i ∧
  { state := (read stDone (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1,
          workTapes := fun i ↦
            match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
              ((read stDone (boolEmb 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 + ↑((read stDone (boolEmb b)).workActions i).2 }.workTapePos
      i ≤
    ↑widthinrinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputb:Boolwidth:ℕhin:cfg.inputSymbol = some (boolEmb b)hcfg:HeadBound width cfgt:ℕht:t ≤ 1i:Fin 4hq:cfg.state = some stDeadhread:stDead = stTree ∨
  stDead = stZeros ∨
    stDead = stSizeBit ∨ stDead = stLengthBit ∨ stDead = stPayloadBit ∨ stDead = stDone ∨ stDead = stDead⊢ 0 ≤
    { state := (read stDead (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1,
          workTapes := fun i ↦
            match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
              ((read stDead (boolEmb 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 + ↑((read stDead (boolEmb b)).workActions i).2 }.workTapePos
      i ∧
  { state := (read stDead (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1,
          workTapes := fun i ↦
            match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
              ((read stDead (boolEmb 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 + ↑((read stDead (boolEmb b)).workActions i).2 }.workTapePos
      i ≤
    ↑width <;>inlinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputb:Boolwidth:ℕhin:cfg.inputSymbol = some (boolEmb b)hcfg:HeadBound width cfgt:ℕht:t ≤ 1i:Fin 4hq:cfg.state = some stDonehread:stDone = stTree ∨
  stDone = stZeros ∨
    stDone = stSizeBit ∨ stDone = stLengthBit ∨ stDone = stPayloadBit ∨ stDone = stDone ∨ stDone = stDead⊢ 0 ≤
    { state := (read stDone (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1,
          workTapes := fun i ↦
            match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
              ((read stDone (boolEmb 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 + ↑((read stDone (boolEmb b)).workActions i).2 }.workTapePos
      i ∧
  { state := (read stDone (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1,
          workTapes := fun i ↦
            match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
              ((read stDone (boolEmb 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 + ↑((read stDone (boolEmb b)).workActions i).2 }.workTapePos
      i ≤
    ↑widthinrinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputb:Boolwidth:ℕhin:cfg.inputSymbol = some (boolEmb b)hcfg:HeadBound width cfgt:ℕht:t ≤ 1i:Fin 4hq:cfg.state = some stDeadhread:stDead = stTree ∨
  stDead = stZeros ∨
    stDead = stSizeBit ∨ stDead = stLengthBit ∨ stDead = stPayloadBit ∨ stDead = stDone ∨ stDead = stDead⊢ 0 ≤
    { state := (read stDead (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1,
          workTapes := fun i ↦
            match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
              ((read stDead (boolEmb 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 + ↑((read stDead (boolEmb b)).workActions i).2 }.workTapePos
      i ∧
  { state := (read stDead (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1,
          workTapes := fun i ↦
            match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3))
              ((read stDead (boolEmb 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 + ↑((read stDead (boolEmb b)).workActions i).2 }.workTapePos
      i ≤
    ↑width
    simpa [read, stDone, stDead, stTree, stZeros, stSizeBit, stLengthBit, stPayloadBit,
      consume, jump] using hcfg iAll goals completed! 🐙

end Geb.BitTree.Elias.Machine