1. Geb
  2. Prototypes
  3. Computability
  4. BitTree
  5. Elias
  6. MachineHeaderBound
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

Work space throughout the delta-header macros

Appending a header bit needs one additional binary cell. The following countdown sweeps stay between their marked origin and right-hand blank. Composing these bounds controls every intermediate configuration of both header phases.

Implementation notes

These Cslib execution statements inherit Classical.choice from its input reader.

Tags

Elias delta code, Turing machine, space complexity

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

The first binary counter's decrement stays within a boundary configuration's head bound.

theorem decrement_false_scan_headBound (input : List (Fin 3)) (pos : Fin (input.length + 2)) (pending zeros : ℕ) (bs cs : List Bool) (width : ℕ) (hcfg : HeadBound width (scanCfg input pos (stDecrement false) pending zeros bs cs)) (hw : bs.length + 1 ≤ width) (hb : 0 < Counter.value bs) (t : ℕ) (ht : t ≤ 2 * bs.length + 3) : HeadBound width (machine.configs (scanCfg input pos (stDecrement false) pending zeros bs cs) t) := input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolwidth:ℕhcfg:HeadBound width (scanCfg input pos (stDecrement false) pending zeros bs cs)hw:bs.length + 1 ≤ widthhb:0 < Counter.value bst:ℕht:t ≤ 2 * bs.length + 3⊢ HeadBound width (configs (scanCfg input pos (stDecrement false) pending zeros bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolwidth:ℕhcfg:HeadBound width (scanCfg input pos (stDecrement false) pending zeros bs cs)hw:bs.length + 1 ≤ widthhb:0 < Counter.value bst:ℕht:t ≤ 2 * bs.length + 3h:HeadBound width (configs (counterCfg (scanCfg input pos (stDecrement false) pending zeros bs cs) false bs (stDecrement false) (bs.length + 1)) t)⊢ HeadBound width (configs (scanCfg input pos (stDecrement false) pending zeros bs cs) t) rwa [input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolwidth:ℕhcfg:HeadBound width (scanCfg input pos (stDecrement false) pending zeros bs cs)hw:bs.length + 1 ≤ widthhb:0 < Counter.value bst:ℕht:t ≤ 2 * bs.length + 3h:HeadBound width (configs (scanCfg input pos (stDecrement false) pending zeros bs cs) t)⊢ HeadBound width (configs (scanCfg input pos (stDecrement false) pending zeros bs cs) t)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolwidth:ℕhcfg:HeadBound width (scanCfg input pos (stDecrement false) pending zeros bs cs)hw:bs.length + 1 ≤ widthhb:0 < Counter.value bst:ℕht:t ≤ 2 * bs.length + 3h:HeadBound width (configs (scanCfg input pos (stDecrement false) pending zeros bs cs) t)⊢ HeadBound width (configs (scanCfg input pos (stDecrement false) pending zeros bs cs) t) at h

The second binary counter's decrement stays within its boundary head bound.

theorem decrement_true_scan_headBound (input : List (Fin 3)) (pos : Fin (input.length + 2)) (pending zeros : ℕ) (bs cs : List Bool) (width : ℕ) (hcfg : HeadBound width (scanCfg input pos (stDecrement true) pending zeros bs cs)) (hw : cs.length + 1 ≤ width) (hc : 0 < Counter.value cs) (t : ℕ) (ht : t ≤ 2 * cs.length + 3) : HeadBound width (machine.configs (scanCfg input pos (stDecrement true) pending zeros bs cs) t) := input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolwidth:ℕhcfg:HeadBound width (scanCfg input pos (stDecrement true) pending zeros bs cs)hw:cs.length + 1 ≤ widthhc:0 < Counter.value cst:ℕht:t ≤ 2 * cs.length + 3⊢ HeadBound width (configs (scanCfg input pos (stDecrement true) pending zeros bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolwidth:ℕhcfg:HeadBound width (scanCfg input pos (stDecrement true) pending zeros bs cs)hw:cs.length + 1 ≤ widthhc:0 < Counter.value cst:ℕht:t ≤ 2 * cs.length + 3h:HeadBound width (configs (counterCfg (scanCfg input pos (stDecrement true) pending zeros bs cs) true cs (stDecrement true) (cs.length + 1)) t)⊢ HeadBound width (configs (scanCfg input pos (stDecrement true) pending zeros bs cs) t) rwa [input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolwidth:ℕhcfg:HeadBound width (scanCfg input pos (stDecrement true) pending zeros bs cs)hw:cs.length + 1 ≤ widthhc:0 < Counter.value cst:ℕht:t ≤ 2 * cs.length + 3h:HeadBound width (configs (scanCfg input pos (stDecrement true) pending zeros bs cs) t)⊢ HeadBound width (configs (scanCfg input pos (stDecrement true) pending zeros bs cs) t)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolwidth:ℕhcfg:HeadBound width (scanCfg input pos (stDecrement true) pending zeros bs cs)hw:cs.length + 1 ≤ widthhc:0 < Counter.value cst:ℕht:t ≤ 2 * cs.length + 3h:HeadBound width (configs (scanCfg input pos (stDecrement true) pending zeros bs cs) t)⊢ HeadBound width (configs (scanCfg input pos (stDecrement true) pending zeros bs cs) t) at h

Every width-field macro prefix stays within the available unary and binary widths.

theorem configs_size_headBound (input : List (Fin 3)) (pos : Fin (input.length + 2)) (pending remaining : ℕ) (bs cs : List Bool) (b : Bool) (hr : 0 < remaining) (hb : 0 < Counter.value bs) (hin : (scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)) (width : ℕ) (hp : pending + 1 ≤ width) (hz : remaining + 1 ≤ width) (hbs : bs.length + 2 ≤ width) (hcs : cs.length + 2 ≤ width) (t : ℕ) (ht : t ≤ if remaining = 1 then 2 * bs.length + 7 else 2) : HeadBound width (machine.configs (scanCfg input pos stSizeBit pending remaining bs cs) t) := input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2⊢ HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending (remaining - 1 + 1) bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending (remaining - 1 + 1) bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs⊢ HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs⊢ HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)⊢ HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)hcheck:HeadBound width (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs)⊢ HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)hcheck:HeadBound width (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs)htwo:configs (scanCfg input pos stSizeBit pending remaining bs cs) 2 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cs⊢ HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)hcheck:HeadBound width (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs)htwo:configs (scanCfg input pos stSizeBit pending remaining bs cs) 2 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cshfirst:∀ u ≤ 2, HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) u)⊢ HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)hcheck:HeadBound width (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs)htwo:configs (scanCfg input pos stSizeBit pending remaining bs cs) 2 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cshfirst:∀ u ≤ 2, HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) u)he:remaining = 1⊢ HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) t)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)hcheck:HeadBound width (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs)htwo:configs (scanCfg input pos stSizeBit pending remaining bs cs) 2 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cshfirst:∀ u ≤ 2, HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) u)he:¬remaining = 1⊢ HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)hcheck:HeadBound width (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs)htwo:configs (scanCfg input pos stSizeBit pending remaining bs cs) 2 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cshfirst:∀ u ≤ 2, HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) u)he:remaining = 1⊢ HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)hcheck:HeadBound width (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs)htwo:configs (scanCfg input pos stSizeBit pending remaining bs cs) 2 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cshfirst:∀ u ≤ 2, HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) u)he:remaining = 1hv:0 < Counter.value (b :: bs)⊢ HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) t) apply headBound_add _ 2 (2 * (b :: bs).length + 3) width hfirst ?_ t (input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)hcheck:HeadBound width (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs)htwo:configs (scanCfg input pos stSizeBit pending remaining bs cs) 2 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cshfirst:∀ u ≤ 2, HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) u)he:remaining = 1hv:0 < Counter.value (b :: bs)⊢ t ≤ 2 + (2 * (b :: bs).length + 3) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕhs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)hcheck:HeadBound width (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs)htwo:configs (scanCfg input pos stSizeBit pending remaining bs cs) 2 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cshfirst:∀ u ≤ 2, HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) u)he:remaining = 1hv:0 < Counter.value (b :: bs)ht:t ≤ 2 * bs.length + 7⊢ t ≤ 2 + (2 * (bs.length + 1) + 3); All goals completed! 🐙) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)hcheck:HeadBound width (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs)htwo:configs (scanCfg input pos stSizeBit pending remaining bs cs) 2 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cshfirst:∀ u ≤ 2, HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) u)he:remaining = 1hv:0 < Counter.value (b :: bs)⊢ ∀ t ≤ 2 * (b :: bs).length + 3, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)hcheck:HeadBound width (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs)htwo:configs (scanCfg input pos stSizeBit pending remaining bs cs) 2 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cshfirst:∀ u ≤ 2, HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) u)he:remaining = 1hv:0 < Counter.value (b :: bs)⊢ ∀ t ≤ 2 * (b :: bs).length + 3, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 (b :: bs) cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)hcheck:HeadBound width (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs)htwo:configs (scanCfg input pos stSizeBit pending remaining bs cs) 2 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cshfirst:∀ u ≤ 2, HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) u)he:remaining = 1hv:0 < Counter.value (b :: bs)u:ℕhu:u ≤ 2 * (b :: bs).length + 3⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 (b :: bs) cs) u) exact decrement_false_scan_headBound input (moveInputPos pos 1) pending 0 (b :: bs) cs width (scanCfg_headBound input (moveInputPos pos 1) _ pending 0 (b :: bs) cs width (input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)hcheck:HeadBound width (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs)htwo:configs (scanCfg input pos stSizeBit pending remaining bs cs) 2 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cshfirst:∀ u ≤ 2, HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) u)he:remaining = 1hv:0 < Counter.value (b :: bs)u:ℕhu:u ≤ 2 * (b :: bs).length + 3⊢ pending ≤ width All goals completed! 🐙) (input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)hcheck:HeadBound width (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs)htwo:configs (scanCfg input pos stSizeBit pending remaining bs cs) 2 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cshfirst:∀ u ≤ 2, HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) u)he:remaining = 1hv:0 < Counter.value (b :: bs)u:ℕhu:u ≤ 2 * (b :: bs).length + 3⊢ 0 ≤ width All goals completed! 🐙) (input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)hcheck:HeadBound width (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs)htwo:configs (scanCfg input pos stSizeBit pending remaining bs cs) 2 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cshfirst:∀ u ≤ 2, HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) u)he:remaining = 1hv:0 < Counter.value (b :: bs)u:ℕhu:u ≤ 2 * (b :: bs).length + 3⊢ (b :: bs).length + 1 ≤ width input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)hcheck:HeadBound width (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs)htwo:configs (scanCfg input pos stSizeBit pending remaining bs cs) 2 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cshfirst:∀ u ≤ 2, HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) u)he:remaining = 1hv:0 < Counter.value (b :: bs)u:ℕhu:u ≤ 2 * (b :: bs).length + 3⊢ bs.length + 1 + 1 ≤ width; All goals completed! 🐙) (input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)hcheck:HeadBound width (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs)htwo:configs (scanCfg input pos stSizeBit pending remaining bs cs) 2 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cshfirst:∀ u ≤ 2, HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) u)he:remaining = 1hv:0 < Counter.value (b :: bs)u:ℕhu:u ≤ 2 * (b :: bs).length + 3⊢ cs.length + 1 ≤ width All goals completed! 🐙)) (input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)hcheck:HeadBound width (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs)htwo:configs (scanCfg input pos stSizeBit pending remaining bs cs) 2 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cshfirst:∀ u ≤ 2, HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) u)he:remaining = 1hv:0 < Counter.value (b :: bs)u:ℕhu:u ≤ 2 * (b :: bs).length + 3⊢ (b :: bs).length + 1 ≤ width input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)hcheck:HeadBound width (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs)htwo:configs (scanCfg input pos stSizeBit pending remaining bs cs) 2 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cshfirst:∀ u ≤ 2, HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) u)he:remaining = 1hv:0 < Counter.value (b :: bs)u:ℕhu:u ≤ 2 * (b :: bs).length + 3⊢ bs.length + 1 + 1 ≤ width; All goals completed! 🐙) hv u hu input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)hcheck:HeadBound width (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs)htwo:configs (scanCfg input pos stSizeBit pending remaining bs cs) 2 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cshfirst:∀ u ≤ 2, HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) u)he:¬remaining = 1⊢ HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) t) exact hfirst t (input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:0 < Counter.value bshin:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:remaining + 1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 7 else 2hs:(scanCfg input pos stSizeBit pending remaining bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending remaining bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cshinit:HeadBound width (scanCfg input pos stSizeBit pending remaining bs cs)hcheck:HeadBound width (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs)htwo:configs (scanCfg input pos stSizeBit pending remaining bs cs) 2 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cshfirst:∀ u ≤ 2, HeadBound width (configs (scanCfg input pos stSizeBit pending remaining bs cs) u)he:¬remaining = 1⊢ t ≤ 2 All goals completed! 🐙)

Every length-field macro prefix is bounded by word widths, regardless of decoded value.

theorem configs_length_headBound (input : List (Fin 3)) (pos : Fin (input.length + 2)) (pending remaining : ℕ) (bs cs : List Bool) (b : Bool) (hr : 0 < remaining) (hb : Counter.value bs = remaining) (hc : 0 < Counter.value cs) (hin : (scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)) (width : ℕ) (hp : pending + 1 ≤ width) (hz : 1 ≤ width) (hbs : bs.length + 2 ≤ width) (hcs : cs.length + 2 ≤ width) (t : ℕ) (ht : t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4) : HeadBound width (machine.configs (scanCfg input pos stLengthBit pending 0 bs cs) t) := input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4⊢ HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)⊢ HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))⊢ HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bs⊢ HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)⊢ HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)he:remaining = 1⊢ HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) t)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)he:¬remaining = 1⊢ HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)he:remaining = 1⊢ HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)he:remaining = 1hzero:(Counter.decrement bs).any id = false⊢ HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)he:remaining = 1hzero:(Counter.decrement bs).any id = falsehend:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)⊢ HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)he:remaining = 1hzero:(Counter.decrement bs).any id = falsehend:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)hv:0 < Counter.value (b :: cs)⊢ HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) t) apply headBound_add _ (1 + (2 * bs.length + 3)) (2 * (b :: cs).length + 3) width hfirst ?_ t (input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)he:remaining = 1hzero:(Counter.decrement bs).any id = falsehend:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)hv:0 < Counter.value (b :: cs)⊢ t ≤ 1 + (2 * bs.length + 3) + (2 * (b :: cs).length + 3) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕhinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)he:remaining = 1hzero:(Counter.decrement bs).any id = falsehend:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)hv:0 < Counter.value (b :: cs)ht:t ≤ 2 * bs.length + 2 * cs.length + 9⊢ t ≤ 1 + (2 * bs.length + 3) + (2 * (cs.length + 1) + 3); All goals completed! 🐙) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)he:remaining = 1hzero:(Counter.decrement bs).any id = falsehend:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)hv:0 < Counter.value (b :: cs)⊢ ∀ t ≤ 2 * (b :: cs).length + 3, HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)) t) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)he:remaining = 1hzero:(Counter.decrement bs).any id = falsehend:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)hv:0 < Counter.value (b :: cs)u:ℕhu:u ≤ 2 * (b :: cs).length + 3⊢ HeadBound width (configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)) u) exact decrement_true_scan_headBound input (moveInputPos pos 1) pending 0 (Counter.decrement bs) (b :: cs) width (scanCfg_headBound input (moveInputPos pos 1) _ pending 0 (Counter.decrement bs) (b :: cs) width (input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)he:remaining = 1hzero:(Counter.decrement bs).any id = falsehend:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)hv:0 < Counter.value (b :: cs)u:ℕhu:u ≤ 2 * (b :: cs).length + 3⊢ pending ≤ width All goals completed! 🐙) (input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)he:remaining = 1hzero:(Counter.decrement bs).any id = falsehend:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)hv:0 < Counter.value (b :: cs)u:ℕhu:u ≤ 2 * (b :: cs).length + 3⊢ 0 ≤ width All goals completed! 🐙) (input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)he:remaining = 1hzero:(Counter.decrement bs).any id = falsehend:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)hv:0 < Counter.value (b :: cs)u:ℕhu:u ≤ 2 * (b :: cs).length + 3⊢ (Counter.decrement bs).length + 1 ≤ width input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)he:remaining = 1hzero:(Counter.decrement bs).any id = falsehend:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)hv:0 < Counter.value (b :: cs)u:ℕhu:u ≤ 2 * (b :: cs).length + 3⊢ bs.length + 1 ≤ width; All goals completed! 🐙) (input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)he:remaining = 1hzero:(Counter.decrement bs).any id = falsehend:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)hv:0 < Counter.value (b :: cs)u:ℕhu:u ≤ 2 * (b :: cs).length + 3⊢ (b :: cs).length + 1 ≤ width input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)he:remaining = 1hzero:(Counter.decrement bs).any id = falsehend:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)hv:0 < Counter.value (b :: cs)u:ℕhu:u ≤ 2 * (b :: cs).length + 3⊢ cs.length + 1 + 1 ≤ width; All goals completed! 🐙)) (input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)he:remaining = 1hzero:(Counter.decrement bs).any id = falsehend:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)hv:0 < Counter.value (b :: cs)u:ℕhu:u ≤ 2 * (b :: cs).length + 3⊢ (b :: cs).length + 1 ≤ width input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)he:remaining = 1hzero:(Counter.decrement bs).any id = falsehend:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)hv:0 < Counter.value (b :: cs)u:ℕhu:u ≤ 2 * (b :: cs).length + 3⊢ cs.length + 1 + 1 ≤ width; All goals completed! 🐙) hv u hu input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)he:¬remaining = 1⊢ HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) t) exact hfirst t (input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕht:t ≤ if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4hinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)he:¬remaining = 1⊢ t ≤ 1 + (2 * bs.length + 3) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕremaining:ℕbs:List Boolcs:List Boolb:Boolhr:0 < remaininghb:Counter.value bs = remaininghc:0 < Counter.value cshin:(scanCfg input pos stLengthBit pending 0 bs cs).inputSymbol = some (boolEmb b)width:ℕhp:pending + 1 ≤ widthhz:1 ≤ widthhbs:bs.length + 2 ≤ widthhcs:cs.length + 2 ≤ widtht:ℕhinit:HeadBound width (scanCfg input pos stLengthBit pending 0 bs cs)hdec:HeadBound width (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs))hbpos:0 < Counter.value bshfirst:∀ u ≤ 1 + (2 * bs.length + 3), HeadBound width (configs (scanCfg input pos stLengthBit pending 0 bs cs) u)he:¬remaining = 1ht:t ≤ 2 * bs.length + 4⊢ t ≤ 1 + (2 * bs.length + 3); All goals completed! 🐙)
end Geb.BitTree.Elias.Machine