1. Geb
  2. Prototypes
  3. Computability
  4. BitTree
  5. Elias
  6. MachineBit
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 public import Geb.Prototypes.Computability.BitTree.Elias.MachineEmpty public import Geb.Prototypes.Computability.BitTree.Elias.MachinePayload public import Geb.Prototypes.Computability.BitTree.Elias.MachineSimpleBound public import Geb.Prototypes.Computability.BitTree.Elias.MachineHeaderBound
set_option doc.verso true

One complete scanner transition on the Turing machine

The read, countdown, and cleanup phases compose to exactly one transition of the scalar scanner. Its binary-word model retains the physical field widths, so the cost records every sweep even when a counter has acquired leading zeros.

Main statements

  • configs_bit proves the exact one-bit simulation and absence of output.

  • configs_bit_headBound bounds every intermediate work-head position.

Implementation notes

This module states correspondence with Cslib execution and consequently inherits Classical.choice from the input reader.

Tags

Elias delta code, Turing machine, scanner, simulation

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

Additional input after a completed tree enters or remains in the rejecting state.

theorem step_terminal (input : List (Fin 3)) (pos : Fin (input.length + 2)) (q : Control) (pending zeros : ℕ) (bs cs : List Bool) (b : Bool) (hq : q = stDone ∨ q = stDead) (hin : (scanCfg input pos q pending zeros bs cs).inputSymbol = some (boolEmb b)) : machine.step (scanCfg input pos q pending zeros bs cs) = scanCfg input (moveInputPos pos 1) stDead pending zeros bs cs := input:List (Fin 3)pos:Fin (input.length + 2)q:Controlpending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhq:q = stDone ∨ q = stDeadhin:(scanCfg input pos q pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ step (scanCfg input pos q pending zeros bs cs) = scanCfg input (moveInputPos pos 1) stDead pending zeros bs cs input:List (Fin 3)pos:Fin (input.length + 2)q:Controlpending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhq:q = stDone ∨ q = stDeadhin:(scanCfg input pos q pending zeros bs cs).inputSymbol = some (boolEmb b)hr:q = stTree ∨ q = stZeros ∨ q = stSizeBit ∨ q = stLengthBit ∨ q = stPayloadBit ∨ q = stDone ∨ q = stDead⊢ step (scanCfg input pos q pending zeros bs cs) = scanCfg input (moveInputPos pos 1) stDead pending zeros bs cs input:List (Fin 3)pos:Fin (input.length + 2)q:Controlpending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhq:q = stDone ∨ q = stDeadhin:(scanCfg input pos q pending zeros bs cs).inputSymbol = some (boolEmb b)hr:q = stTree ∨ q = stZeros ∨ q = stSizeBit ∨ q = stLengthBit ∨ q = stPayloadBit ∨ q = stDone ∨ q = stDead⊢ { state := (read q (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos q pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read q (boolEmb b)).workActions i).1 with | none => (scanCfg input pos q pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos q pending zeros bs cs).workTapes i) ((scanCfg input pos q pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos q pending zeros bs cs).workTapePos i + ↑((read q (boolEmb b)).workActions i).2 } = scanCfg input (moveInputPos pos 1) stDead pending zeros bs cs input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stDone pending zeros bs cs).inputSymbol = some (boolEmb b)hr:stDone = stTree ∨ stDone = stZeros ∨ stDone = stSizeBit ∨ stDone = stLengthBit ∨ stDone = stPayloadBit ∨ stDone = stDone ∨ stDone = stDead⊢ { state := (read stDone (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stDone pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stDone pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stDone pending zeros bs cs).workTapes i) ((scanCfg input pos stDone pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stDone pending zeros bs cs).workTapePos i + ↑((read stDone (boolEmb b)).workActions i).2 } = scanCfg input (moveInputPos pos 1) stDead pending zeros bs csinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stDead pending zeros bs cs).inputSymbol = some (boolEmb b)hr:stDead = stTree ∨ stDead = stZeros ∨ stDead = stSizeBit ∨ stDead = stLengthBit ∨ stDead = stPayloadBit ∨ stDead = stDone ∨ stDead = stDead⊢ { state := (read stDead (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stDead pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stDead pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stDead pending zeros bs cs).workTapes i) ((scanCfg input pos stDead pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stDead pending zeros bs cs).workTapePos i + ↑((read stDead (boolEmb b)).workActions i).2 } = scanCfg input (moveInputPos pos 1) stDead pending zeros bs cs input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stDone pending zeros bs cs).inputSymbol = some (boolEmb b)hr:stDone = stTree ∨ stDone = stZeros ∨ stDone = stSizeBit ∨ stDone = stLengthBit ∨ stDone = stPayloadBit ∨ stDone = stDone ∨ stDone = stDead⊢ { state := (read stDone (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stDone pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stDone pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stDone pending zeros bs cs).workTapes i) ((scanCfg input pos stDone pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stDone pending zeros bs cs).workTapePos i + ↑((read stDone (boolEmb b)).workActions i).2 } = scanCfg input (moveInputPos pos 1) stDead pending zeros bs csinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stDead pending zeros bs cs).inputSymbol = some (boolEmb b)hr:stDead = stTree ∨ stDead = stZeros ∨ stDead = stSizeBit ∨ stDead = stLengthBit ∨ stDead = stPayloadBit ∨ stDead = stDone ∨ stDead = stDead⊢ { state := (read stDead (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stDead pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stDead pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stDead pending zeros bs cs).workTapes i) ((scanCfg input pos stDead pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stDead pending zeros bs cs).workTapePos i + ↑((read stDead (boolEmb b)).workActions i).2 } = scanCfg input (moveInputPos pos 1) stDead pending zeros bs cs input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stDead pending zeros bs cs).inputSymbol = some (boolEmb b)hr:stDead = stTree ∨ stDead = stZeros ∨ stDead = stSizeBit ∨ stDead = stLengthBit ∨ stDead = stPayloadBit ∨ stDead = stDone ∨ stDead = stDead⊢ { state := (read stDead (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stDead pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stDead pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stDead pending zeros bs cs).workTapes i) ((scanCfg input pos stDead pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stDead pending zeros bs cs).workTapePos i + ↑((read stDead (boolEmb b)).workActions i).2 }.workTapePos = (scanCfg input (moveInputPos pos 1) stDead pending zeros bs cs).workTapePos all_goals input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stDead pending zeros bs cs).inputSymbol = some (boolEmb b)hr:stDead = stTree ∨ stDead = stZeros ∨ stDead = stSizeBit ∨ stDead = stLengthBit ∨ stDead = stPayloadBit ∨ stDead = stDone ∨ stDead = stDeadi:Fin 4⊢ { state := (read stDead (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stDead pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stDead pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stDead pending zeros bs cs).workTapes i) ((scanCfg input pos stDead pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stDead pending zeros bs cs).workTapePos i + ↑((read stDead (boolEmb b)).workActions i).2 }.workTapePos i = (scanCfg input (moveInputPos pos 1) stDead pending zeros bs cs).workTapePos i input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stDead pending zeros bs cs).inputSymbol = some (boolEmb b)hr:stDead = stTree ∨ stDead = stZeros ∨ stDead = stSizeBit ∨ stDead = stLengthBit ∨ stDead = stPayloadBit ∨ stDead = stDone ∨ stDead = stDeadi:Fin 4⊢ (scanCfg input pos stDead pending zeros bs cs).workTapePos i + 0 = (scanCfg input (moveInputPos pos 1) stDead pending zeros bs cs).workTapePos i All goals completed! 🐙

