1. Geb
  2. Prototypes
  3. Computability
  4. BitTree
  5. Elias
  6. MachineHeader
Imports
/- Copyright (c) 2026 Terence Rokop. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Terence Rokop -/ module public import Geb.Prototypes.Computability.BitTree.Elias.MachineRead public import Geb.Prototypes.Computability.BitTree.Elias.MachineCounter public import Geb.Prototypes.Computability.BitTree.Elias.MachineNormalize
set_option doc.verso true

Executing the two binary delta-header fields

A width-field bit consumes one unary count position and, when that field ends, starts the binary countdown. A length-field bit appends to the payload count and decrements the width count. The last such bit also performs the initial payload decrement, removing its implicit offset of one.

Main statements

  • configs_size executes one bit of the binary width field.

  • configs_length executes one bit of the payload-length field.

Implementation notes

These are correspondence statements for Cslib execution and inherit Classical.choice from its input reader.

Tags

Elias delta code, Turing machine, header, simulation

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

Execute the width countdown in boundary configuration form.

theorem configs_decrement_false_scan (input : List (Fin 3)) (pos : Fin (input.length + 2)) (pending zeros : ℕ) (bs cs : List Bool) (hb : 0 < Counter.value bs) : machine.configs (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = scanCfg input pos (afterDecrement false ((Counter.decrement bs).any id)) pending zeros (Counter.decrement bs) cs ∧ machine.outputString (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = [] := input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhb:0 < Counter.value bs⊢ configs (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = scanCfg input pos (afterDecrement false ((Counter.decrement bs).any id)) pending zeros (Counter.decrement bs) cs ∧ machine.outputString (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhb:0 < Counter.value bsh:configs (counterCfg (scanCfg input pos (stDecrement false) pending zeros bs cs) false bs (stDecrement false) (bs.length + 1)) (2 * bs.length + 3) = counterCfg (scanCfg input pos (stDecrement false) pending zeros bs cs) false (Counter.decrement bs) (afterDecrement false ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (counterCfg (scanCfg input pos (stDecrement false) pending zeros bs cs) false bs (stDecrement false) (bs.length + 1)) (2 * bs.length + 3) = []⊢ configs (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = scanCfg input pos (afterDecrement false ((Counter.decrement bs).any id)) pending zeros (Counter.decrement bs) cs ∧ machine.outputString (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhb:0 < Counter.value bsh:configs (counterCfg (scanCfg input pos (stDecrement false) pending zeros bs cs) false bs (stDecrement false) (bs.length + 1)) (2 * bs.length + 3) = counterCfg (scanCfg input pos (stDecrement false) pending zeros bs cs) false (Counter.decrement bs) (afterDecrement false ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (counterCfg (scanCfg input pos (stDecrement false) pending zeros bs cs) false bs (stDecrement false) (bs.length + 1)) (2 * bs.length + 3) = []he:counterCfg (scanCfg input pos (stDecrement false) pending zeros bs cs) false (Counter.decrement bs) (afterDecrement false ((Counter.decrement bs).any id)) ((Counter.decrement bs).length + 1) = scanCfg input pos (afterDecrement false ((Counter.decrement bs).any id)) pending zeros (Counter.decrement bs) cs⊢ configs (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = scanCfg input pos (afterDecrement false ((Counter.decrement bs).any id)) pending zeros (Counter.decrement bs) cs ∧ machine.outputString (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhb:0 < Counter.value bsh:configs (counterCfg (scanCfg input pos (stDecrement false) pending zeros bs cs) false bs (stDecrement false) (bs.length + 1)) (2 * bs.length + 3) = counterCfg (scanCfg input pos (stDecrement false) pending zeros bs cs) false (Counter.decrement bs) (afterDecrement false ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (counterCfg (scanCfg input pos (stDecrement false) pending zeros bs cs) false bs (stDecrement false) (bs.length + 1)) (2 * bs.length + 3) = []he:counterCfg (scanCfg input pos (stDecrement false) pending zeros bs cs) false (Counter.decrement bs) (afterDecrement false ((Counter.decrement bs).any id)) (bs.length + 1) = scanCfg input pos (afterDecrement false ((Counter.decrement bs).any id)) pending zeros (Counter.decrement bs) cs⊢ configs (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = scanCfg input pos (afterDecrement false ((Counter.decrement bs).any id)) pending zeros (Counter.decrement bs) cs ∧ machine.outputString (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = [] rwa [input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhb:0 < Counter.value bsh:configs (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = counterCfg (scanCfg input pos (stDecrement false) pending zeros bs cs) false (Counter.decrement bs) (afterDecrement false ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = []he:counterCfg (scanCfg input pos (stDecrement false) pending zeros bs cs) false (Counter.decrement bs) (afterDecrement false ((Counter.decrement bs).any id)) (bs.length + 1) = scanCfg input pos (afterDecrement false ((Counter.decrement bs).any id)) pending zeros (Counter.decrement bs) cs⊢ configs (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = scanCfg input pos (afterDecrement false ((Counter.decrement bs).any id)) pending zeros (Counter.decrement bs) cs ∧ machine.outputString (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhb:0 < Counter.value bsh:configs (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = scanCfg input pos (afterDecrement false ((Counter.decrement bs).any id)) pending zeros (Counter.decrement bs) cs ∧ machine.outputString (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = []he:counterCfg (scanCfg input pos (stDecrement false) pending zeros bs cs) false (Counter.decrement bs) (afterDecrement false ((Counter.decrement bs).any id)) (bs.length + 1) = scanCfg input pos (afterDecrement false ((Counter.decrement bs).any id)) pending zeros (Counter.decrement bs) cs⊢ configs (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = scanCfg input pos (afterDecrement false ((Counter.decrement bs).any id)) pending zeros (Counter.decrement bs) cs ∧ machine.outputString (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = []input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhb:0 < Counter.value bsh:configs (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = scanCfg input pos (afterDecrement false ((Counter.decrement bs).any id)) pending zeros (Counter.decrement bs) cs ∧ machine.outputString (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = []he:counterCfg (scanCfg input pos (stDecrement false) pending zeros bs cs) false (Counter.decrement bs) (afterDecrement false ((Counter.decrement bs).any id)) (bs.length + 1) = scanCfg input pos (afterDecrement false ((Counter.decrement bs).any id)) pending zeros (Counter.decrement bs) cs⊢ configs (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = scanCfg input pos (afterDecrement false ((Counter.decrement bs).any id)) pending zeros (Counter.decrement bs) cs ∧ machine.outputString (scanCfg input pos (stDecrement false) pending zeros bs cs) (2 * bs.length + 3) = [] at h

Execute the payload countdown in boundary configuration form.

theorem configs_decrement_true_scan (input : List (Fin 3)) (pos : Fin (input.length + 2)) (pending zeros : ℕ) (bs cs : List Bool) (hc : 0 < Counter.value cs) : machine.configs (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = scanCfg input pos (afterDecrement true ((Counter.decrement cs).any id)) pending zeros bs (Counter.decrement cs) ∧ machine.outputString (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = [] := input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhc:0 < Counter.value cs⊢ configs (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = scanCfg input pos (afterDecrement true ((Counter.decrement cs).any id)) pending zeros bs (Counter.decrement cs) ∧ machine.outputString (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhc:0 < Counter.value csh:configs (counterCfg (scanCfg input pos (stDecrement true) pending zeros bs cs) true cs (stDecrement true) (cs.length + 1)) (2 * cs.length + 3) = counterCfg (scanCfg input pos (stDecrement true) pending zeros bs cs) true (Counter.decrement cs) (afterDecrement true ((Counter.decrement cs).any id)) (cs.length + 1) ∧ machine.outputString (counterCfg (scanCfg input pos (stDecrement true) pending zeros bs cs) true cs (stDecrement true) (cs.length + 1)) (2 * cs.length + 3) = []⊢ configs (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = scanCfg input pos (afterDecrement true ((Counter.decrement cs).any id)) pending zeros bs (Counter.decrement cs) ∧ machine.outputString (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhc:0 < Counter.value csh:configs (counterCfg (scanCfg input pos (stDecrement true) pending zeros bs cs) true cs (stDecrement true) (cs.length + 1)) (2 * cs.length + 3) = counterCfg (scanCfg input pos (stDecrement true) pending zeros bs cs) true (Counter.decrement cs) (afterDecrement true ((Counter.decrement cs).any id)) (cs.length + 1) ∧ machine.outputString (counterCfg (scanCfg input pos (stDecrement true) pending zeros bs cs) true cs (stDecrement true) (cs.length + 1)) (2 * cs.length + 3) = []he:counterCfg (scanCfg input pos (stDecrement true) pending zeros bs cs) true (Counter.decrement cs) (afterDecrement true ((Counter.decrement cs).any id)) ((Counter.decrement cs).length + 1) = scanCfg input pos (afterDecrement true ((Counter.decrement cs).any id)) pending zeros bs (Counter.decrement cs)⊢ configs (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = scanCfg input pos (afterDecrement true ((Counter.decrement cs).any id)) pending zeros bs (Counter.decrement cs) ∧ machine.outputString (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhc:0 < Counter.value csh:configs (counterCfg (scanCfg input pos (stDecrement true) pending zeros bs cs) true cs (stDecrement true) (cs.length + 1)) (2 * cs.length + 3) = counterCfg (scanCfg input pos (stDecrement true) pending zeros bs cs) true (Counter.decrement cs) (afterDecrement true ((Counter.decrement cs).any id)) (cs.length + 1) ∧ machine.outputString (counterCfg (scanCfg input pos (stDecrement true) pending zeros bs cs) true cs (stDecrement true) (cs.length + 1)) (2 * cs.length + 3) = []he:counterCfg (scanCfg input pos (stDecrement true) pending zeros bs cs) true (Counter.decrement cs) (afterDecrement true ((Counter.decrement cs).any id)) (cs.length + 1) = scanCfg input pos (afterDecrement true ((Counter.decrement cs).any id)) pending zeros bs (Counter.decrement cs)⊢ configs (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = scanCfg input pos (afterDecrement true ((Counter.decrement cs).any id)) pending zeros bs (Counter.decrement cs) ∧ machine.outputString (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = [] rwa [input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhc:0 < Counter.value csh:configs (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = counterCfg (scanCfg input pos (stDecrement true) pending zeros bs cs) true (Counter.decrement cs) (afterDecrement true ((Counter.decrement cs).any id)) (cs.length + 1) ∧ machine.outputString (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = []he:counterCfg (scanCfg input pos (stDecrement true) pending zeros bs cs) true (Counter.decrement cs) (afterDecrement true ((Counter.decrement cs).any id)) (cs.length + 1) = scanCfg input pos (afterDecrement true ((Counter.decrement cs).any id)) pending zeros bs (Counter.decrement cs)⊢ configs (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = scanCfg input pos (afterDecrement true ((Counter.decrement cs).any id)) pending zeros bs (Counter.decrement cs) ∧ machine.outputString (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhc:0 < Counter.value csh:configs (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = scanCfg input pos (afterDecrement true ((Counter.decrement cs).any id)) pending zeros bs (Counter.decrement cs) ∧ machine.outputString (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = []he:counterCfg (scanCfg input pos (stDecrement true) pending zeros bs cs) true (Counter.decrement cs) (afterDecrement true ((Counter.decrement cs).any id)) (cs.length + 1) = scanCfg input pos (afterDecrement true ((Counter.decrement cs).any id)) pending zeros bs (Counter.decrement cs)⊢ configs (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = scanCfg input pos (afterDecrement true ((Counter.decrement cs).any id)) pending zeros bs (Counter.decrement cs) ∧ machine.outputString (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = []input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhc:0 < Counter.value csh:configs (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = scanCfg input pos (afterDecrement true ((Counter.decrement cs).any id)) pending zeros bs (Counter.decrement cs) ∧ machine.outputString (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = []he:counterCfg (scanCfg input pos (stDecrement true) pending zeros bs cs) true (Counter.decrement cs) (afterDecrement true ((Counter.decrement cs).any id)) (cs.length + 1) = scanCfg input pos (afterDecrement true ((Counter.decrement cs).any id)) pending zeros bs (Counter.decrement cs)⊢ configs (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = scanCfg input pos (afterDecrement true ((Counter.decrement cs).any id)) pending zeros bs (Counter.decrement cs) ∧ machine.outputString (scanCfg input pos (stDecrement true) pending zeros bs cs) (2 * cs.length + 3) = [] at h

Read a width-field bit, including the unary test and any initial width decrement.

theorem configs_size (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)) : machine.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) = [] := 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)⊢ 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) = [] 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)hs:(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⊢ 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) = [] 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)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) cs⊢ 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) = [] 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)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) cshread:configs (scanCfg input pos stSizeBit pending remaining bs cs) 1 = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending remaining bs cs) 1 = []⊢ 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) = [] 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)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) cshread:configs (scanCfg input pos stSizeBit pending remaining bs cs) 1 = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending remaining bs cs) 1 = []hcheck:configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs) 1 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs) 1 = []⊢ 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) = [] 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)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) cshread:configs (scanCfg input pos stSizeBit pending remaining bs cs) 1 = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending remaining bs cs) 1 = []hcheck:configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs) 1 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs) 1 = []hfirst:configs (scanCfg input pos stSizeBit pending remaining bs cs) (1 + 1) = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending remaining bs cs) (1 + 1) = []⊢ 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) = [] 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)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) cshread:configs (scanCfg input pos stSizeBit pending remaining bs cs) 1 = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending remaining bs cs) 1 = []hcheck:configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs) 1 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs) 1 = []hfirst:configs (scanCfg input pos stSizeBit pending remaining bs cs) (1 + 1) = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending remaining bs cs) (1 + 1) = []he:remaining = 1⊢ 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) = []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)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) cshread:configs (scanCfg input pos stSizeBit pending remaining bs cs) 1 = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending remaining bs cs) 1 = []hcheck:configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs) 1 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs) 1 = []hfirst:configs (scanCfg input pos stSizeBit pending remaining bs cs) (1 + 1) = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending remaining bs cs) (1 + 1) = []he:¬remaining = 1⊢ 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) = [] 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)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) cshread:configs (scanCfg input pos stSizeBit pending remaining bs cs) 1 = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending remaining bs cs) 1 = []hcheck:configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs) 1 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs) 1 = []hfirst:configs (scanCfg input pos stSizeBit pending remaining bs cs) (1 + 1) = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending remaining bs cs) (1 + 1) = []he:remaining = 1⊢ 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) = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolb:Boolhb:0 < Counter.value bshr:0 < 1hin:(scanCfg input pos stSizeBit pending 1 bs cs).inputSymbol = some (boolEmb b)hs:(scanCfg input pos stSizeBit pending 1 bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending 1 bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cshread:configs (scanCfg input pos stSizeBit pending 1 bs cs) 1 = scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) 1 = []hcheck:configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cs) 1 = scanCfg input (moveInputPos pos 1) (if 1 - 1 = 0 then stDecrement false else stSizeBit) pending (1 - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cs) 1 = []hfirst:configs (scanCfg input pos stSizeBit pending 1 bs cs) (1 + 1) = scanCfg input (moveInputPos pos 1) (if 1 - 1 = 0 then stDecrement false else stSizeBit) pending (1 - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) (1 + 1) = []⊢ configs (scanCfg input pos stSizeBit pending 1 bs cs) (if 1 = 1 then 2 * bs.length + 7 else 2) = scanCfg input (moveInputPos pos 1) (if 1 = 1 then stLengthBit else stSizeBit) pending (1 - 1) (if 1 = 1 then Counter.decrement (b :: bs) else b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) (if 1 = 1 then 2 * bs.length + 7 else 2) = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolb:Boolhb:0 < Counter.value bshr:0 < 1hin:(scanCfg input pos stSizeBit pending 1 bs cs).inputSymbol = some (boolEmb b)hs:(scanCfg input pos stSizeBit pending 1 bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending 1 bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cshread:configs (scanCfg input pos stSizeBit pending 1 bs cs) 1 = scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) 1 = []hcheck:configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cs) 1 = scanCfg input (moveInputPos pos 1) (if 1 - 1 = 0 then stDecrement false else stSizeBit) pending (1 - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cs) 1 = []hfirst:configs (scanCfg input pos stSizeBit pending 1 bs cs) (1 + 1) = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) (1 + 1) = []⊢ configs (scanCfg input pos stSizeBit pending 1 bs cs) (2 * bs.length + 7) = scanCfg input (moveInputPos pos 1) stLengthBit pending 0 (Counter.decrement (b :: bs)) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) (2 * bs.length + 7) = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolb:Boolhb:0 < Counter.value bshr:0 < 1hin:(scanCfg input pos stSizeBit pending 1 bs cs).inputSymbol = some (boolEmb b)hs:(scanCfg input pos stSizeBit pending 1 bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending 1 bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cshread:configs (scanCfg input pos stSizeBit pending 1 bs cs) 1 = scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) 1 = []hcheck:configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cs) 1 = scanCfg input (moveInputPos pos 1) (if 1 - 1 = 0 then stDecrement false else stSizeBit) pending (1 - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cs) 1 = []hfirst:configs (scanCfg input pos stSizeBit pending 1 bs cs) (1 + 1) = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) (1 + 1) = []hv:1 < Counter.value (b :: bs)⊢ configs (scanCfg input pos stSizeBit pending 1 bs cs) (2 * bs.length + 7) = scanCfg input (moveInputPos pos 1) stLengthBit pending 0 (Counter.decrement (b :: bs)) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) (2 * bs.length + 7) = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolb:Boolhb:0 < Counter.value bshr:0 < 1hin:(scanCfg input pos stSizeBit pending 1 bs cs).inputSymbol = some (boolEmb b)hs:(scanCfg input pos stSizeBit pending 1 bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending 1 bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cshread:configs (scanCfg input pos stSizeBit pending 1 bs cs) 1 = scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) 1 = []hcheck:configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cs) 1 = scanCfg input (moveInputPos pos 1) (if 1 - 1 = 0 then stDecrement false else stSizeBit) pending (1 - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cs) 1 = []hfirst:configs (scanCfg input pos stSizeBit pending 1 bs cs) (1 + 1) = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) (1 + 1) = []hv:1 < Counter.value (b :: bs)hseen:(Counter.decrement (b :: bs)).any id = true⊢ configs (scanCfg input pos stSizeBit pending 1 bs cs) (2 * bs.length + 7) = scanCfg input (moveInputPos pos 1) stLengthBit pending 0 (Counter.decrement (b :: bs)) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) (2 * bs.length + 7) = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolb:Boolhb:0 < Counter.value bshr:0 < 1hin:(scanCfg input pos stSizeBit pending 1 bs cs).inputSymbol = some (boolEmb b)hs:(scanCfg input pos stSizeBit pending 1 bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending 1 bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cshread:configs (scanCfg input pos stSizeBit pending 1 bs cs) 1 = scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) 1 = []hcheck:configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cs) 1 = scanCfg input (moveInputPos pos 1) (if 1 - 1 = 0 then stDecrement false else stSizeBit) pending (1 - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cs) 1 = []hfirst:configs (scanCfg input pos stSizeBit pending 1 bs cs) (1 + 1) = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) (1 + 1) = []hv:1 < Counter.value (b :: bs)hseen:(Counter.decrement (b :: bs)).any id = truehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 (b :: bs) cs) (2 * (b :: bs).length + 3) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement (b :: bs)).any id)) pending 0 (Counter.decrement (b :: bs)) cs ∧ machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 (b :: bs) cs) (2 * (b :: bs).length + 3) = []⊢ configs (scanCfg input pos stSizeBit pending 1 bs cs) (2 * bs.length + 7) = scanCfg input (moveInputPos pos 1) stLengthBit pending 0 (Counter.decrement (b :: bs)) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) (2 * bs.length + 7) = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolb:Boolhb:0 < Counter.value bshr:0 < 1hin:(scanCfg input pos stSizeBit pending 1 bs cs).inputSymbol = some (boolEmb b)hs:(scanCfg input pos stSizeBit pending 1 bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending 1 bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cshread:configs (scanCfg input pos stSizeBit pending 1 bs cs) 1 = scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) 1 = []hcheck:configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cs) 1 = scanCfg input (moveInputPos pos 1) (if 1 - 1 = 0 then stDecrement false else stSizeBit) pending (1 - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cs) 1 = []hfirst:configs (scanCfg input pos stSizeBit pending 1 bs cs) (1 + 1) = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) (1 + 1) = []hv:1 < Counter.value (b :: bs)hseen:(Counter.decrement (b :: bs)).any id = truehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 (b :: bs) cs) (2 * (b :: bs).length + 3) = scanCfg input (moveInputPos pos 1) (afterDecrement false true) pending 0 (Counter.decrement (b :: bs)) cs ∧ machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 (b :: bs) cs) (2 * (b :: bs).length + 3) = []⊢ configs (scanCfg input pos stSizeBit pending 1 bs cs) (2 * bs.length + 7) = scanCfg input (moveInputPos pos 1) stLengthBit pending 0 (Counter.decrement (b :: bs)) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) (2 * bs.length + 7) = [] input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕbs:List Boolcs:List Boolb:Boolhb:0 < Counter.value bshr:0 < 1hin:(scanCfg input pos stSizeBit pending 1 bs cs).inputSymbol = some (boolEmb b)hs:(scanCfg input pos stSizeBit pending 1 bs cs).inputSymbol = some (boolEmb b) → step (scanCfg input pos stSizeBit pending 1 bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cshread:configs (scanCfg input pos stSizeBit pending 1 bs cs) 1 = scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) 1 = []hcheck:configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cs) 1 = scanCfg input (moveInputPos pos 1) (if 1 - 1 = 0 then stDecrement false else stSizeBit) pending (1 - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input (moveInputPos pos 1) stSizeCheck pending (1 - 1) (b :: bs) cs) 1 = []hfirst:configs (scanCfg input pos stSizeBit pending 1 bs cs) (1 + 1) = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) (1 + 1) = []hv:1 < Counter.value (b :: bs)hseen:(Counter.decrement (b :: bs)).any id = truehdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 (b :: bs) cs) (2 * (b :: bs).length + 3) = scanCfg input (moveInputPos pos 1) (afterDecrement false true) pending 0 (Counter.decrement (b :: bs)) cs ∧ machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 (b :: bs) cs) (2 * (b :: bs).length + 3) = []h:configs (scanCfg input pos stSizeBit pending 1 bs cs) (2 + (2 * (b :: bs).length + 3)) = scanCfg input (moveInputPos pos 1) (afterDecrement false true) pending 0 (Counter.decrement (b :: bs)) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) (2 + (2 * (b :: bs).length + 3)) = []⊢ configs (scanCfg input pos stSizeBit pending 1 bs cs) (2 * bs.length + 7) = scanCfg input (moveInputPos pos 1) stLengthBit pending 0 (Counter.decrement (b :: bs)) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending 1 bs cs) (2 * bs.length + 7) = [] simpa only [List.length_cons, afterDecrement, Bool.false_eq_true, ↓reduceIte, show 2 + (2 * (bs.length + 1) + 3) = 2 * bs.length + 7 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)⊢ 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) = [] All goals completed! 🐙] using h 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)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) cshread:configs (scanCfg input pos stSizeBit pending remaining bs cs) 1 = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending remaining bs cs) 1 = []hcheck:configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs) 1 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs) 1 = []hfirst:configs (scanCfg input pos stSizeBit pending remaining bs cs) (1 + 1) = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending remaining bs cs) (1 + 1) = []he:¬remaining = 1⊢ 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) = [] 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)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) cshread:configs (scanCfg input pos stSizeBit pending remaining bs cs) 1 = scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending remaining bs cs) 1 = []hcheck:configs (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs) 1 = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input (moveInputPos pos 1) stSizeCheck pending (remaining - 1) (b :: bs) cs) 1 = []hfirst:configs (scanCfg input pos stSizeBit pending remaining bs cs) (1 + 1) = scanCfg input (moveInputPos pos 1) (if remaining - 1 = 0 then stDecrement false else stSizeBit) pending (remaining - 1) (b :: bs) cs ∧ machine.outputString (scanCfg input pos stSizeBit pending remaining bs cs) (1 + 1) = []he:¬remaining = 1hz:remaining - 1 ≠ 0⊢ 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) = [] All goals completed! 🐙

