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

set_option doc.verso true

The empty-payload transition

The shortest delta header encodes length zero. Reading its terminating one initializes the width counter; two binary countdowns then reach zero and erase both fields before completing the leaf. The entire transition takes sixteen machine steps.

Main statements

configs_empty_leaf proves the exact result and cost of the empty-leaf transition.
configs_empty_leaf_headBound bounds every intermediate work-tape head.

Tags

Elias delta code, Turing machine, empty leaf, simulation

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

Decrementing the one-bit width field reaches the payload countdown with a zero width.

theorem configs_empty_width (input : List (Fin 3)) (pos : Fin (input.length + 2))
    (pending : ℕ) :
    machine.configs (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 =
      scanCfg input pos (stDecrement true) pending 0 [false] [true] ∧
    machine.outputString (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 =
      [] := byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕ⊢ configs (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 =
    scanCfg input pos (stDecrement true) pending 0 [false] [true] ∧
  machine.outputString (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 = []
  have h := configs_decrement
    (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [true]
    (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕ⊢ 0 < Counter.value [true] decideAll goals completed! 🐙)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕh:configs
      (counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [true] (stDecrement false)
        ([true].length + 1))
      (2 * [true].length + 3) =
    counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false (Counter.decrement [true])
      (afterDecrement false ((Counter.decrement [true]).any id)) ([true].length + 1) ∧
  machine.outputString
      (counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [true] (stDecrement false)
        ([true].length + 1))
      (2 * [true].length + 3) =
    []⊢ configs (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 =
    scanCfg input pos (stDecrement true) pending 0 [false] [true] ∧
  machine.outputString (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 = []
  change machine.configs (counterCfg _ false [true] (stDecrement false) 2) 5 =
    counterCfg _ false [false] (stDecrement true) 2 ∧ _ at hinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕh:configs (counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [true] (stDecrement false) 2)
      5 =
    counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [false] (stDecrement true) 2 ∧
  machine.outputString
      (counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [true] (stDecrement false)
        ([true].length + 1))
      (2 * [true].length + 3) =
    []⊢ configs (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 =
    scanCfg input pos (stDecrement true) pending 0 [false] [true] ∧
  machine.outputString (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 = []
  have hstart := counterCfg_scanCfg_false input pos (stDecrement false) (stDecrement false)
    pending 0 [true] [true] [true]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕh:configs (counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [true] (stDecrement false) 2)
      5 =
    counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [false] (stDecrement true) 2 ∧
  machine.outputString
      (counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [true] (stDecrement false)
        ([true].length + 1))
      (2 * [true].length + 3) =
    []hstart:counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [true] (stDecrement false)
    ([true].length + 1) =
  scanCfg input pos (stDecrement false) pending 0 [true] [true]⊢ configs (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 =
    scanCfg input pos (stDecrement true) pending 0 [false] [true] ∧
  machine.outputString (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 = []
  have hend := counterCfg_scanCfg_false input pos (stDecrement false) (stDecrement true)
    pending 0 [true] [true] [false]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕh:configs (counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [true] (stDecrement false) 2)
      5 =
    counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [false] (stDecrement true) 2 ∧
  machine.outputString
      (counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [true] (stDecrement false)
        ([true].length + 1))
      (2 * [true].length + 3) =
    []hstart:counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [true] (stDecrement false)
    ([true].length + 1) =
  scanCfg input pos (stDecrement false) pending 0 [true] [true]hend:counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [false] (stDecrement true)
    ([false].length + 1) =
  scanCfg input pos (stDecrement true) pending 0 [false] [true]⊢ configs (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 =
    scanCfg input pos (stDecrement true) pending 0 [false] [true] ∧
  machine.outputString (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 = []
  simp only [List.length_cons, List.length_nil, Nat.reduceAdd] at hstart hendinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕh:configs (counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [true] (stDecrement false) 2)
      5 =
    counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [false] (stDecrement true) 2 ∧
  machine.outputString
      (counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [true] (stDecrement false)
        ([true].length + 1))
      (2 * [true].length + 3) =
    []hstart:counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [true] (stDecrement false) 2 =
  scanCfg input pos (stDecrement false) pending 0 [true] [true]hend:counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [false] (stDecrement true) 2 =
  scanCfg input pos (stDecrement true) pending 0 [false] [true]⊢ configs (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 =
    scanCfg input pos (stDecrement true) pending 0 [false] [true] ∧
  machine.outputString (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 = []
  simp only [List.length_cons, List.length_nil, Nat.reduceAdd, Nat.reduceMul] at hinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕh:configs (counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [true] (stDecrement false) 2)
      5 =
    counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [false] (stDecrement true) 2 ∧
  machine.outputString
      (counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [true] (stDecrement false) 2)
      5 =
    []hstart:counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [true] (stDecrement false) 2 =
  scanCfg input pos (stDecrement false) pending 0 [true] [true]hend:counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [false] (stDecrement true) 2 =
  scanCfg input pos (stDecrement true) pending 0 [false] [true]⊢ configs (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 =
    scanCfg input pos (stDecrement true) pending 0 [false] [true] ∧
  machine.outputString (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 = []
  rw [hstart,input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕh:configs (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 =
    counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [false] (stDecrement true) 2 ∧
  machine.outputString (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 = []hstart:counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [true] (stDecrement false) 2 =
  scanCfg input pos (stDecrement false) pending 0 [true] [true]hend:counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [false] (stDecrement true) 2 =
  scanCfg input pos (stDecrement true) pending 0 [false] [true]⊢ configs (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 =
    scanCfg input pos (stDecrement true) pending 0 [false] [true] ∧
  machine.outputString (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 = [] hendinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕh:configs (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 =
    scanCfg input pos (stDecrement true) pending 0 [false] [true] ∧
  machine.outputString (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 = []hstart:counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [true] (stDecrement false) 2 =
  scanCfg input pos (stDecrement false) pending 0 [true] [true]hend:counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [false] (stDecrement true) 2 =
  scanCfg input pos (stDecrement true) pending 0 [false] [true]⊢ configs (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 =
    scanCfg input pos (stDecrement true) pending 0 [false] [true] ∧
  machine.outputString (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 = []] at hinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕh:configs (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 =
    scanCfg input pos (stDecrement true) pending 0 [false] [true] ∧
  machine.outputString (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 = []hstart:counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [true] (stDecrement false) 2 =
  scanCfg input pos (stDecrement false) pending 0 [true] [true]hend:counterCfg (scanCfg input pos (stDecrement false) pending 0 [true] [true]) false [false] (stDecrement true) 2 =
  scanCfg input pos (stDecrement true) pending 0 [false] [true]⊢ configs (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 =
    scanCfg input pos (stDecrement true) pending 0 [false] [true] ∧
  machine.outputString (scanCfg input pos (stDecrement false) pending 0 [true] [true]) 5 = []
  exact hAll goals completed! 🐙

Decrementing the one-bit payload field reaches cleanup with both fields zero.

theorem configs_empty_payload (input : List (Fin 3)) (pos : Fin (input.length + 2))
    (pending : ℕ) :
    machine.configs (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 =
      scanCfg input pos stClear pending 0 [false] [false] ∧
    machine.outputString (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 =
      [] := byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕ⊢ configs (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 =
    scanCfg input pos stClear pending 0 [false] [false] ∧
  machine.outputString (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 = []
  have h := configs_decrement
    (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [true]
    (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕ⊢ 0 < Counter.value [true] decideAll goals completed! 🐙)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕh:configs
      (counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [true] (stDecrement true)
        ([true].length + 1))
      (2 * [true].length + 3) =
    counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true (Counter.decrement [true])
      (afterDecrement true ((Counter.decrement [true]).any id)) ([true].length + 1) ∧
  machine.outputString
      (counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [true] (stDecrement true)
        ([true].length + 1))
      (2 * [true].length + 3) =
    []⊢ configs (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 =
    scanCfg input pos stClear pending 0 [false] [false] ∧
  machine.outputString (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 = []
  change machine.configs (counterCfg _ true [true] (stDecrement true) 2) 5 =
    counterCfg _ true [false] stClear 2 ∧ _ at hinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕh:configs (counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [true] (stDecrement true) 2)
      5 =
    counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [false] stClear 2 ∧
  machine.outputString
      (counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [true] (stDecrement true)
        ([true].length + 1))
      (2 * [true].length + 3) =
    []⊢ configs (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 =
    scanCfg input pos stClear pending 0 [false] [false] ∧
  machine.outputString (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 = []
  have hstart := counterCfg_scanCfg_true input pos (stDecrement true) (stDecrement true)
    pending 0 [false] [true] [true]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕh:configs (counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [true] (stDecrement true) 2)
      5 =
    counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [false] stClear 2 ∧
  machine.outputString
      (counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [true] (stDecrement true)
        ([true].length + 1))
      (2 * [true].length + 3) =
    []hstart:counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [true] (stDecrement true)
    ([true].length + 1) =
  scanCfg input pos (stDecrement true) pending 0 [false] [true]⊢ configs (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 =
    scanCfg input pos stClear pending 0 [false] [false] ∧
  machine.outputString (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 = []
  have hend := counterCfg_scanCfg_true input pos (stDecrement true) stClear
    pending 0 [false] [true] [false]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕh:configs (counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [true] (stDecrement true) 2)
      5 =
    counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [false] stClear 2 ∧
  machine.outputString
      (counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [true] (stDecrement true)
        ([true].length + 1))
      (2 * [true].length + 3) =
    []hstart:counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [true] (stDecrement true)
    ([true].length + 1) =
  scanCfg input pos (stDecrement true) pending 0 [false] [true]hend:counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [false] stClear ([false].length + 1) =
  scanCfg input pos stClear pending 0 [false] [false]⊢ configs (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 =
    scanCfg input pos stClear pending 0 [false] [false] ∧
  machine.outputString (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 = []
  simp only [List.length_cons, List.length_nil, Nat.reduceAdd] at hstart hendinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕh:configs (counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [true] (stDecrement true) 2)
      5 =
    counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [false] stClear 2 ∧
  machine.outputString
      (counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [true] (stDecrement true)
        ([true].length + 1))
      (2 * [true].length + 3) =
    []hstart:counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [true] (stDecrement true) 2 =
  scanCfg input pos (stDecrement true) pending 0 [false] [true]hend:counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [false] stClear 2 =
  scanCfg input pos stClear pending 0 [false] [false]⊢ configs (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 =
    scanCfg input pos stClear pending 0 [false] [false] ∧
  machine.outputString (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 = []
  simp only [List.length_cons, List.length_nil, Nat.reduceAdd, Nat.reduceMul] at hinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕh:configs (counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [true] (stDecrement true) 2)
      5 =
    counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [false] stClear 2 ∧
  machine.outputString
      (counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [true] (stDecrement true) 2) 5 =
    []hstart:counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [true] (stDecrement true) 2 =
  scanCfg input pos (stDecrement true) pending 0 [false] [true]hend:counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [false] stClear 2 =
  scanCfg input pos stClear pending 0 [false] [false]⊢ configs (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 =
    scanCfg input pos stClear pending 0 [false] [false] ∧
  machine.outputString (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 = []
  rw [hstart,input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕh:configs (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 =
    counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [false] stClear 2 ∧
  machine.outputString (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 = []hstart:counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [true] (stDecrement true) 2 =
  scanCfg input pos (stDecrement true) pending 0 [false] [true]hend:counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [false] stClear 2 =
  scanCfg input pos stClear pending 0 [false] [false]⊢ configs (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 =
    scanCfg input pos stClear pending 0 [false] [false] ∧
  machine.outputString (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 = [] hendinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕh:configs (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 =
    scanCfg input pos stClear pending 0 [false] [false] ∧
  machine.outputString (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 = []hstart:counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [true] (stDecrement true) 2 =
  scanCfg input pos (stDecrement true) pending 0 [false] [true]hend:counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [false] stClear 2 =
  scanCfg input pos stClear pending 0 [false] [false]⊢ configs (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 =
    scanCfg input pos stClear pending 0 [false] [false] ∧
  machine.outputString (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 = []] at hinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕh:configs (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 =
    scanCfg input pos stClear pending 0 [false] [false] ∧
  machine.outputString (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 = []hstart:counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [true] (stDecrement true) 2 =
  scanCfg input pos (stDecrement true) pending 0 [false] [true]hend:counterCfg (scanCfg input pos (stDecrement true) pending 0 [false] [true]) true [false] stClear 2 =
  scanCfg input pos stClear pending 0 [false] [false]⊢ configs (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 =
    scanCfg input pos stClear pending 0 [false] [false] ∧
  machine.outputString (scanCfg input pos (stDecrement true) pending 0 [false] [true]) 5 = []
  exact hAll goals completed! 🐙

Erasing the two zero fields completes an empty leaf in four transitions.

theorem configs_empty_clear (input : List (Fin 3)) (pos : Fin (input.length + 2))
    (pending : ℕ) (hp : 0 < pending) :
    machine.configs (scanCfg input pos stClear pending 0 [false] [false]) 4 =
      modelCfg input pos (Scanner.finish pending) [] [] ∧
    machine.outputString (scanCfg input pos stClear pending 0 [false] [false]) 4 = [] := byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhp:0 < pending⊢ configs (scanCfg input pos stClear pending 0 [false] [false]) 4 = modelCfg input pos (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stClear pending 0 [false] [false]) 4 = []
  have h := configs_clear_ready (scanCfg input pos stClear pending 0 [false] [false])
    [false] [false] 2 2input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhp:0 < pendingh:configs (clearingCfg (scanCfg input pos stClear pending 0 [false] [false]) [false] [false] 2 2) (max 2 2 + 2) =
    completedCfg (scanCfg input pos stClear pending 0 [false] [false]) ∧
  machine.outputString (clearingCfg (scanCfg input pos stClear pending 0 [false] [false]) [false] [false] 2 2)
      (max 2 2 + 2) =
    []⊢ configs (scanCfg input pos stClear pending 0 [false] [false]) 4 = modelCfg input pos (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stClear pending 0 [false] [false]) 4 = []
  have hn := clearingCfg_scanCfg input pos stClear pending 0 [false] [false]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhp:0 < pendingh:configs (clearingCfg (scanCfg input pos stClear pending 0 [false] [false]) [false] [false] 2 2) (max 2 2 + 2) =
    completedCfg (scanCfg input pos stClear pending 0 [false] [false]) ∧
  machine.outputString (clearingCfg (scanCfg input pos stClear pending 0 [false] [false]) [false] [false] 2 2)
      (max 2 2 + 2) =
    []hn:clearingCfg (scanCfg input pos stClear pending 0 [false] [false]) [false] [false] ([false].length + 1)
    ([false].length + 1) =
  scanCfg input pos stClear pending 0 [false] [false]⊢ configs (scanCfg input pos stClear pending 0 [false] [false]) 4 = modelCfg input pos (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stClear pending 0 [false] [false]) 4 = []
  simp only [List.length_cons, List.length_nil, Nat.reduceAdd] at hninput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhp:0 < pendingh:configs (clearingCfg (scanCfg input pos stClear pending 0 [false] [false]) [false] [false] 2 2) (max 2 2 + 2) =
    completedCfg (scanCfg input pos stClear pending 0 [false] [false]) ∧
  machine.outputString (clearingCfg (scanCfg input pos stClear pending 0 [false] [false]) [false] [false] 2 2)
      (max 2 2 + 2) =
    []hn:clearingCfg (scanCfg input pos stClear pending 0 [false] [false]) [false] [false] 2 2 =
  scanCfg input pos stClear pending 0 [false] [false]⊢ configs (scanCfg input pos stClear pending 0 [false] [false]) 4 = modelCfg input pos (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stClear pending 0 [false] [false]) 4 = []
  rw [hn,input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhp:0 < pendingh:configs (scanCfg input pos stClear pending 0 [false] [false]) (max 2 2 + 2) =
    completedCfg (scanCfg input pos stClear pending 0 [false] [false]) ∧
  machine.outputString (scanCfg input pos stClear pending 0 [false] [false]) (max 2 2 + 2) = []hn:clearingCfg (scanCfg input pos stClear pending 0 [false] [false]) [false] [false] 2 2 =
  scanCfg input pos stClear pending 0 [false] [false]⊢ configs (scanCfg input pos stClear pending 0 [false] [false]) 4 = modelCfg input pos (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stClear pending 0 [false] [false]) 4 = [] completedCfg_scanCfg input pos stClear pending [false] [false] hpinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhp:0 < pendingh:configs (scanCfg input pos stClear pending 0 [false] [false]) (max 2 2 + 2) =
    modelCfg input pos (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stClear pending 0 [false] [false]) (max 2 2 + 2) = []hn:clearingCfg (scanCfg input pos stClear pending 0 [false] [false]) [false] [false] 2 2 =
  scanCfg input pos stClear pending 0 [false] [false]⊢ configs (scanCfg input pos stClear pending 0 [false] [false]) 4 = modelCfg input pos (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stClear pending 0 [false] [false]) 4 = []] at hinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhp:0 < pendingh:configs (scanCfg input pos stClear pending 0 [false] [false]) (max 2 2 + 2) =
    modelCfg input pos (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stClear pending 0 [false] [false]) (max 2 2 + 2) = []hn:clearingCfg (scanCfg input pos stClear pending 0 [false] [false]) [false] [false] 2 2 =
  scanCfg input pos stClear pending 0 [false] [false]⊢ configs (scanCfg input pos stClear pending 0 [false] [false]) 4 = modelCfg input pos (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stClear pending 0 [false] [false]) 4 = []
  exact hAll goals completed! 🐙

Reading the shortest delta header finishes its empty leaf in sixteen silent steps.

theorem configs_empty_leaf (input : List (Fin 3)) (pos : Fin (input.length + 2))
    (pending : ℕ) (hp : 0 < pending)
    (hin : (scanCfg input pos stZeros pending 0 [] [true]).inputSymbol =
      some (boolEmb true)) :
    machine.configs (scanCfg input pos stZeros pending 0 [] [true]) 16 =
      modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] [] ∧
    machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) 16 = [] := byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhp:0 < pendinghin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)⊢ configs (scanCfg input pos stZeros pending 0 [] [true]) 16 =
    modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) 16 = []
  have hs := step_zeros input pos pending 0 [] [true] true hininput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhp:0 < pendinghin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]
  else scanCfg input (moveInputPos pos 1) stZeros pending (0 + 1) [] [true]⊢ configs (scanCfg input pos stZeros pending 0 [] [true]) 16 =
    modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) 16 = []
  simp only [↓reduceIte] at hsinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhp:0 < pendinghin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]⊢ configs (scanCfg input pos stZeros pending 0 [] [true]) 16 =
    modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) 16 = []
  have hread := configs_output_one _ _ hs
    (outputSymbol_read _ stZeros true rfl hin (Or.inr (Or.inl rfl)))input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhp:0 < pendinghin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]hread:configs (scanCfg input pos stZeros pending 0 [] [true]) 1 =
    scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) 1 = []⊢ configs (scanCfg input pos stZeros pending 0 [] [true]) 16 =
    modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) 16 = []
  have hc := step_sizeCheck input (moveInputPos pos 1) pending 0 [true] [true]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhp:0 < pendinghin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]hread:configs (scanCfg input pos stZeros pending 0 [] [true]) 1 =
    scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) 1 = []hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) =
  scanCfg input (moveInputPos pos 1) (if 0 = 0 then stDecrement false else stSizeBit) pending 0 [true] [true]⊢ configs (scanCfg input pos stZeros pending 0 [] [true]) 16 =
    modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) 16 = []
  simp only [ite_true] at hcinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhp:0 < pendinghin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]hread:configs (scanCfg input pos stZeros pending 0 [] [true]) 1 =
    scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) 1 = []hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) =
  scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]⊢ configs (scanCfg input pos stZeros pending 0 [] [true]) 16 =
    modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) 16 = []
  have hcheck := configs_output_one _ _ hc
    (outputSymbol_sizeCheck input (moveInputPos pos 1) pending 0 [true] [true])input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhp:0 < pendinghin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]hread:configs (scanCfg input pos stZeros pending 0 [] [true]) 1 =
    scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) 1 = []hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) =
  scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]hcheck:configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true] ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) 1 = []⊢ configs (scanCfg input pos stZeros pending 0 [] [true]) 16 =
    modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) 16 = []
  have h2 := configs_output_add _ _ _ 1 1 hread hcheckinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhp:0 < pendinghin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]hread:configs (scanCfg input pos stZeros pending 0 [] [true]) 1 =
    scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) 1 = []hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) =
  scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]hcheck:configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true] ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) 1 = []h2:configs (scanCfg input pos stZeros pending 0 [] [true]) (1 + 1) =
    scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) (1 + 1) = []⊢ configs (scanCfg input pos stZeros pending 0 [] [true]) 16 =
    modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) 16 = []
  have h7 := configs_output_add _ _ _ 2 5 h2
    (configs_empty_width input (moveInputPos pos 1) pending)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhp:0 < pendinghin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]hread:configs (scanCfg input pos stZeros pending 0 [] [true]) 1 =
    scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) 1 = []hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) =
  scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]hcheck:configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true] ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) 1 = []h2:configs (scanCfg input pos stZeros pending 0 [] [true]) (1 + 1) =
    scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) (1 + 1) = []h7:configs (scanCfg input pos stZeros pending 0 [] [true]) (2 + 5) =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) (2 + 5) = []⊢ configs (scanCfg input pos stZeros pending 0 [] [true]) 16 =
    modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) 16 = []
  have h12 := configs_output_add _ _ _ 7 5 h7
    (configs_empty_payload input (moveInputPos pos 1) pending)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhp:0 < pendinghin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]hread:configs (scanCfg input pos stZeros pending 0 [] [true]) 1 =
    scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) 1 = []hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) =
  scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]hcheck:configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true] ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) 1 = []h2:configs (scanCfg input pos stZeros pending 0 [] [true]) (1 + 1) =
    scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) (1 + 1) = []h7:configs (scanCfg input pos stZeros pending 0 [] [true]) (2 + 5) =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) (2 + 5) = []h12:configs (scanCfg input pos stZeros pending 0 [] [true]) (7 + 5) =
    scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) (7 + 5) = []⊢ configs (scanCfg input pos stZeros pending 0 [] [true]) 16 =
    modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stZeros pending 0 [] [true]) 16 = []
  exact configs_output_add _ _ _ 12 4 h12
    (configs_empty_clear input (moveInputPos pos 1) pending hp)All goals completed! 🐙

Every prefix of the empty-leaf transition stays within the initial pending count and two binary-field cells.

theorem configs_empty_leaf_headBound (input : List (Fin 3))
    (pos : Fin (input.length + 2)) (pending width : ℕ) (hp : 0 < pending)
    (hpw : pending ≤ width) (hw : 2 ≤ width)
    (hin : (scanCfg input pos stZeros pending 0 [] [true]).inputSymbol =
      some (boolEmb true)) (t : ℕ) (ht : t ≤ 16) :
    HeadBound width (machine.configs (scanCfg input pos stZeros pending 0 [] [true]) t) := byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16⊢ HeadBound width (configs (scanCfg input pos stZeros pending 0 [] [true]) t)
  have hb : ∀ q bs cs, bs.length ≤ 1 → cs.length ≤ 1 →
      HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs) := by
    intro q bs cs hbs hcsinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16q:Controlbs:List Boolcs:List Boolhbs:bs.length ≤ 1hcs:cs.length ≤ 1⊢ HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)
    exact scanCfg_headBound _ _ _ _ _ _ _ _ hpw (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16q:Controlbs:List Boolcs:List Boolhbs:bs.length ≤ 1hcs:cs.length ≤ 1⊢ 0 ≤ width omegaAll goals completed! 🐙) (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16q:Controlbs:List Boolcs:List Boolhbs:bs.length ≤ 1hcs:cs.length ≤ 1⊢ bs.length + 1 ≤ width omegaAll goals completed! 🐙) (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16q:Controlbs:List Boolcs:List Boolhbs:bs.length ≤ 1hcs:cs.length ≤ 1⊢ cs.length + 1 ≤ width omegaAll goals completed! 🐙)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)⊢ HeadBound width (configs (scanCfg input pos stZeros pending 0 [] [true]) t)
  have hwdec : ∀ r ≤ 5, HeadBound width (machine.configs
      (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r) := by
    intro r hrinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)r:ℕhr:r ≤ 5⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)
    have h := configs_decrement_headBound
      (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true])
      false [true] width (hb _ _ _ (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)r:ℕhr:r ≤ 5⊢ [true].length ≤ 1 decideAll goals completed! 🐙) (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)r:ℕhr:r ≤ 5⊢ [true].length ≤ 1 decideAll goals completed! 🐙)) (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)r:ℕhr:r ≤ 5⊢ [true].length + 1 ≤ width simpa using hwAll goals completed! 🐙)
      (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)r:ℕhr:r ≤ 5⊢ 0 < Counter.value [true] decideAll goals completed! 🐙) r hrinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)r:ℕhr:r ≤ 5h:HeadBound width
  (configs
    (counterCfg (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) false [true]
      (stDecrement false) ([true].length + 1))
    r)⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)
    rw [counterCfg_scanCfg_false input (moveInputPos pos 1) _ _ pending 0
      [true] [true] [true]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)r:ℕhr:r ≤ 5h:HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)] at hinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)r:ℕhr:r ≤ 5h:HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)
    exact hinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)⊢ HeadBound width (configs (scanCfg input pos stZeros pending 0 [] [true]) t)
  have hpdec : ∀ r ≤ 5, HeadBound width (machine.configs
      (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r) := by
    intro r hrinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)r:ℕhr:r ≤ 5⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)
    have h := configs_decrement_headBound
      (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true])
      true [true] width (hb _ _ _ (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)r:ℕhr:r ≤ 5⊢ [false].length ≤ 1 decideAll goals completed! 🐙) (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)r:ℕhr:r ≤ 5⊢ [true].length ≤ 1 decideAll goals completed! 🐙)) (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)r:ℕhr:r ≤ 5⊢ [true].length + 1 ≤ width simpa using hwAll goals completed! 🐙)
      (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)r:ℕhr:r ≤ 5⊢ 0 < Counter.value [true] decideAll goals completed! 🐙) r hrinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)r:ℕhr:r ≤ 5h:HeadBound width
  (configs
    (counterCfg (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) true [true]
      (stDecrement true) ([true].length + 1))
    r)⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)
    rw [counterCfg_scanCfg_true input (moveInputPos pos 1) _ _ pending 0
      [false] [true] [true]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)r:ℕhr:r ≤ 5h:HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)] at hinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)r:ℕhr:r ≤ 5h:HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)
    exact hinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)⊢ HeadBound width (configs (scanCfg input pos stZeros pending 0 [] [true]) t)
  have hclear : ∀ r ≤ 4, HeadBound width (machine.configs
      (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r) := by
    intro r hrinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)r:ℕhr:r ≤ 4⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)
    have h := configs_clear_headBound
      (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false])
      [false] [false] 2 2 width (hb _ _ _ (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)r:ℕhr:r ≤ 4⊢ [false].length ≤ 1 decideAll goals completed! 🐙) (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)r:ℕhr:r ≤ 4⊢ [false].length ≤ 1 decideAll goals completed! 🐙)) hw hw
      (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)r:ℕhr:r ≤ 4⊢ 1 ≤ (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]).workTapePos 0 change (1 : ℤ) ≤ pendinginput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)r:ℕhr:r ≤ 4⊢ 1 ≤ ↑pending; omegaAll goals completed! 🐙) r hrinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)r:ℕhr:r ≤ 4h:HeadBound width
  (configs (clearingCfg (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) [false] [false] 2 2) r)⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)
    have hn := clearingCfg_scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)r:ℕhr:r ≤ 4h:HeadBound width
  (configs (clearingCfg (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) [false] [false] 2 2) r)hn:clearingCfg (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) [false] [false] ([false].length + 1)
    ([false].length + 1) =
  scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)
    simp only [List.length_cons, List.length_nil, Nat.reduceAdd] at hninput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)r:ℕhr:r ≤ 4h:HeadBound width
  (configs (clearingCfg (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) [false] [false] 2 2) r)hn:clearingCfg (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) [false] [false] 2 2 =
  scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)
    rw [hninput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)r:ℕhr:r ≤ 4h:HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)hn:clearingCfg (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) [false] [false] 2 2 =
  scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)] at hinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)r:ℕhr:r ≤ 4h:HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)hn:clearingCfg (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) [false] [false] 2 2 =
  scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)
    exact hinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)⊢ HeadBound width (configs (scanCfg input pos stZeros pending 0 [] [true]) t)
  have htail : ∀ r ≤ 14, HeadBound width (machine.configs
      (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r) := by
    apply headBound_add _ 5 9 width hwdecinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)⊢ ∀ t ≤ 9,
  HeadBound width
    (configs (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) 5) t)
    rw [(configs_empty_width input (moveInputPos pos 1) pending).1input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)⊢ ∀ t ≤ 9, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) t)]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)⊢ ∀ t ≤ 9, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) t)
    apply headBound_add _ 5 4 width hpdecinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)⊢ ∀ t ≤ 4,
  HeadBound width
    (configs (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) 5) t)
    rw [(configs_empty_payload input (moveInputPos pos 1) pending).1input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)⊢ ∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)⊢ ∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)
    exact hclearinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)htail:∀ r ≤ 14, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)⊢ HeadBound width (configs (scanCfg input pos stZeros pending 0 [] [true]) t)
  have hs := step_zeros input pos pending 0 [] [true] true hininput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)htail:∀ r ≤ 14, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]
  else scanCfg input (moveInputPos pos 1) stZeros pending (0 + 1) [] [true]⊢ HeadBound width (configs (scanCfg input pos stZeros pending 0 [] [true]) t)
  simp only [↓reduceIte] at hsinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)htail:∀ r ≤ 14, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]⊢ HeadBound width (configs (scanCfg input pos stZeros pending 0 [] [true]) t)
  have hc := step_sizeCheck input (moveInputPos pos 1) pending 0 [true] [true]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)htail:∀ r ≤ 14, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) =
  scanCfg input (moveInputPos pos 1) (if 0 = 0 then stDecrement false else stSizeBit) pending 0 [true] [true]⊢ HeadBound width (configs (scanCfg input pos stZeros pending 0 [] [true]) t)
  simp only [ite_true] at hcinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)htail:∀ r ≤ 14, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) =
  scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]⊢ HeadBound width (configs (scanCfg input pos stZeros pending 0 [] [true]) t)
  apply headBound_succ _ 15 width
    (scanCfg_headBound _ _ _ _ _ _ _ _ hpw (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)htail:∀ r ≤ 14, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) =
  scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]⊢ 0 ≤ width omegaAll goals completed! 🐙) (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)htail:∀ r ≤ 14, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) =
  scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]⊢ [].length + 1 ≤ width simpinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)htail:∀ r ≤ 14, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) =
  scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]⊢ 1 ≤ width; omegaAll goals completed! 🐙) (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)htail:∀ r ≤ 14, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) =
  scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]⊢ [true].length + 1 ≤ width simpa using hwAll goals completed! 🐙)) ?_ t ht
  rw [hsinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)htail:∀ r ≤ 14, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) =
  scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]⊢ ∀ t ≤ 15, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) t)]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)htail:∀ r ≤ 14, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) =
  scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]⊢ ∀ t ≤ 15, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) t)
  intro r hrinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)htail:∀ r ≤ 14, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) =
  scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]r:ℕhr:r ≤ 15⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) r)
  apply headBound_succ _ 14 width (hb _ _ _ (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)htail:∀ r ≤ 14, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) =
  scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]r:ℕhr:r ≤ 15⊢ [true].length ≤ 1 decideAll goals completed! 🐙) (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)htail:∀ r ≤ 14, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) =
  scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]r:ℕhr:r ≤ 15⊢ [true].length ≤ 1 decideAll goals completed! 🐙)) ?_ r hr
  rw [hcinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)htail:∀ r ≤ 14, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) =
  scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]r:ℕhr:r ≤ 15⊢ ∀ r ≤ 14, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕwidth:ℕhp:0 < pendinghpw:pending ≤ widthhw:2 ≤ widthhin:(scanCfg input pos stZeros pending 0 [] [true]).inputSymbol = some (boolEmb true)t:ℕht:t ≤ 16hb:∀ (q : Control) (bs cs : List Bool),
  bs.length ≤ 1 → cs.length ≤ 1 → HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hwdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hpdec:∀ r ≤ 5, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 [false] [true]) r)hclear:∀ r ≤ 4, HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 [false] [false]) r)htail:∀ r ≤ 14, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)hs:step (scanCfg input pos stZeros pending 0 [] [true]) =
  scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending 0 [true] [true]) =
  scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]r:ℕhr:r ≤ 15⊢ ∀ r ≤ 14, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 [true] [true]) r)
  exact htailAll goals completed! 🐙

end Geb.BitTree.Elias.Machine