A nonempty unary prefix enters the width-field reader after its first one.

theorem configs_zeros_positive (input : List (Fin 3)) (pos : Fin (input.length + 2)) (pending zeros : ℕ) (hz : 0 < zeros) (hin : (scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)) : machine.configs (scanCfg input pos stZeros pending zeros [] [true]) 2 = scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true] ∧ machine.outputString (scanCfg input pos stZeros pending zeros [] [true]) 2 = [] := input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕhz:0 < zeroshin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)⊢ configs (scanCfg input pos stZeros pending zeros [] [true]) 2 = scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true] ∧ machine.outputString (scanCfg input pos stZeros pending zeros [] [true]) 2 = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕhz:0 < zeroshin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)hs:step (scanCfg input pos stZeros pending zeros [] [true]) = if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true] else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) [] [true]⊢ configs (scanCfg input pos stZeros pending zeros [] [true]) 2 = scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true] ∧ machine.outputString (scanCfg input pos stZeros pending zeros [] [true]) 2 = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕhz:0 < zeroshin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)hs:step (scanCfg input pos stZeros pending zeros [] [true]) = scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]⊢ configs (scanCfg input pos stZeros pending zeros [] [true]) 2 = scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true] ∧ machine.outputString (scanCfg input pos stZeros pending zeros [] [true]) 2 = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕhz:0 < zeroshin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)hs:step (scanCfg input pos stZeros pending zeros [] [true]) = scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]hread:configs (scanCfg input pos stZeros pending zeros [] [true]) 1 = scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true] ∧ machine.outputString (scanCfg input pos stZeros pending zeros [] [true]) 1 = []⊢ configs (scanCfg input pos stZeros pending zeros [] [true]) 2 = scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true] ∧ machine.outputString (scanCfg input pos stZeros pending zeros [] [true]) 2 = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕhz:0 < zeroshin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)hs:step (scanCfg input pos stZeros pending zeros [] [true]) = scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]hread:configs (scanCfg input pos stZeros pending zeros [] [true]) 1 = scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true] ∧ machine.outputString (scanCfg input pos stZeros pending zeros [] [true]) 1 = []hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]) = scanCfg input (moveInputPos pos 1) (if zeros = 0 then stDecrement false else stSizeBit) pending zeros [true] [true]⊢ configs (scanCfg input pos stZeros pending zeros [] [true]) 2 = scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true] ∧ machine.outputString (scanCfg input pos stZeros pending zeros [] [true]) 2 = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕhz:0 < zeroshin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)hs:step (scanCfg input pos stZeros pending zeros [] [true]) = scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]hread:configs (scanCfg input pos stZeros pending zeros [] [true]) 1 = scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true] ∧ machine.outputString (scanCfg input pos stZeros pending zeros [] [true]) 1 = []hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]) = scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true]⊢ configs (scanCfg input pos stZeros pending zeros [] [true]) 2 = scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true] ∧ machine.outputString (scanCfg input pos stZeros pending zeros [] [true]) 2 = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕhz:0 < zeroshin:(scanCfg input pos stZeros pending zeros [] [true]).inputSymbol = some (boolEmb true)hs:step (scanCfg input pos stZeros pending zeros [] [true]) = scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]hread:configs (scanCfg input pos stZeros pending zeros [] [true]) 1 = scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true] ∧ machine.outputString (scanCfg input pos stZeros pending zeros [] [true]) 1 = []hc:step (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]) = scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true]hcheck:configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]) 1 = scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true] ∧ machine.outputString (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true]) 1 = []⊢ configs (scanCfg input pos stZeros pending zeros [] [true]) 2 = scanCfg input (moveInputPos pos 1) stSizeBit pending zeros [true] [true] ∧ machine.outputString (scanCfg input pos stZeros pending zeros [] [true]) 2 = [] All goals completed! 🐙

Every complete one-bit macro realizes the scalar scanner transition at its exact cost.

