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.MachineHeader

set_option doc.verso true

Executing raw leaf payloads

Each payload bit advances the input and decrements its remaining length. The final bit also erases both binary fields and completes the leaf. These statements include the exact machine transition count and the work-tape interval visited by every execution prefix.

Main statements

configs_payload executes one raw payload bit.
configs_payload_headBound bounds all intermediate head positions.

Tags

Elias delta code, Turing machine, payload, simulation

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

Erasing complete binary fields returns to the scalar leaf-completion boundary.

theorem configs_clear_scan (input : List (Fin 3)) (pos : Fin (input.length + 2))
    (pending : ℕ) (bs cs : List Bool) (hp : 0 < pending) :
    machine.configs (scanCfg input pos stClear pending 0 bs cs)
        (max bs.length cs.length + 3) =
      modelCfg input pos (Scanner.finish pending) [] [] ∧
    machine.outputString (scanCfg input pos stClear pending 0 bs cs)
        (max bs.length cs.length + 3) = [] := byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolhp:0 < pending⊢ configs (scanCfg input pos stClear pending 0 bs cs) (max bs.length cs.length + 3) =
    modelCfg input pos (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stClear pending 0 bs cs) (max bs.length cs.length + 3) = []
  have h := configs_clear_ready (scanCfg input pos stClear pending 0 bs cs)
    bs cs (bs.length + 1) (cs.length + 1)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolhp:0 < pendingh:configs (clearingCfg (scanCfg input pos stClear pending 0 bs cs) bs cs (bs.length + 1) (cs.length + 1))
      (max (bs.length + 1) (cs.length + 1) + 2) =
    completedCfg (scanCfg input pos stClear pending 0 bs cs) ∧
  machine.outputString (clearingCfg (scanCfg input pos stClear pending 0 bs cs) bs cs (bs.length + 1) (cs.length + 1))
      (max (bs.length + 1) (cs.length + 1) + 2) =
    []⊢ configs (scanCfg input pos stClear pending 0 bs cs) (max bs.length cs.length + 3) =
    modelCfg input pos (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stClear pending 0 bs cs) (max bs.length cs.length + 3) = []
  rw [clearingCfg_scanCfg,input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolhp:0 < pendingh:configs (scanCfg input pos stClear pending 0 bs cs) (max (bs.length + 1) (cs.length + 1) + 2) =
    completedCfg (scanCfg input pos stClear pending 0 bs cs) ∧
  machine.outputString (scanCfg input pos stClear pending 0 bs cs) (max (bs.length + 1) (cs.length + 1) + 2) = []⊢ configs (scanCfg input pos stClear pending 0 bs cs) (max bs.length cs.length + 3) =
    modelCfg input pos (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stClear pending 0 bs cs) (max bs.length cs.length + 3) = [] completedCfg_scanCfg _ _ _ _ _ _ hpinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolhp:0 < pendingh:configs (scanCfg input pos stClear pending 0 bs cs) (max (bs.length + 1) (cs.length + 1) + 2) =
    modelCfg input pos (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stClear pending 0 bs cs) (max (bs.length + 1) (cs.length + 1) + 2) = []⊢ configs (scanCfg input pos stClear pending 0 bs cs) (max bs.length cs.length + 3) =
    modelCfg input pos (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stClear pending 0 bs cs) (max bs.length cs.length + 3) = []] at hinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolhp:0 < pendingh:configs (scanCfg input pos stClear pending 0 bs cs) (max (bs.length + 1) (cs.length + 1) + 2) =
    modelCfg input pos (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stClear pending 0 bs cs) (max (bs.length + 1) (cs.length + 1) + 2) = []⊢ configs (scanCfg input pos stClear pending 0 bs cs) (max bs.length cs.length + 3) =
    modelCfg input pos (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stClear pending 0 bs cs) (max bs.length cs.length + 3) = []
  simpa only [show max (bs.length + 1) (cs.length + 1) + 2 =
    max bs.length cs.length + 3 byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolhp:0 < pending⊢ configs (scanCfg input pos stClear pending 0 bs cs) (max bs.length cs.length + 3) =
    modelCfg input pos (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stClear pending 0 bs cs) (max bs.length cs.length + 3) = [] omegaAll goals completed! 🐙] using h