Read a length-field bit, decrementing the width and then any completed payload value.

theorem configs_length (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)) : machine.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) = [] := 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)⊢ 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) = [] 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)hread:configs (scanCfg input pos stLengthBit pending 0 bs cs) 1 = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) 1 = []⊢ 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) = [] 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)hread:configs (scanCfg input pos stLengthBit pending 0 bs cs) 1 = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = []⊢ 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) = [] 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)hread:configs (scanCfg input pos stLengthBit pending 0 bs cs) 1 = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = []hfirst:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = []⊢ 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) = [] 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)hread:configs (scanCfg input pos stLengthBit pending 0 bs cs) 1 = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = []hfirst:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = []he:remaining = 1⊢ 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) = []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)hread:configs (scanCfg input pos stLengthBit pending 0 bs cs) 1 = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = []hfirst:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = []he:¬remaining = 1⊢ 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) = [] 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)hread:configs (scanCfg input pos stLengthBit pending 0 bs cs) 1 = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = []hfirst:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = []he:remaining = 1⊢ 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) = [] 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)hread:configs (scanCfg input pos stLengthBit pending 0 bs cs) 1 = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = []hfirst:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = []he:remaining = 1hzero:(Counter.decrement bs).any id = false⊢ 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) = [] 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)hread:configs (scanCfg input pos stLengthBit pending 0 bs cs) 1 = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = []hfirst:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (afterDecrement false false) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = []he:remaining = 1hzero:(Counter.decrement bs).any id = false⊢ 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) = [] 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)hread:configs (scanCfg input pos stLengthBit pending 0 bs cs) 1 = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = []hfirst:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (afterDecrement false false) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = []he:remaining = 1hzero:(Counter.decrement bs).any id = falsehv:1 < Counter.value (b :: cs)⊢ 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) = [] 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)hread:configs (scanCfg input pos stLengthBit pending 0 bs cs) 1 = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = []hfirst:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (afterDecrement false false) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = []he:remaining = 1hzero:(Counter.decrement bs).any id = falsehv:1 < Counter.value (b :: cs)hseen:(Counter.decrement (b :: cs)).any id = true⊢ 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) = [] 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)hread:configs (scanCfg input pos stLengthBit pending 0 bs cs) 1 = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = []hfirst:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (afterDecrement false false) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = []he:remaining = 1hzero:(Counter.decrement bs).any id = falsehv:1 < Counter.value (b :: cs)hseen:(Counter.decrement (b :: cs)).any id = truehlast:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)) (2 * (b :: cs).length + 3) = scanCfg input (moveInputPos pos 1) (afterDecrement true ((Counter.decrement (b :: cs)).any id)) pending 0 (Counter.decrement bs) (Counter.decrement (b :: cs)) ∧ machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)) (2 * (b :: cs).length + 3) = []⊢ 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) = [] 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)hread:configs (scanCfg input pos stLengthBit pending 0 bs cs) 1 = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = []hfirst:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (afterDecrement false false) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = []he:remaining = 1hzero:(Counter.decrement bs).any id = falsehv:1 < Counter.value (b :: cs)hseen:(Counter.decrement (b :: cs)).any id = truehlast:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)) (2 * (b :: cs).length + 3) = scanCfg input (moveInputPos pos 1) (afterDecrement true true) pending 0 (Counter.decrement bs) (Counter.decrement (b :: cs)) ∧ machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)) (2 * (b :: cs).length + 3) = []⊢ 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) = [] 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)hread:configs (scanCfg input pos stLengthBit pending 0 bs cs) 1 = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = []hfirst:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (afterDecrement false false) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = []he:remaining = 1hzero:(Counter.decrement bs).any id = falsehv:1 < Counter.value (b :: cs)hseen:(Counter.decrement (b :: cs)).any id = truehlast:configs (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)) (2 * (b :: cs).length + 3) = scanCfg input (moveInputPos pos 1) (afterDecrement true true) pending 0 (Counter.decrement bs) (Counter.decrement (b :: cs)) ∧ machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement true) pending 0 (Counter.decrement bs) (b :: cs)) (2 * (b :: cs).length + 3) = []h:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3) + (2 * (b :: cs).length + 3)) = scanCfg input (moveInputPos pos 1) (afterDecrement true true) pending 0 (Counter.decrement bs) (Counter.decrement (b :: cs)) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3) + (2 * (b :: cs).length + 3)) = []⊢ 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) = [] simpa only [he, ↓reduceIte, List.length_cons, afterDecrement, Bool.false_eq_true, show 1 + (2 * bs.length + 3) + (2 * (cs.length + 1) + 3) = 2 * bs.length + 2 * cs.length + 9 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)⊢ 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) = [] All goals completed! 🐙] using h 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)hread:configs (scanCfg input pos stLengthBit pending 0 bs cs) 1 = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = []hfirst:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = []he:¬remaining = 1⊢ 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) = [] 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)hread:configs (scanCfg input pos stLengthBit pending 0 bs cs) 1 = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = []hfirst:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = []he:¬remaining = 1hseen:(Counter.decrement bs).any id = true⊢ 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) = [] 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)hread:configs (scanCfg input pos stLengthBit pending 0 bs cs) 1 = scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) 1 = []hdec:configs (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = scanCfg input (moveInputPos pos 1) (afterDecrement false ((Counter.decrement bs).any id)) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input (moveInputPos pos 1) (stDecrement false) pending 0 bs (b :: cs)) (2 * bs.length + 3) = []hfirst:configs (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = scanCfg input (moveInputPos pos 1) (afterDecrement false true) pending 0 (Counter.decrement bs) (b :: cs) ∧ machine.outputString (scanCfg input pos stLengthBit pending 0 bs cs) (1 + (2 * bs.length + 3)) = []he:¬remaining = 1hseen:(Counter.decrement bs).any id = true⊢ 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) = [] simpa only [he, ↓reduceIte, afterDecrement, Bool.false_eq_true, show 1 + (2 * bs.length + 3) = 2 * bs.length + 4 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)⊢ 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) = [] All goals completed! 🐙] using hfirst
end Geb.BitTree.Elias.Machine