theorem configs_bit (input : List (Fin 3)) (pos : Fin (input.length + 2)) (s : Scanner.State) (bs cs : List Bool) (b : Bool) (hs : Scanner.Active s) (hw : Words s.1 bs cs) (hin : (modelCfg input pos s bs cs).inputSymbol = some (boolEmb b)) : machine.configs (modelCfg input pos s bs cs) (bitCost s.1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step s b) (nextWords s.1 bs cs b).1 (nextWords s.1 bs cs b).2 ∧ machine.outputString (modelCfg input pos s bs cs) (bitCost s.1 bs cs b) = [] := input:List (Fin 3)pos:Fin (input.length + 2)s:Scanner.Statebs:List Boolcs:List Boolb:Boolhs:Scanner.Active shw:Words s.1 bs cshin:(modelCfg input pos s bs cs).inputSymbol = some (boolEmb b)⊢ configs (modelCfg input pos s bs cs) (bitCost s.1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step s b) (nextWords s.1 bs cs b).1 (nextWords s.1 bs cs b).2 ∧ machine.outputString (modelCfg input pos s bs cs) (bitCost s.1 bs cs b) = [] input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolm:Scanner.Modepending:ℕhs:Scanner.Active (m, pending)hw:Words (m, pending).1 bs cshin:(modelCfg input pos (m, pending) bs cs).inputSymbol = some (boolEmb b)⊢ configs (modelCfg input pos (m, pending) bs cs) (bitCost (m, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (m, pending) b) (nextWords (m, pending).1 bs cs b).1 (nextWords (m, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (m, pending) bs cs) (bitCost (m, pending).1 bs cs b) = [] cases m with input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕhs:Scanner.Active (Scanner.Mode.tree, pending)hw:Words (Scanner.Mode.tree, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.tree, pending) bs cs).inputSymbol = some (boolEmb b)⊢ configs (modelCfg input pos (Scanner.Mode.tree, pending) bs cs) (bitCost (Scanner.Mode.tree, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.tree, pending) b) (nextWords (Scanner.Mode.tree, pending).1 bs cs b).1 (nextWords (Scanner.Mode.tree, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.tree, pending) bs cs) (bitCost (Scanner.Mode.tree, pending).1 bs cs b) = [] input:List (Fin 3)pos:Fin (input.length + 2)b:Boolpending:ℕhs:Scanner.Active (Scanner.Mode.tree, pending)hin:(modelCfg input pos (Scanner.Mode.tree, pending) [] []).inputSymbol = some (boolEmb b)⊢ configs (modelCfg input pos (Scanner.Mode.tree, pending) [] []) (bitCost (Scanner.Mode.tree, pending).1 [] [] b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.tree, pending) b) (nextWords (Scanner.Mode.tree, pending).1 [] [] b).1 (nextWords (Scanner.Mode.tree, pending).1 [] [] b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.tree, pending) [] []) (bitCost (Scanner.Mode.tree, pending).1 [] [] b) = [] input:List (Fin 3)pos:Fin (input.length + 2)b:Boolpending:ℕhs:Scanner.Active (Scanner.Mode.tree, pending)hin:(modelCfg input pos (Scanner.Mode.tree, pending) [] []).inputSymbol = some (boolEmb b)h:(configs (scanCfg input pos stTree pending 0 [] []) 1 = if b = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) 0 [] [] else scanCfg input (moveInputPos pos 1) stZeros pending 0 [] [true]) ∧ machine.outputString (scanCfg input pos stTree pending 0 [] []) 1 = []⊢ configs (modelCfg input pos (Scanner.Mode.tree, pending) [] []) (bitCost (Scanner.Mode.tree, pending).1 [] [] b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.tree, pending) b) (nextWords (Scanner.Mode.tree, pending).1 [] [] b).1 (nextWords (Scanner.Mode.tree, pending).1 [] [] b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.tree, pending) [] []) (bitCost (Scanner.Mode.tree, pending).1 [] [] b) = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhs:Scanner.Active (Scanner.Mode.tree, pending)hin:(modelCfg input pos (Scanner.Mode.tree, pending) [] []).inputSymbol = some (boolEmb false)h:(configs (scanCfg input pos stTree pending 0 [] []) 1 = if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) 0 [] [] else scanCfg input (moveInputPos pos 1) stZeros pending 0 [] [true]) ∧ machine.outputString (scanCfg input pos stTree pending 0 [] []) 1 = []⊢ configs (modelCfg input pos (Scanner.Mode.tree, pending) [] []) (bitCost (Scanner.Mode.tree, pending).1 [] [] false) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.tree, pending) false) (nextWords (Scanner.Mode.tree, pending).1 [] [] false).1 (nextWords (Scanner.Mode.tree, pending).1 [] [] false).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.tree, pending) [] []) (bitCost (Scanner.Mode.tree, pending).1 [] [] false) = []input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhs:Scanner.Active (Scanner.Mode.tree, pending)hin:(modelCfg input pos (Scanner.Mode.tree, pending) [] []).inputSymbol = some (boolEmb true)h:(configs (scanCfg input pos stTree pending 0 [] []) 1 = if true = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) 0 [] [] else scanCfg input (moveInputPos pos 1) stZeros pending 0 [] [true]) ∧ machine.outputString (scanCfg input pos stTree pending 0 [] []) 1 = []⊢ configs (modelCfg input pos (Scanner.Mode.tree, pending) [] []) (bitCost (Scanner.Mode.tree, pending).1 [] [] true) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.tree, pending) true) (nextWords (Scanner.Mode.tree, pending).1 [] [] true).1 (nextWords (Scanner.Mode.tree, pending).1 [] [] true).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.tree, pending) [] []) (bitCost (Scanner.Mode.tree, pending).1 [] [] true) = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhs:Scanner.Active (Scanner.Mode.tree, pending)hin:(modelCfg input pos (Scanner.Mode.tree, pending) [] []).inputSymbol = some (boolEmb false)h:(configs (scanCfg input pos stTree pending 0 [] []) 1 = if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) 0 [] [] else scanCfg input (moveInputPos pos 1) stZeros pending 0 [] [true]) ∧ machine.outputString (scanCfg input pos stTree pending 0 [] []) 1 = []⊢ configs (modelCfg input pos (Scanner.Mode.tree, pending) [] []) (bitCost (Scanner.Mode.tree, pending).1 [] [] false) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.tree, pending) false) (nextWords (Scanner.Mode.tree, pending).1 [] [] false).1 (nextWords (Scanner.Mode.tree, pending).1 [] [] false).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.tree, pending) [] []) (bitCost (Scanner.Mode.tree, pending).1 [] [] false) = []input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhs:Scanner.Active (Scanner.Mode.tree, pending)hin:(modelCfg input pos (Scanner.Mode.tree, pending) [] []).inputSymbol = some (boolEmb true)h:(configs (scanCfg input pos stTree pending 0 [] []) 1 = if true = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) 0 [] [] else scanCfg input (moveInputPos pos 1) stZeros pending 0 [] [true]) ∧ machine.outputString (scanCfg input pos stTree pending 0 [] []) 1 = []⊢ configs (modelCfg input pos (Scanner.Mode.tree, pending) [] []) (bitCost (Scanner.Mode.tree, pending).1 [] [] true) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.tree, pending) true) (nextWords (Scanner.Mode.tree, pending).1 [] [] true).1 (nextWords (Scanner.Mode.tree, pending).1 [] [] true).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.tree, pending) [] []) (bitCost (Scanner.Mode.tree, pending).1 [] [] true) = [] All goals completed! 🐙 input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hw:Words (Scanner.Mode.zeros zeros, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) bs cs).inputSymbol = some (boolEmb b)⊢ configs (modelCfg input pos (Scanner.Mode.zeros zeros, pending) bs cs) (bitCost (Scanner.Mode.zeros zeros, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.zeros zeros, pending) b) (nextWords (Scanner.Mode.zeros zeros, pending).1 bs cs b).1 (nextWords (Scanner.Mode.zeros zeros, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.zeros zeros, pending) bs cs) (bitCost (Scanner.Mode.zeros zeros, pending).1 bs cs b) = [] input:List (Fin 3)pos:Fin (input.length + 2)b:Boolpending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb b)⊢ configs (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) (bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.zeros zeros, pending) b) (nextWords (Scanner.Mode.zeros zeros, pending).1 [] [true] b).1 (nextWords (Scanner.Mode.zeros zeros, pending).1 [] [true] b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) (bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] b) = [] cases b with input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb false)⊢ configs (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) (bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] false) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.zeros zeros, pending) false) (nextWords (Scanner.Mode.zeros zeros, pending).1 [] [true] false).1 (nextWords (Scanner.Mode.zeros zeros, pending).1 [] [true] false).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) (bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] false) = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb false)h:(configs (scanCfg input pos stZeros pending zeros [] [true]) 1 = if false = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros [true] [true] else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) [] [true]) ∧ machine.outputString (scanCfg input pos stZeros pending zeros [] [true]) 1 = []⊢ configs (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) (bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] false) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.zeros zeros, pending) false) (nextWords (Scanner.Mode.zeros zeros, pending).1 [] [true] false).1 (nextWords (Scanner.Mode.zeros zeros, pending).1 [] [true] false).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) (bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] false) = [] All goals completed! 🐙 input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb true)⊢ configs (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) (bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] true) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.zeros zeros, pending) true) (nextWords (Scanner.Mode.zeros zeros, pending).1 [] [true] true).1 (nextWords (Scanner.Mode.zeros zeros, pending).1 [] [true] true).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) (bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] true) = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb true)hz:zeros = 0⊢ configs (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) (bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] true) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.zeros zeros, pending) true) (nextWords (Scanner.Mode.zeros zeros, pending).1 [] [true] true).1 (nextWords (Scanner.Mode.zeros zeros, pending).1 [] [true] true).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) (bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] true) = []input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb true)hz:¬zeros = 0⊢ configs (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) (bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] true) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.zeros zeros, pending) true) (nextWords (Scanner.Mode.zeros zeros, pending).1 [] [true] true).1 (nextWords (Scanner.Mode.zeros zeros, pending).1 [] [true] true).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) (bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] true) = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb true)hz:zeros = 0⊢ configs (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) (bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] true) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.zeros zeros, pending) true) (nextWords (Scanner.Mode.zeros zeros, pending).1 [] [true] true).1 (nextWords (Scanner.Mode.zeros zeros, pending).1 [] [true] true).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) (bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] true) = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕhs:Scanner.Active (Scanner.Mode.zeros 0, pending)hin:(modelCfg input pos (Scanner.Mode.zeros 0, pending) [] [true]).inputSymbol = some (boolEmb true)⊢ configs (modelCfg input pos (Scanner.Mode.zeros 0, pending) [] [true]) (bitCost (Scanner.Mode.zeros 0, pending).1 [] [true] true) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.zeros 0, pending) true) (nextWords (Scanner.Mode.zeros 0, pending).1 [] [true] true).1 (nextWords (Scanner.Mode.zeros 0, pending).1 [] [true] true).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.zeros 0, pending) [] [true]) (bitCost (Scanner.Mode.zeros 0, pending).1 [] [true] true) = [] All goals completed! 🐙 input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb true)hz:¬zeros = 0⊢ configs (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) (bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] true) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.zeros zeros, pending) true) (nextWords (Scanner.Mode.zeros zeros, pending).1 [] [true] true).1 (nextWords (Scanner.Mode.zeros zeros, pending).1 [] [true] true).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) (bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] true) = [] simpa only [Scanner.step, nextWords, bitCost, modelCfg, modeState, zeroCount, hz, ↓reduceIte] using configs_zeros_positive input pos pending zeros (input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb true)hz:¬zeros = 0⊢ 0 < zeros All goals completed! 🐙) hin input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕremaining:ℕv:ℕhs:Scanner.Active (Scanner.Mode.size remaining v, pending)hw:Words (Scanner.Mode.size remaining v, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs).inputSymbol = some (boolEmb b)⊢ configs (modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs) (bitCost (Scanner.Mode.size remaining v, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.size remaining v, pending) b) (nextWords (Scanner.Mode.size remaining v, pending).1 bs cs b).1 (nextWords (Scanner.Mode.size remaining v, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs) (bitCost (Scanner.Mode.size remaining v, pending).1 bs cs b) = [] input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕremaining:ℕv:ℕhs:Scanner.Active (Scanner.Mode.size remaining v, pending)hw:Words (Scanner.Mode.size remaining v, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs).inputSymbol = some (boolEmb b)h:configs (scanCfg input pos stSizeBit pending remaining bs cs) (if remaining = 1 then 2 * bs.length + 7 else 2) = scanCfg input (moveInputPos pos 1) (if remaining = 1 then stLengthBit else stSizeBit) pending (remaining - 1) (if remaining = 1 then Counter.decrement (b :: bs) else b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending remaining bs cs) (if remaining = 1 then 2 * bs.length + 7 else 2) = []⊢ configs (modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs) (bitCost (Scanner.Mode.size remaining v, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.size remaining v, pending) b) (nextWords (Scanner.Mode.size remaining v, pending).1 bs cs b).1 (nextWords (Scanner.Mode.size remaining v, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs) (bitCost (Scanner.Mode.size remaining v, pending).1 bs cs b) = [] input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕremaining:ℕv:ℕhs:Scanner.Active (Scanner.Mode.size remaining v, pending)hw:Words (Scanner.Mode.size remaining v, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs).inputSymbol = some (boolEmb b)h:configs (scanCfg input pos stSizeBit pending remaining bs cs) (if remaining = 1 then 2 * bs.length + 7 else 2) = scanCfg input (moveInputPos pos 1) (if remaining = 1 then stLengthBit else stSizeBit) pending (remaining - 1) (if remaining = 1 then Counter.decrement (b :: bs) else b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending remaining bs cs) (if remaining = 1 then 2 * bs.length + 7 else 2) = []he:remaining = 1⊢ configs (modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs) (bitCost (Scanner.Mode.size remaining v, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.size remaining v, pending) b) (nextWords (Scanner.Mode.size remaining v, pending).1 bs cs b).1 (nextWords (Scanner.Mode.size remaining v, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs) (bitCost (Scanner.Mode.size remaining v, pending).1 bs cs b) = []input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕremaining:ℕv:ℕhs:Scanner.Active (Scanner.Mode.size remaining v, pending)hw:Words (Scanner.Mode.size remaining v, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs).inputSymbol = some (boolEmb b)h:configs (scanCfg input pos stSizeBit pending remaining bs cs) (if remaining = 1 then 2 * bs.length + 7 else 2) = scanCfg input (moveInputPos pos 1) (if remaining = 1 then stLengthBit else stSizeBit) pending (remaining - 1) (if remaining = 1 then Counter.decrement (b :: bs) else b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending remaining bs cs) (if remaining = 1 then 2 * bs.length + 7 else 2) = []he:¬remaining = 1⊢ configs (modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs) (bitCost (Scanner.Mode.size remaining v, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.size remaining v, pending) b) (nextWords (Scanner.Mode.size remaining v, pending).1 bs cs b).1 (nextWords (Scanner.Mode.size remaining v, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs) (bitCost (Scanner.Mode.size remaining v, pending).1 bs cs b) = [] input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕremaining:ℕv:ℕhs:Scanner.Active (Scanner.Mode.size remaining v, pending)hw:Words (Scanner.Mode.size remaining v, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs).inputSymbol = some (boolEmb b)h:configs (scanCfg input pos stSizeBit pending remaining bs cs) (if remaining = 1 then 2 * bs.length + 7 else 2) = scanCfg input (moveInputPos pos 1) (if remaining = 1 then stLengthBit else stSizeBit) pending (remaining - 1) (if remaining = 1 then Counter.decrement (b :: bs) else b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending remaining bs cs) (if remaining = 1 then 2 * bs.length + 7 else 2) = []he:remaining = 1⊢ configs (modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs) (bitCost (Scanner.Mode.size remaining v, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.size remaining v, pending) b) (nextWords (Scanner.Mode.size remaining v, pending).1 bs cs b).1 (nextWords (Scanner.Mode.size remaining v, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs) (bitCost (Scanner.Mode.size remaining v, pending).1 bs cs b) = []input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕremaining:ℕv:ℕhs:Scanner.Active (Scanner.Mode.size remaining v, pending)hw:Words (Scanner.Mode.size remaining v, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs).inputSymbol = some (boolEmb b)h:configs (scanCfg input pos stSizeBit pending remaining bs cs) (if remaining = 1 then 2 * bs.length + 7 else 2) = scanCfg input (moveInputPos pos 1) (if remaining = 1 then stLengthBit else stSizeBit) pending (remaining - 1) (if remaining = 1 then Counter.decrement (b :: bs) else b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending remaining bs cs) (if remaining = 1 then 2 * bs.length + 7 else 2) = []he:¬remaining = 1⊢ configs (modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs) (bitCost (Scanner.Mode.size remaining v, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.size remaining v, pending) b) (nextWords (Scanner.Mode.size remaining v, pending).1 bs cs b).1 (nextWords (Scanner.Mode.size remaining v, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs) (bitCost (Scanner.Mode.size remaining v, pending).1 bs cs b) = [] All goals completed! 🐙 input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕremaining:ℕv:ℕhs:Scanner.Active (Scanner.Mode.length remaining v, pending)hw:Words (Scanner.Mode.length remaining v, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs).inputSymbol = some (boolEmb b)⊢ configs (modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs) (bitCost (Scanner.Mode.length remaining v, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.length remaining v, pending) b) (nextWords (Scanner.Mode.length remaining v, pending).1 bs cs b).1 (nextWords (Scanner.Mode.length remaining v, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs) (bitCost (Scanner.Mode.length remaining v, pending).1 bs cs b) = [] input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕremaining:ℕv:ℕhs:Scanner.Active (Scanner.Mode.length remaining v, pending)hw:Words (Scanner.Mode.length remaining v, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs).inputSymbol = some (boolEmb b)h:configs (scanCfg input pos stLengthBit pending 0 bs cs) (if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4) = scanCfg input (moveInputPos pos 1) (if remaining = 1 then stPayloadBit else stLengthBit) pending 0 (Counter.decrement bs) (if remaining = 1 then Counter.decrement (b :: cs) else b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) (if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4) = []⊢ configs (modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs) (bitCost (Scanner.Mode.length remaining v, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.length remaining v, pending) b) (nextWords (Scanner.Mode.length remaining v, pending).1 bs cs b).1 (nextWords (Scanner.Mode.length remaining v, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs) (bitCost (Scanner.Mode.length remaining v, pending).1 bs cs b) = [] input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕremaining:ℕv:ℕhs:Scanner.Active (Scanner.Mode.length remaining v, pending)hw:Words (Scanner.Mode.length remaining v, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs).inputSymbol = some (boolEmb b)h:configs (scanCfg input pos stLengthBit pending 0 bs cs) (if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4) = scanCfg input (moveInputPos pos 1) (if remaining = 1 then stPayloadBit else stLengthBit) pending 0 (Counter.decrement bs) (if remaining = 1 then Counter.decrement (b :: cs) else b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) (if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4) = []he:remaining = 1⊢ configs (modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs) (bitCost (Scanner.Mode.length remaining v, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.length remaining v, pending) b) (nextWords (Scanner.Mode.length remaining v, pending).1 bs cs b).1 (nextWords (Scanner.Mode.length remaining v, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs) (bitCost (Scanner.Mode.length remaining v, pending).1 bs cs b) = []input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕremaining:ℕv:ℕhs:Scanner.Active (Scanner.Mode.length remaining v, pending)hw:Words (Scanner.Mode.length remaining v, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs).inputSymbol = some (boolEmb b)h:configs (scanCfg input pos stLengthBit pending 0 bs cs) (if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4) = scanCfg input (moveInputPos pos 1) (if remaining = 1 then stPayloadBit else stLengthBit) pending 0 (Counter.decrement bs) (if remaining = 1 then Counter.decrement (b :: cs) else b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) (if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4) = []he:¬remaining = 1⊢ configs (modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs) (bitCost (Scanner.Mode.length remaining v, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.length remaining v, pending) b) (nextWords (Scanner.Mode.length remaining v, pending).1 bs cs b).1 (nextWords (Scanner.Mode.length remaining v, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs) (bitCost (Scanner.Mode.length remaining v, pending).1 bs cs b) = [] input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕremaining:ℕv:ℕhs:Scanner.Active (Scanner.Mode.length remaining v, pending)hw:Words (Scanner.Mode.length remaining v, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs).inputSymbol = some (boolEmb b)h:configs (scanCfg input pos stLengthBit pending 0 bs cs) (if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4) = scanCfg input (moveInputPos pos 1) (if remaining = 1 then stPayloadBit else stLengthBit) pending 0 (Counter.decrement bs) (if remaining = 1 then Counter.decrement (b :: cs) else b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) (if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4) = []he:remaining = 1⊢ configs (modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs) (bitCost (Scanner.Mode.length remaining v, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.length remaining v, pending) b) (nextWords (Scanner.Mode.length remaining v, pending).1 bs cs b).1 (nextWords (Scanner.Mode.length remaining v, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs) (bitCost (Scanner.Mode.length remaining v, pending).1 bs cs b) = []input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕremaining:ℕv:ℕhs:Scanner.Active (Scanner.Mode.length remaining v, pending)hw:Words (Scanner.Mode.length remaining v, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs).inputSymbol = some (boolEmb b)h:configs (scanCfg input pos stLengthBit pending 0 bs cs) (if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4) = scanCfg input (moveInputPos pos 1) (if remaining = 1 then stPayloadBit else stLengthBit) pending 0 (Counter.decrement bs) (if remaining = 1 then Counter.decrement (b :: cs) else b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) (if remaining = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4) = []he:¬remaining = 1⊢ configs (modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs) (bitCost (Scanner.Mode.length remaining v, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.length remaining v, pending) b) (nextWords (Scanner.Mode.length remaining v, pending).1 bs cs b).1 (nextWords (Scanner.Mode.length remaining v, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs) (bitCost (Scanner.Mode.length remaining v, pending).1 bs cs b) = [] All goals completed! 🐙 input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕremaining:ℕhs:Scanner.Active (Scanner.Mode.payload remaining, pending)hw:Words (Scanner.Mode.payload remaining, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs).inputSymbol = some (boolEmb b)⊢ configs (modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs) (bitCost (Scanner.Mode.payload remaining, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.payload remaining, pending) b) (nextWords (Scanner.Mode.payload remaining, pending).1 bs cs b).1 (nextWords (Scanner.Mode.payload remaining, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs) (bitCost (Scanner.Mode.payload remaining, pending).1 bs cs b) = [] input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕremaining:ℕhs:Scanner.Active (Scanner.Mode.payload remaining, pending)hw:Words (Scanner.Mode.payload remaining, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs).inputSymbol = some (boolEmb b)h:(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) = []⊢ configs (modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs) (bitCost (Scanner.Mode.payload remaining, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.payload remaining, pending) b) (nextWords (Scanner.Mode.payload remaining, pending).1 bs cs b).1 (nextWords (Scanner.Mode.payload remaining, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs) (bitCost (Scanner.Mode.payload remaining, pending).1 bs cs b) = [] input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕremaining:ℕhs:Scanner.Active (Scanner.Mode.payload remaining, pending)hw:Words (Scanner.Mode.payload remaining, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs).inputSymbol = some (boolEmb b)h:(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) = []he:remaining = 1⊢ configs (modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs) (bitCost (Scanner.Mode.payload remaining, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.payload remaining, pending) b) (nextWords (Scanner.Mode.payload remaining, pending).1 bs cs b).1 (nextWords (Scanner.Mode.payload remaining, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs) (bitCost (Scanner.Mode.payload remaining, pending).1 bs cs b) = []input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕremaining:ℕhs:Scanner.Active (Scanner.Mode.payload remaining, pending)hw:Words (Scanner.Mode.payload remaining, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs).inputSymbol = some (boolEmb b)h:(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) = []he:¬remaining = 1⊢ configs (modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs) (bitCost (Scanner.Mode.payload remaining, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.payload remaining, pending) b) (nextWords (Scanner.Mode.payload remaining, pending).1 bs cs b).1 (nextWords (Scanner.Mode.payload remaining, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs) (bitCost (Scanner.Mode.payload remaining, pending).1 bs cs b) = [] input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕremaining:ℕhs:Scanner.Active (Scanner.Mode.payload remaining, pending)hw:Words (Scanner.Mode.payload remaining, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs).inputSymbol = some (boolEmb b)h:(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) = []he:remaining = 1⊢ configs (modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs) (bitCost (Scanner.Mode.payload remaining, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.payload remaining, pending) b) (nextWords (Scanner.Mode.payload remaining, pending).1 bs cs b).1 (nextWords (Scanner.Mode.payload remaining, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs) (bitCost (Scanner.Mode.payload remaining, pending).1 bs cs b) = []input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕremaining:ℕhs:Scanner.Active (Scanner.Mode.payload remaining, pending)hw:Words (Scanner.Mode.payload remaining, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs).inputSymbol = some (boolEmb b)h:(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) = []he:¬remaining = 1⊢ configs (modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs) (bitCost (Scanner.Mode.payload remaining, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.payload remaining, pending) b) (nextWords (Scanner.Mode.payload remaining, pending).1 bs cs b).1 (nextWords (Scanner.Mode.payload remaining, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs) (bitCost (Scanner.Mode.payload remaining, pending).1 bs cs b) = [] All goals completed! 🐙 input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕhs:Scanner.Active (Scanner.Mode.done, pending)hw:Words (Scanner.Mode.done, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.done, pending) bs cs).inputSymbol = some (boolEmb b)⊢ configs (modelCfg input pos (Scanner.Mode.done, pending) bs cs) (bitCost (Scanner.Mode.done, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.done, pending) b) (nextWords (Scanner.Mode.done, pending).1 bs cs b).1 (nextWords (Scanner.Mode.done, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.done, pending) bs cs) (bitCost (Scanner.Mode.done, pending).1 bs cs b) = [] input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕhs:Scanner.Active (Scanner.Mode.done, pending)hw:Words (Scanner.Mode.done, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.done, pending) bs cs).inputSymbol = some (boolEmb b)h:configs (scanCfg input pos stDone pending 0 bs cs) 1 = scanCfg input (moveInputPos pos 1) stDead pending 0 bs cs ∧ machine.outputString (scanCfg input pos stDone pending 0 bs cs) 1 = []⊢ configs (modelCfg input pos (Scanner.Mode.done, pending) bs cs) (bitCost (Scanner.Mode.done, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.done, pending) b) (nextWords (Scanner.Mode.done, pending).1 bs cs b).1 (nextWords (Scanner.Mode.done, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.done, pending) bs cs) (bitCost (Scanner.Mode.done, pending).1 bs cs b) = [] All goals completed! 🐙 input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕhs:Scanner.Active (Scanner.Mode.dead, pending)hw:Words (Scanner.Mode.dead, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.dead, pending) bs cs).inputSymbol = some (boolEmb b)⊢ configs (modelCfg input pos (Scanner.Mode.dead, pending) bs cs) (bitCost (Scanner.Mode.dead, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.dead, pending) b) (nextWords (Scanner.Mode.dead, pending).1 bs cs b).1 (nextWords (Scanner.Mode.dead, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.dead, pending) bs cs) (bitCost (Scanner.Mode.dead, pending).1 bs cs b) = [] input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolpending:ℕhs:Scanner.Active (Scanner.Mode.dead, pending)hw:Words (Scanner.Mode.dead, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.dead, pending) bs cs).inputSymbol = some (boolEmb b)h:configs (scanCfg input pos stDead pending 0 bs cs) 1 = scanCfg input (moveInputPos pos 1) stDead pending 0 bs cs ∧ machine.outputString (scanCfg input pos stDead pending 0 bs cs) 1 = []⊢ configs (modelCfg input pos (Scanner.Mode.dead, pending) bs cs) (bitCost (Scanner.Mode.dead, pending).1 bs cs b) = modelCfg input (moveInputPos pos 1) (Scanner.step (Scanner.Mode.dead, pending) b) (nextWords (Scanner.Mode.dead, pending).1 bs cs b).1 (nextWords (Scanner.Mode.dead, pending).1 bs cs b).2 ∧ machine.outputString (modelCfg input pos (Scanner.Mode.dead, pending) bs cs) (bitCost (Scanner.Mode.dead, pending).1 bs cs b) = [] All goals completed! 🐙

One free cell beyond each growing field bounds every transition of a complete bit macro.

theorem configs_bit_headBound (input : List (Fin 3)) (pos : Fin (input.length + 2)) (s : Scanner.State) (bs cs : List Bool) (b : Bool) (hs : Scanner.Active s) (hw : Words s.1 bs cs) (hin : (modelCfg input pos s bs cs).inputSymbol = some (boolEmb b)) (width : ℕ) (hp : s.2 + 1 ≤ width) (hz : zeroCount s.1 + 1 ≤ width) (hb : bs.length + 2 ≤ width) (hc : cs.length + 2 ≤ width) (t : ℕ) (ht : t ≤ bitCost s.1 bs cs b) : HeadBound width (machine.configs (modelCfg input pos s bs cs) t) := input:List (Fin 3)pos:Fin (input.length + 2)s:Scanner.Statebs:List Boolcs:List Boolb:Boolhs:Scanner.Active shw:Words s.1 bs cshin:(modelCfg input pos s bs cs).inputSymbol = some (boolEmb b)width:ℕhp:s.2 + 1 ≤ widthhz:zeroCount s.1 + 1 ≤ widthhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕht:t ≤ bitCost s.1 bs cs b⊢ HeadBound width (configs (modelCfg input pos s bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕm:Scanner.Modepending:ℕhs:Scanner.Active (m, pending)hw:Words (m, pending).1 bs cshin:(modelCfg input pos (m, pending) bs cs).inputSymbol = some (boolEmb b)hp:(m, pending).2 + 1 ≤ widthhz:zeroCount (m, pending).1 + 1 ≤ widthht:t ≤ bitCost (m, pending).1 bs cs b⊢ HeadBound width (configs (modelCfg input pos (m, pending) bs cs) t) cases m with input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕhs:Scanner.Active (Scanner.Mode.tree, pending)hw:Words (Scanner.Mode.tree, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.tree, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.tree, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.tree, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.tree, pending).1 bs cs b⊢ HeadBound width (configs (modelCfg input pos (Scanner.Mode.tree, pending) bs cs) t) All goals completed! 🐙 input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hw:Words (Scanner.Mode.zeros zeros, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.zeros zeros, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.zeros zeros, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.zeros zeros, pending).1 bs cs b⊢ HeadBound width (configs (modelCfg input pos (Scanner.Mode.zeros zeros, pending) bs cs) t) input:List (Fin 3)pos:Fin (input.length + 2)b:Boolwidth:ℕt:ℕpending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hp:(Scanner.Mode.zeros zeros, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.zeros zeros, pending).1 + 1 ≤ widthhb:[].length + 2 ≤ widthhc:[true].length + 2 ≤ widthhin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb b)ht:t ≤ bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] b⊢ HeadBound width (configs (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) t) cases b with input:List (Fin 3)pos:Fin (input.length + 2)width:ℕt:ℕpending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hp:(Scanner.Mode.zeros zeros, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.zeros zeros, pending).1 + 1 ≤ widthhb:[].length + 2 ≤ widthhc:[true].length + 2 ≤ widthhin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb false)ht:t ≤ bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] false⊢ HeadBound width (configs (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) t) exact configs_zeros_false_headBound input pos pending zeros [] [true] width (input:List (Fin 3)pos:Fin (input.length + 2)width:ℕt:ℕpending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hp:(Scanner.Mode.zeros zeros, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.zeros zeros, pending).1 + 1 ≤ widthhb:[].length + 2 ≤ widthhc:[true].length + 2 ≤ widthhin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb false)ht:t ≤ bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] false⊢ pending ≤ width All goals completed! 🐙) hz (input:List (Fin 3)pos:Fin (input.length + 2)width:ℕt:ℕpending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hp:(Scanner.Mode.zeros zeros, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.zeros zeros, pending).1 + 1 ≤ widthhb:[].length + 2 ≤ widthhc:[true].length + 2 ≤ widthhin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb false)ht:t ≤ bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] false⊢ [].length + 1 ≤ width simpa only [List.length_nil] using Nat.le_trans (input:List (Fin 3)pos:Fin (input.length + 2)width:ℕt:ℕpending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hp:(Scanner.Mode.zeros zeros, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.zeros zeros, pending).1 + 1 ≤ widthhb:[].length + 2 ≤ widthhc:[true].length + 2 ≤ widthhin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb false)ht:t ≤ bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] false⊢ 0 + 1 ≤ [].length + 2 All goals completed! 🐙) hb) (input:List (Fin 3)pos:Fin (input.length + 2)width:ℕt:ℕpending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hp:(Scanner.Mode.zeros zeros, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.zeros zeros, pending).1 + 1 ≤ widthhb:[].length + 2 ≤ widthhc:[true].length + 2 ≤ widthhin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb false)ht:t ≤ bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] false⊢ [true].length + 1 ≤ width simpa only [List.length_cons, List.length_nil] using Nat.le_trans (input:List (Fin 3)pos:Fin (input.length + 2)width:ℕt:ℕpending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hp:(Scanner.Mode.zeros zeros, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.zeros zeros, pending).1 + 1 ≤ widthhb:[].length + 2 ≤ widthhc:[true].length + 2 ≤ widthhin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb false)ht:t ≤ bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] false⊢ 0 + 1 + 1 ≤ [true].length + 2 All goals completed! 🐙) hc) hin t ht input:List (Fin 3)pos:Fin (input.length + 2)width:ℕt:ℕpending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hp:(Scanner.Mode.zeros zeros, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.zeros zeros, pending).1 + 1 ≤ widthhb:[].length + 2 ≤ widthhc:[true].length + 2 ≤ widthhin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb true)ht:t ≤ bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] true⊢ HeadBound width (configs (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) t) input:List (Fin 3)pos:Fin (input.length + 2)width:ℕt:ℕpending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hp:(Scanner.Mode.zeros zeros, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.zeros zeros, pending).1 + 1 ≤ widthhb:[].length + 2 ≤ widthhc:[true].length + 2 ≤ widthhin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb true)ht:t ≤ bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] truehe:zeros = 0⊢ HeadBound width (configs (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) t)input:List (Fin 3)pos:Fin (input.length + 2)width:ℕt:ℕpending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hp:(Scanner.Mode.zeros zeros, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.zeros zeros, pending).1 + 1 ≤ widthhb:[].length + 2 ≤ widthhc:[true].length + 2 ≤ widthhin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb true)ht:t ≤ bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] truehe:¬zeros = 0⊢ HeadBound width (configs (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) t) input:List (Fin 3)pos:Fin (input.length + 2)width:ℕt:ℕpending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hp:(Scanner.Mode.zeros zeros, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.zeros zeros, pending).1 + 1 ≤ widthhb:[].length + 2 ≤ widthhc:[true].length + 2 ≤ widthhin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb true)ht:t ≤ bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] truehe:zeros = 0⊢ HeadBound width (configs (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) t) input:List (Fin 3)pos:Fin (input.length + 2)width:ℕt:ℕpending:ℕhb:[].length + 2 ≤ widthhc:[true].length + 2 ≤ widthhs:Scanner.Active (Scanner.Mode.zeros 0, pending)hp:(Scanner.Mode.zeros 0, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.zeros 0, pending).1 + 1 ≤ widthhin:(modelCfg input pos (Scanner.Mode.zeros 0, pending) [] [true]).inputSymbol = some (boolEmb true)ht:t ≤ bitCost (Scanner.Mode.zeros 0, pending).1 [] [true] true⊢ HeadBound width (configs (modelCfg input pos (Scanner.Mode.zeros 0, pending) [] [true]) t) exact configs_empty_leaf_headBound input pos pending width hs (input:List (Fin 3)pos:Fin (input.length + 2)width:ℕt:ℕpending:ℕhb:[].length + 2 ≤ widthhc:[true].length + 2 ≤ widthhs:Scanner.Active (Scanner.Mode.zeros 0, pending)hp:(Scanner.Mode.zeros 0, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.zeros 0, pending).1 + 1 ≤ widthhin:(modelCfg input pos (Scanner.Mode.zeros 0, pending) [] [true]).inputSymbol = some (boolEmb true)ht:t ≤ bitCost (Scanner.Mode.zeros 0, pending).1 [] [true] true⊢ pending ≤ width All goals completed! 🐙) (input:List (Fin 3)pos:Fin (input.length + 2)width:ℕt:ℕpending:ℕhb:[].length + 2 ≤ widthhc:[true].length + 2 ≤ widthhs:Scanner.Active (Scanner.Mode.zeros 0, pending)hp:(Scanner.Mode.zeros 0, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.zeros 0, pending).1 + 1 ≤ widthhin:(modelCfg input pos (Scanner.Mode.zeros 0, pending) [] [true]).inputSymbol = some (boolEmb true)ht:t ≤ bitCost (Scanner.Mode.zeros 0, pending).1 [] [true] true⊢ 2 ≤ width All goals completed! 🐙) hin t ht input:List (Fin 3)pos:Fin (input.length + 2)width:ℕt:ℕpending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hp:(Scanner.Mode.zeros zeros, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.zeros zeros, pending).1 + 1 ≤ widthhb:[].length + 2 ≤ widthhc:[true].length + 2 ≤ widthhin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb true)ht:t ≤ bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] truehe:¬zeros = 0⊢ HeadBound width (configs (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) t) input:List (Fin 3)pos:Fin (input.length + 2)width:ℕt:ℕpending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hp:(Scanner.Mode.zeros zeros, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.zeros zeros, pending).1 + 1 ≤ widthhb:[].length + 2 ≤ widthhc:[true].length + 2 ≤ widthhin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb true)ht:t ≤ bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] truehe:¬zeros = 0ht':t ≤ 2⊢ HeadBound width (configs (modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]) t) exact configs_zeros_true_headBound input pos pending zeros width (input:List (Fin 3)pos:Fin (input.length + 2)width:ℕt:ℕpending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hp:(Scanner.Mode.zeros zeros, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.zeros zeros, pending).1 + 1 ≤ widthhb:[].length + 2 ≤ widthhc:[true].length + 2 ≤ widthhin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb true)ht:t ≤ bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] truehe:¬zeros = 0ht':t ≤ 2⊢ 0 < zeros All goals completed! 🐙) (input:List (Fin 3)pos:Fin (input.length + 2)width:ℕt:ℕpending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hp:(Scanner.Mode.zeros zeros, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.zeros zeros, pending).1 + 1 ≤ widthhb:[].length + 2 ≤ widthhc:[true].length + 2 ≤ widthhin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb true)ht:t ≤ bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] truehe:¬zeros = 0ht':t ≤ 2⊢ pending ≤ width All goals completed! 🐙) (input:List (Fin 3)pos:Fin (input.length + 2)width:ℕt:ℕpending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hp:(Scanner.Mode.zeros zeros, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.zeros zeros, pending).1 + 1 ≤ widthhb:[].length + 2 ≤ widthhc:[true].length + 2 ≤ widthhin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb true)ht:t ≤ bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] truehe:¬zeros = 0ht':t ≤ 2⊢ zeros ≤ width input:List (Fin 3)pos:Fin (input.length + 2)width:ℕt:ℕpending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hp:(Scanner.Mode.zeros zeros, pending).2 + 1 ≤ widthhb:[].length + 2 ≤ widthhc:[true].length + 2 ≤ widthhin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb true)ht:t ≤ bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] truehe:¬zeros = 0ht':t ≤ 2hz:zeros + 1 ≤ width⊢ zeros ≤ width; All goals completed! 🐙) (input:List (Fin 3)pos:Fin (input.length + 2)width:ℕt:ℕpending:ℕzeros:ℕhs:Scanner.Active (Scanner.Mode.zeros zeros, pending)hp:(Scanner.Mode.zeros zeros, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.zeros zeros, pending).1 + 1 ≤ widthhb:[].length + 2 ≤ widthhc:[true].length + 2 ≤ widthhin:(modelCfg input pos (Scanner.Mode.zeros zeros, pending) [] [true]).inputSymbol = some (boolEmb true)ht:t ≤ bitCost (Scanner.Mode.zeros zeros, pending).1 [] [true] truehe:¬zeros = 0ht':t ≤ 2⊢ 2 ≤ width All goals completed! 🐙) hin t ht' input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕremaining:ℕv:ℕhs:Scanner.Active (Scanner.Mode.size remaining v, pending)hw:Words (Scanner.Mode.size remaining v, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.size remaining v, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.size remaining v, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.size remaining v, pending).1 bs cs b⊢ HeadBound width (configs (modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs) t) exact configs_size_headBound input pos pending remaining bs cs b hs.2.1 (input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕremaining:ℕv:ℕhs:Scanner.Active (Scanner.Mode.size remaining v, pending)hw:Words (Scanner.Mode.size remaining v, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.size remaining v, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.size remaining v, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.size remaining v, pending).1 bs cs b⊢ 0 < Counter.value bs input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕremaining:ℕv:ℕhs:Scanner.Active (Scanner.Mode.size remaining v, pending)hw:Words (Scanner.Mode.size remaining v, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.size remaining v, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.size remaining v, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.size remaining v, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.size remaining v, pending).1 bs cs b⊢ 0 < v; All goals completed! 🐙) hin width hp hz hb hc t ht input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕremaining:ℕv:ℕhs:Scanner.Active (Scanner.Mode.length remaining v, pending)hw:Words (Scanner.Mode.length remaining v, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.length remaining v, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.length remaining v, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.length remaining v, pending).1 bs cs b⊢ HeadBound width (configs (modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs) t) exact configs_length_headBound input pos pending remaining bs cs b hs.2.1 hw.1 (input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕremaining:ℕv:ℕhs:Scanner.Active (Scanner.Mode.length remaining v, pending)hw:Words (Scanner.Mode.length remaining v, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.length remaining v, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.length remaining v, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.length remaining v, pending).1 bs cs b⊢ 0 < Counter.value cs input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕremaining:ℕv:ℕhs:Scanner.Active (Scanner.Mode.length remaining v, pending)hw:Words (Scanner.Mode.length remaining v, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.length remaining v, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.length remaining v, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.length remaining v, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.length remaining v, pending).1 bs cs b⊢ 0 < v; All goals completed! 🐙) hin width hp hz hb hc t ht input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕremaining:ℕhs:Scanner.Active (Scanner.Mode.payload remaining, pending)hw:Words (Scanner.Mode.payload remaining, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.payload remaining, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.payload remaining, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.payload remaining, pending).1 bs cs b⊢ HeadBound width (configs (modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs) t) exact configs_payload_headBound input pos pending remaining bs cs b width hs.1 hs.2 hw.2 (input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕremaining:ℕhs:Scanner.Active (Scanner.Mode.payload remaining, pending)hw:Words (Scanner.Mode.payload remaining, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.payload remaining, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.payload remaining, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.payload remaining, pending).1 bs cs b⊢ pending ≤ width All goals completed! 🐙) (input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕremaining:ℕhs:Scanner.Active (Scanner.Mode.payload remaining, pending)hw:Words (Scanner.Mode.payload remaining, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.payload remaining, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.payload remaining, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.payload remaining, pending).1 bs cs b⊢ bs.length + 1 ≤ width All goals completed! 🐙) (input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕremaining:ℕhs:Scanner.Active (Scanner.Mode.payload remaining, pending)hw:Words (Scanner.Mode.payload remaining, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.payload remaining, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.payload remaining, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.payload remaining, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.payload remaining, pending).1 bs cs b⊢ cs.length + 1 ≤ width All goals completed! 🐙) hin t ht input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕhs:Scanner.Active (Scanner.Mode.done, pending)hw:Words (Scanner.Mode.done, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.done, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.done, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.done, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.done, pending).1 bs cs b⊢ HeadBound width (configs (modelCfg input pos (Scanner.Mode.done, pending) bs cs) t) exact configs_terminal_headBound _ stDone b width rfl (Or.inl rfl) hin (scanCfg_headBound input pos stDone pending 0 bs cs width (input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕhs:Scanner.Active (Scanner.Mode.done, pending)hw:Words (Scanner.Mode.done, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.done, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.done, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.done, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.done, pending).1 bs cs b⊢ pending ≤ width All goals completed! 🐙) (input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕhs:Scanner.Active (Scanner.Mode.done, pending)hw:Words (Scanner.Mode.done, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.done, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.done, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.done, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.done, pending).1 bs cs b⊢ 0 ≤ width All goals completed! 🐙) (input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕhs:Scanner.Active (Scanner.Mode.done, pending)hw:Words (Scanner.Mode.done, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.done, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.done, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.done, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.done, pending).1 bs cs b⊢ bs.length + 1 ≤ width All goals completed! 🐙) (input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕhs:Scanner.Active (Scanner.Mode.done, pending)hw:Words (Scanner.Mode.done, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.done, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.done, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.done, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.done, pending).1 bs cs b⊢ cs.length + 1 ≤ width All goals completed! 🐙)) t ht input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕhs:Scanner.Active (Scanner.Mode.dead, pending)hw:Words (Scanner.Mode.dead, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.dead, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.dead, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.dead, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.dead, pending).1 bs cs b⊢ HeadBound width (configs (modelCfg input pos (Scanner.Mode.dead, pending) bs cs) t) exact configs_terminal_headBound _ stDead b width rfl (Or.inr rfl) hin (scanCfg_headBound input pos stDead pending 0 bs cs width (input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕhs:Scanner.Active (Scanner.Mode.dead, pending)hw:Words (Scanner.Mode.dead, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.dead, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.dead, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.dead, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.dead, pending).1 bs cs b⊢ pending ≤ width All goals completed! 🐙) (input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕhs:Scanner.Active (Scanner.Mode.dead, pending)hw:Words (Scanner.Mode.dead, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.dead, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.dead, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.dead, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.dead, pending).1 bs cs b⊢ 0 ≤ width All goals completed! 🐙) (input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕhs:Scanner.Active (Scanner.Mode.dead, pending)hw:Words (Scanner.Mode.dead, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.dead, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.dead, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.dead, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.dead, pending).1 bs cs b⊢ bs.length + 1 ≤ width All goals completed! 🐙) (input:List (Fin 3)pos:Fin (input.length + 2)bs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length + 2 ≤ widthhc:cs.length + 2 ≤ widtht:ℕpending:ℕhs:Scanner.Active (Scanner.Mode.dead, pending)hw:Words (Scanner.Mode.dead, pending).1 bs cshin:(modelCfg input pos (Scanner.Mode.dead, pending) bs cs).inputSymbol = some (boolEmb b)hp:(Scanner.Mode.dead, pending).2 + 1 ≤ widthhz:zeroCount (Scanner.Mode.dead, pending).1 + 1 ≤ widthht:t ≤ bitCost (Scanner.Mode.dead, pending).1 bs cs b⊢ cs.length + 1 ≤ width All goals completed! 🐙)) t ht
end Geb.BitTree.Elias.Machine