Reading one payload bit includes cleanup exactly when its remaining count is one.

theorem configs_payload (input : List (Fin 3)) (pos : Fin (input.length + 2))
    (pending remaining : ℕ) (bs cs : List Bool) (b : Bool)
    (hp : 0 < pending) (hr : 0 < remaining) (hc : Counter.value cs = remaining)
    (hin : (scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)) :
    machine.configs (scanCfg input pos stPayloadBit pending 0 bs cs)
        (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7
          else 2 * cs.length + 4) =
      (if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
        else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
    machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
        (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7
          else 2 * cs.length + 4) = [] := byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)⊢ (configs (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
    else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    []
  have hread := configs_output_one _ _ (step_payload input pos pending 0 bs cs b hin)
    (outputSymbol_read _ stPayloadBit b rfl hin
      (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl rfl))))))input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []⊢ (configs (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
    else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    []
  have hdec := configs_decrement_true_scan input (moveInputPos pos 1) pending 0 bs cs
    (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []⊢ 0 < Counter.value cs omegaAll goals completed! 🐙)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true ((Counter.decrement cs).any id)) pending 0 bs
      (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []⊢ (configs (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
    else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    []
  by_cases he : remaining = 1posinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true ((Counter.decrement cs).any id)) pending 0 bs
      (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:remaining = 1⊢ (configs (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
    else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    []neginput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true ((Counter.decrement cs).any id)) pending 0 bs
      (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:¬remaining = 1⊢ (configs (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
    else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    []
  ·posinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true ((Counter.decrement cs).any id)) pending 0 bs
      (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:remaining = 1⊢ (configs (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
    else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    [] have hseen : (Counter.decrement cs).any id = false := by
      apply (Counter.any_eq_false_iff _).mprinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true ((Counter.decrement cs).any id)) pending 0 bs
      (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:remaining = 1⊢ Counter.value (Counter.decrement cs) = 0
      rw [Counter.value_decrement _ (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true ((Counter.decrement cs).any id)) pending 0 bs
      (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:remaining = 1⊢ 0 < Counter.value cs omegaAll goals completed! 🐙), hc,input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true ((Counter.decrement cs).any id)) pending 0 bs
      (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:remaining = 1⊢ remaining - 1 = 0 heinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true ((Counter.decrement cs).any id)) pending 0 bs
      (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:remaining = 1⊢ 1 - 1 = 0]posinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true ((Counter.decrement cs).any id)) pending 0 bs
      (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:remaining = 1hseen:(Counter.decrement cs).any id = false⊢ (configs (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
    else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    []
    rw [hseenposinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:remaining = 1hseen:(Counter.decrement cs).any id = false⊢ (configs (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
    else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    []] at hdecposinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:remaining = 1hseen:(Counter.decrement cs).any id = false⊢ (configs (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
    else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    []
    have hfirst := configs_output_add _ _ _ 1 (2 * cs.length + 3) hread hdecposinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:remaining = 1hseen:(Counter.decrement cs).any id = falsehfirst:configs (scanCfg input pos stPayloadBit pending 0 bs cs) (1 + (2 * cs.length + 3)) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) (1 + (2 * cs.length + 3)) = []⊢ (configs (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
    else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    []
    have hclear := configs_clear_scan input (moveInputPos pos 1) pending bs
      (Counter.decrement cs) hpposinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:remaining = 1hseen:(Counter.decrement cs).any id = falsehfirst:configs (scanCfg input pos stPayloadBit pending 0 bs cs) (1 + (2 * cs.length + 3)) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) (1 + (2 * cs.length + 3)) = []hclear:configs (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs))
      (max bs.length (Counter.decrement cs).length + 3) =
    modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs))
      (max bs.length (Counter.decrement cs).length + 3) =
    []⊢ (configs (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
    else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    []
    rw [Counter.length_decrementposinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:remaining = 1hseen:(Counter.decrement cs).any id = falsehfirst:configs (scanCfg input pos stPayloadBit pending 0 bs cs) (1 + (2 * cs.length + 3)) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) (1 + (2 * cs.length + 3)) = []hclear:configs (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs)) (max bs.length cs.length + 3) =
    modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs))
      (max bs.length cs.length + 3) =
    []⊢ (configs (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
    else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    []] at hclearposinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:remaining = 1hseen:(Counter.decrement cs).any id = falsehfirst:configs (scanCfg input pos stPayloadBit pending 0 bs cs) (1 + (2 * cs.length + 3)) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) (1 + (2 * cs.length + 3)) = []hclear:configs (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs)) (max bs.length cs.length + 3) =
    modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs))
      (max bs.length cs.length + 3) =
    []⊢ (configs (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
    else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    []
    have hall := configs_output_add _ _ _ (1 + (2 * cs.length + 3))
      (max bs.length cs.length + 3) hfirst hclearposinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:remaining = 1hseen:(Counter.decrement cs).any id = falsehfirst:configs (scanCfg input pos stPayloadBit pending 0 bs cs) (1 + (2 * cs.length + 3)) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) (1 + (2 * cs.length + 3)) = []hclear:configs (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs)) (max bs.length cs.length + 3) =
    modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs))
      (max bs.length cs.length + 3) =
    []hall:configs (scanCfg input pos stPayloadBit pending 0 bs cs) (1 + (2 * cs.length + 3) + (max bs.length cs.length + 3)) =
    modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] [] ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (1 + (2 * cs.length + 3) + (max bs.length cs.length + 3)) =
    []⊢ (configs (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
    else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    []
    simpa only [he, ↓reduceIte,
      show 1 + (2 * cs.length + 3) + (max bs.length cs.length + 3) =
        2 * cs.length + max bs.length cs.length + 7 byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)⊢ (configs (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
    else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    [] omegaAll goals completed! 🐙] using hall
  ·neginput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true ((Counter.decrement cs).any id)) pending 0 bs
      (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:¬remaining = 1⊢ (configs (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
    else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    [] have hseen : (Counter.decrement cs).any id = true := by
      cases hx : (Counter.decrement cs).any id with
      | false =>falseinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true ((Counter.decrement cs).any id)) pending 0 bs
      (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:¬remaining = 1hx:(Counter.decrement cs).any id = false⊢ false = true
        have hz := (Counter.any_eq_false_iff _).mp hxfalseinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true ((Counter.decrement cs).any id)) pending 0 bs
      (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:¬remaining = 1hx:(Counter.decrement cs).any id = falsehz:Counter.value (Counter.decrement cs) = 0⊢ false = true
        rw [Counter.value_decrement _ (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true ((Counter.decrement cs).any id)) pending 0 bs
      (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:¬remaining = 1hx:(Counter.decrement cs).any id = falsehz:Counter.value (Counter.decrement cs) = 0⊢ 0 < Counter.value cs omegaAll goals completed! 🐙), hcfalseinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true ((Counter.decrement cs).any id)) pending 0 bs
      (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:¬remaining = 1hx:(Counter.decrement cs).any id = falsehz:remaining - 1 = 0⊢ false = true] at hzfalseinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true ((Counter.decrement cs).any id)) pending 0 bs
      (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:¬remaining = 1hx:(Counter.decrement cs).any id = falsehz:remaining - 1 = 0⊢ false = true
        omegaAll goals completed! 🐙
      | true =>trueinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true ((Counter.decrement cs).any id)) pending 0 bs
      (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:¬remaining = 1hx:(Counter.decrement cs).any id = true⊢ true = true rflneginput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true ((Counter.decrement cs).any id)) pending 0 bs
      (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:¬remaining = 1hseen:(Counter.decrement cs).any id = true⊢ (configs (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
    else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    []
    rw [hseenneginput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true true) pending 0 bs (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:¬remaining = 1hseen:(Counter.decrement cs).any id = true⊢ (configs (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
    else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    []] at hdecneginput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true true) pending 0 bs (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:¬remaining = 1hseen:(Counter.decrement cs).any id = true⊢ (configs (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
    else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    []
    have hall := configs_output_add _ _ _ 1 (2 * cs.length + 3) hread hdecneginput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)hread:configs (scanCfg input pos stPayloadBit pending 0 bs cs) 1 =
    scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true true) pending 0 bs (Counter.decrement cs) ∧
  machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) = []he:¬remaining = 1hseen:(Counter.decrement cs).any id = truehall:configs (scanCfg input pos stPayloadBit pending 0 bs cs) (1 + (2 * cs.length + 3)) =
    scanCfg input (moveInputPos pos 1) (afterDecrement true true) pending 0 bs (Counter.decrement cs) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs) (1 + (2 * cs.length + 3)) = []⊢ (configs (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
    else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    []
    simpa only [he, ↓reduceIte, afterDecrement,
      show 1 + (2 * cs.length + 3) = 2 * cs.length + 4 byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)⊢ (configs (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    if remaining = 1 then modelCfg input (moveInputPos pos 1) (Scanner.finish pending) [] []
    else scanCfg input (moveInputPos pos 1) stPayloadBit pending 0 bs (Counter.decrement cs)) ∧
  machine.outputString (scanCfg input pos stPayloadBit pending 0 bs cs)
      (if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) =
    [] omegaAll goals completed! 🐙] using hall

Every payload-bit execution prefix stays inside a bound containing the initial field blanks and the positive pending count.

theorem configs_payload_headBound (input : List (Fin 3)) (pos : Fin (input.length + 2))
    (pending remaining : ℕ) (bs cs : List Bool) (b : Bool) (width : ℕ)
    (hp : 0 < pending) (hr : 0 < remaining) (hc : Counter.value cs = remaining)
    (hpw : pending ≤ width) (hbw : bs.length + 1 ≤ width) (hcw : cs.length + 1 ≤ width)
    (hin : (scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b))
    (t : ℕ) (ht : t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7
      else 2 * cs.length + 4) :
    HeadBound width (machine.configs (scanCfg input pos stPayloadBit pending 0 bs cs) t) := byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4⊢ HeadBound width (configs (scanCfg input pos stPayloadBit pending 0 bs cs) t)
  have hb : ∀ q, HeadBound width
      (scanCfg input (moveInputPos pos 1) q pending 0 bs cs) := by
    intro qinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4q:Control⊢ 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:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4q:Control⊢ 0 ≤ width omegaAll goals completed! 🐙) hbw hcwinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)⊢ HeadBound width (configs (scanCfg input pos stPayloadBit pending 0 bs cs) t)
  have hdecbound : ∀ r ≤ 2 * cs.length + 3, HeadBound width (machine.configs
      (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r) := by
    intro r hr'input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)r:ℕhr':r ≤ 2 * cs.length + 3⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)
    have h := configs_decrement_headBound
      (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs)
      true cs width (hb _) hcw (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)r:ℕhr':r ≤ 2 * cs.length + 3⊢ 0 < Counter.value cs omegaAll goals completed! 🐙) r hr'input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)r:ℕhr':r ≤ 2 * cs.length + 3h:HeadBound width
  (configs
    (counterCfg (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) true cs (stDecrement true)
      (cs.length + 1))
    r)⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)
    rwa [counterCfg_scanCfg_trueinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)r:ℕhr':r ≤ 2 * cs.length + 3h:HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)r:ℕhr':r ≤ 2 * cs.length + 3h:HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r) at hinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)⊢ HeadBound width (configs (scanCfg input pos stPayloadBit pending 0 bs cs) t)
  have hstart : HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs) :=
    scanCfg_headBound _ _ _ _ _ _ _ _ hpw (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)⊢ 0 ≤ width omegaAll goals completed! 🐙) hbw hcwinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)⊢ HeadBound width (configs (scanCfg input pos stPayloadBit pending 0 bs cs) t)
  have hs := step_payload input pos pending 0 bs cs b hininput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs⊢ HeadBound width (configs (scanCfg input pos stPayloadBit pending 0 bs cs) t)
  by_cases he : remaining = 1posinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1⊢ HeadBound width (configs (scanCfg input pos stPayloadBit pending 0 bs cs) t)neginput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:¬remaining = 1⊢ HeadBound width (configs (scanCfg input pos stPayloadBit pending 0 bs cs) t)
  ·posinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1⊢ HeadBound width (configs (scanCfg input pos stPayloadBit pending 0 bs cs) t) have hseen : (Counter.decrement cs).any id = false := by
      apply (Counter.any_eq_false_iff _).mprinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1⊢ Counter.value (Counter.decrement cs) = 0
      rw [Counter.value_decrement _ (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1⊢ 0 < Counter.value cs omegaAll goals completed! 🐙), hc,input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1⊢ remaining - 1 = 0 heinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1⊢ 1 - 1 = 0]posinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = false⊢ HeadBound width (configs (scanCfg input pos stPayloadBit pending 0 bs cs) t)
    have hdec := (configs_decrement_true_scan input (moveInputPos pos 1) pending 0 bs cs
      (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = false⊢ 0 < Counter.value cs omegaAll goals completed! 🐙)).1posinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true ((Counter.decrement cs).any id)) pending 0 bs
    (Counter.decrement cs)⊢ HeadBound width (configs (scanCfg input pos stPayloadBit pending 0 bs cs) t)
    rw [hseenposinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)⊢ HeadBound width (configs (scanCfg input pos stPayloadBit pending 0 bs cs) t)] at hdecposinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)⊢ HeadBound width (configs (scanCfg input pos stPayloadBit pending 0 bs cs) t)
    have hclear : ∀ r ≤ max bs.length cs.length + 3, HeadBound width (machine.configs
        (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs)) r) := by
      intro r hr'input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)r:ℕhr':r ≤ max bs.length cs.length + 3⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs)) r)
      have h := configs_clear_headBound
        (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs))
        bs (Counter.decrement cs) (bs.length + 1) ((Counter.decrement cs).length + 1) width
        (scanCfg_headBound _ _ _ _ _ _ _ _ hpw (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)r:ℕhr':r ≤ max bs.length cs.length + 3⊢ 0 ≤ width omegaAll goals completed! 🐙) hbw
          (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)r:ℕhr':r ≤ max bs.length cs.length + 3⊢ (Counter.decrement cs).length + 1 ≤ width simpa only [Counter.length_decrement] using hcwAll goals completed! 🐙)) hbw
        (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)r:ℕhr':r ≤ max bs.length cs.length + 3⊢ (Counter.decrement cs).length + 1 ≤ width simpa only [Counter.length_decrement] using hcwAll goals completed! 🐙)
        (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)r:ℕhr':r ≤ max bs.length cs.length + 3⊢ 1 ≤ (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs)).workTapePos 0 change (1 : ℤ) ≤ pendinginput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)r:ℕhr':r ≤ max bs.length cs.length + 3⊢ 1 ≤ ↑pending; omegaAll goals completed! 🐙) r (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)r:ℕhr':r ≤ max bs.length cs.length + 3⊢ r ≤ max (bs.length + 1) ((Counter.decrement cs).length + 1) + 2 rw [Counter.length_decrementinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)r:ℕhr':r ≤ max bs.length cs.length + 3⊢ r ≤ max (bs.length + 1) (cs.length + 1) + 2]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)r:ℕhr':r ≤ max bs.length cs.length + 3⊢ r ≤ max (bs.length + 1) (cs.length + 1) + 2; omegaAll goals completed! 🐙)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)r:ℕhr':r ≤ max bs.length cs.length + 3h:HeadBound width
  (configs
    (clearingCfg (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs)) bs
      (Counter.decrement cs) (bs.length + 1) ((Counter.decrement cs).length + 1))
    r)⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs)) r)
      rwa [clearingCfg_scanCfginput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)r:ℕhr':r ≤ max bs.length cs.length + 3h:HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs)) r)⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs)) r)]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)r:ℕhr':r ≤ max bs.length cs.length + 3h:HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs)) r)⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs)) r) at hposinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)hclear:∀ r ≤ max bs.length cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs)) r)⊢ HeadBound width (configs (scanCfg input pos stPayloadBit pending 0 bs cs) t)
    apply headBound_succ _ ((2 * cs.length + 3) + (max bs.length cs.length + 3)) width
      hstart ?_ t (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)hclear:∀ r ≤ max bs.length cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs)) r)⊢ t ≤ 2 * cs.length + 3 + (max bs.length cs.length + 3) + 1 simp only [he, ite_true] at htinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕhb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)hclear:∀ r ≤ max bs.length cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs)) r)ht:t ≤ 2 * cs.length + max bs.length cs.length + 7⊢ t ≤ 2 * cs.length + 3 + (max bs.length cs.length + 3) + 1; omegaAll goals completed! 🐙)
    rw [hsinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)hclear:∀ r ≤ max bs.length cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs)) r)⊢ ∀ t ≤ 2 * cs.length + 3 + (max bs.length cs.length + 3),
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) t)]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)hclear:∀ r ≤ max bs.length cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs)) r)⊢ ∀ t ≤ 2 * cs.length + 3 + (max bs.length cs.length + 3),
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) t)
    apply headBound_add _ (2 * cs.length + 3) (max bs.length cs.length + 3) width hdecboundinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)hclear:∀ r ≤ max bs.length cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs)) r)⊢ ∀ t ≤ max bs.length cs.length + 3,
  HeadBound width
    (configs (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3)) t)
    rw [hdecinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)hclear:∀ r ≤ max bs.length cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs)) r)⊢ ∀ t ≤ max bs.length cs.length + 3,
  HeadBound width
    (configs (scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)) t)]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:remaining = 1hseen:(Counter.decrement cs).any id = falsehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) (2 * cs.length + 3) =
  scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)hclear:∀ r ≤ max bs.length cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) stClear pending 0 bs (Counter.decrement cs)) r)⊢ ∀ t ≤ max bs.length cs.length + 3,
  HeadBound width
    (configs (scanCfg input (moveInputPos pos 1) (afterDecrement true false) pending 0 bs (Counter.decrement cs)) t)
    exact hclearAll goals completed! 🐙
  ·neginput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:¬remaining = 1⊢ HeadBound width (configs (scanCfg input pos stPayloadBit pending 0 bs cs) t) apply headBound_succ _ (2 * cs.length + 3) width hstart ?_ t
      (byinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:¬remaining = 1⊢ t ≤ 2 * cs.length + 3 + 1 simp only [he, ite_false] at htinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕhb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:¬remaining = 1ht:t ≤ 2 * cs.length + 4⊢ t ≤ 2 * cs.length + 3 + 1; omegaAll goals completed! 🐙)
    rw [hsinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:¬remaining = 1⊢ ∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)]input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolwidth:ℕhp:0 < pendinghr:0 < remaininghc:Counter.value cs = remaininghpw:pending ≤ widthhbw:bs.length + 1 ≤ widthhcw:cs.length + 1 ≤ widthhin:(scanCfg input pos stPayloadBit pending 0 bs cs).inputSymbol = some (boolEmb b)t:ℕht:t ≤ if remaining = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4hb:∀ (q : Control), HeadBound width (scanCfg input (moveInputPos pos 1) q pending 0 bs cs)hdecbound:∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)hstart:HeadBound width (scanCfg input pos stPayloadBit pending 0 bs cs)hs:step (scanCfg input pos stPayloadBit pending 0 bs cs) =
  scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cshe:¬remaining = 1⊢ ∀ r ≤ 2 * cs.length + 3,
  HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 bs cs) r)
    exact hdecboundAll goals completed! 🐙

end Geb.BitTree.Elias.Machine