1. Geb
  2. Prototypes
  3. Computability
  4. BitTree
  5. Elias
  6. MachineCounter
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.MachineSteps public import Geb.Prototypes.Computability.BitTree.Elias.Counter public import Geb.Prototypes.Computability.TreeScanner.Steps
set_option doc.verso true

Execution of binary countdowns

The countdown enters its least significant digit from the blank on the right. Borrowing and the following leftward scan visit the digit positions once; the return scan visits them once more, retaining whether the decremented counter contains a one.

Main statements

  • configs_decrement gives the exact countdown result and transition count.

  • configs_decrement_headBound bounds every intermediate work-tape head.

Tags

Turing machine, binary counter, decrement, simulation

@[expose] public sectionnamespace Geb.BitTree.Elias.Machineopen Turing MultiTapeTMopen Geb.TreeScanner (step_of_state)

A stationary-input counter action with no write changes only its selected head and state.

theorem counterAction_none_run {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (v : Bool) (bs : List Bool) (q q' : Control) (p p' : ℕ) (d : SignType) (htr : machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q') (hp : (p : ℤ) + d = p') : machine.step (counterCfg cfg v bs q p) = counterCfg cfg v bs q' p' ∧ machine.outputSymbol (counterCfg cfg v bs q p) = none := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'⊢ step (counterCfg cfg v bs q p) = counterCfg cfg v bs q' p' ∧ outputSymbol (counterCfg cfg v bs q p) = none input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'⊢ step (counterCfg cfg v bs q p) = counterCfg cfg v bs q' p'input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'⊢ outputSymbol (counterCfg cfg v bs q p) = none input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'⊢ step (counterCfg cfg v bs q p) = counterCfg cfg v bs q' p' input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'⊢ { state := (counterAction v none d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v none d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v none d q').workActions i).2 } = counterCfg cfg v bs q' p' input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'⊢ { state := (counterAction v none d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v none d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v none d q').workActions i).2 }.workTapes = (counterCfg cfg v bs q' p').workTapesinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'⊢ { state := (counterAction v none d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v none d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v none d q').workActions i).2 }.workTapePos = (counterCfg cfg v bs q' p').workTapePos input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'⊢ { state := (counterAction v none d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v none d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v none d q').workActions i).2 }.workTapes = (counterCfg cfg v bs q' p').workTapes input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'i:Fin 4z:ℤ⊢ { state := (counterAction v none d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v none d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v none d q').workActions i).2 }.workTapes i z = (counterCfg cfg v bs q' p').workTapes i z input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'i:Fin 4z:ℤhi:i = counterTape v⊢ { state := (counterAction v none d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v none d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v none d q').workActions i).2 }.workTapes i z = (counterCfg cfg v bs q' p').workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'i:Fin 4z:ℤhi:¬i = counterTape v⊢ { state := (counterAction v none d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v none d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v none d q').workActions i).2 }.workTapes i z = (counterCfg cfg v bs q' p').workTapes i z input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'i:Fin 4z:ℤhi:i = counterTape v⊢ { state := (counterAction v none d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v none d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v none d q').workActions i).2 }.workTapes i z = (counterCfg cfg v bs q' p').workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'i:Fin 4z:ℤhi:¬i = counterTape v⊢ { state := (counterAction v none d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v none d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v none d q').workActions i).2 }.workTapes i z = (counterCfg cfg v bs q' p').workTapes i z All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'⊢ { state := (counterAction v none d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v none d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v none d q').workActions i).2 }.workTapePos = (counterCfg cfg v bs q' p').workTapePos input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'i:Fin 4⊢ { state := (counterAction v none d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v none d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v none d q').workActions i).2 }.workTapePos i = (counterCfg cfg v bs q' p').workTapePos i input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'i:Fin 4hi:i = counterTape v⊢ { state := (counterAction v none d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v none d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v none d q').workActions i).2 }.workTapePos i = (counterCfg cfg v bs q' p').workTapePos iinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'i:Fin 4hi:¬i = counterTape v⊢ { state := (counterAction v none d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v none d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v none d q').workActions i).2 }.workTapePos i = (counterCfg cfg v bs q' p').workTapePos i input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'i:Fin 4hi:i = counterTape v⊢ { state := (counterAction v none d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v none d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v none d q').workActions i).2 }.workTapePos i = (counterCfg cfg v bs q' p').workTapePos iinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'i:Fin 4hi:¬i = counterTape v⊢ { state := (counterAction v none d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v none d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v none d q').workActions i).2 }.workTapePos i = (counterCfg cfg v bs q' p').workTapePos i All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'⊢ outputSymbol (counterCfg cfg v bs q p) = none input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'⊢ (machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols).outS = none input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypehtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v none d q'hp:↑p + ↑d = ↑p'⊢ (counterAction v none d q').outS = none All goals completed! 🐙

A writing counter action realizes a prescribed change of the finite digit word.

theorem counterAction_write_run {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (v : Bool) (bs bs' : List Bool) (q q' : Control) (p p' : ℕ) (d : SignType) (b : Bool) (htr : machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q') (hp : (p : ℤ) + d = p') (hw : Function.update (wordTape bs) (p : ℤ) (some (boolEmb b)) = wordTape bs') : machine.step (counterCfg cfg v bs q p) = counterCfg cfg v bs' q' p' ∧ machine.outputSymbol (counterCfg cfg v bs q p) = none := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'⊢ step (counterCfg cfg v bs q p) = counterCfg cfg v bs' q' p' ∧ outputSymbol (counterCfg cfg v bs q p) = none input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'⊢ step (counterCfg cfg v bs q p) = counterCfg cfg v bs' q' p'input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'⊢ outputSymbol (counterCfg cfg v bs q p) = none input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'⊢ step (counterCfg cfg v bs q p) = counterCfg cfg v bs' q' p' input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'⊢ { state := (counterAction v (some (some (boolEmb b))) d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v (some (some (boolEmb b))) d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v (some (some (boolEmb b))) d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v (some (some (boolEmb b))) d q').workActions i).2 } = counterCfg cfg v bs' q' p' input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'⊢ { state := (counterAction v (some (some (boolEmb b))) d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v (some (some (boolEmb b))) d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v (some (some (boolEmb b))) d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v (some (some (boolEmb b))) d q').workActions i).2 }.workTapes = (counterCfg cfg v bs' q' p').workTapesinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'⊢ { state := (counterAction v (some (some (boolEmb b))) d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v (some (some (boolEmb b))) d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v (some (some (boolEmb b))) d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v (some (some (boolEmb b))) d q').workActions i).2 }.workTapePos = (counterCfg cfg v bs' q' p').workTapePos input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'⊢ { state := (counterAction v (some (some (boolEmb b))) d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v (some (some (boolEmb b))) d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v (some (some (boolEmb b))) d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v (some (some (boolEmb b))) d q').workActions i).2 }.workTapes = (counterCfg cfg v bs' q' p').workTapes input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'i:Fin 4z:ℤ⊢ { state := (counterAction v (some (some (boolEmb b))) d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v (some (some (boolEmb b))) d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v (some (some (boolEmb b))) d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v (some (some (boolEmb b))) d q').workActions i).2 }.workTapes i z = (counterCfg cfg v bs' q' p').workTapes i z input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'i:Fin 4z:ℤhi:i = counterTape v⊢ { state := (counterAction v (some (some (boolEmb b))) d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v (some (some (boolEmb b))) d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v (some (some (boolEmb b))) d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v (some (some (boolEmb b))) d q').workActions i).2 }.workTapes i z = (counterCfg cfg v bs' q' p').workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'i:Fin 4z:ℤhi:¬i = counterTape v⊢ { state := (counterAction v (some (some (boolEmb b))) d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v (some (some (boolEmb b))) d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v (some (some (boolEmb b))) d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v (some (some (boolEmb b))) d q').workActions i).2 }.workTapes i z = (counterCfg cfg v bs' q' p').workTapes i z input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'i:Fin 4z:ℤhi:i = counterTape v⊢ { state := (counterAction v (some (some (boolEmb b))) d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v (some (some (boolEmb b))) d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v (some (some (boolEmb b))) d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v (some (some (boolEmb b))) d q').workActions i).2 }.workTapes i z = (counterCfg cfg v bs' q' p').workTapes i z input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'i:Fin 4z:ℤhi:i = counterTape v⊢ Function.update (wordTape bs) (↑p) (some (boolEmb b)) z = wordTape bs' z All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'i:Fin 4z:ℤhi:¬i = counterTape v⊢ { state := (counterAction v (some (some (boolEmb b))) d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v (some (some (boolEmb b))) d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v (some (some (boolEmb b))) d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v (some (some (boolEmb b))) d q').workActions i).2 }.workTapes i z = (counterCfg cfg v bs' q' p').workTapes i z All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'⊢ { state := (counterAction v (some (some (boolEmb b))) d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v (some (some (boolEmb b))) d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v (some (some (boolEmb b))) d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v (some (some (boolEmb b))) d q').workActions i).2 }.workTapePos = (counterCfg cfg v bs' q' p').workTapePos input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'i:Fin 4⊢ { state := (counterAction v (some (some (boolEmb b))) d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v (some (some (boolEmb b))) d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v (some (some (boolEmb b))) d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v (some (some (boolEmb b))) d q').workActions i).2 }.workTapePos i = (counterCfg cfg v bs' q' p').workTapePos i input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'i:Fin 4hi:i = counterTape v⊢ { state := (counterAction v (some (some (boolEmb b))) d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v (some (some (boolEmb b))) d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v (some (some (boolEmb b))) d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v (some (some (boolEmb b))) d q').workActions i).2 }.workTapePos i = (counterCfg cfg v bs' q' p').workTapePos iinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'i:Fin 4hi:¬i = counterTape v⊢ { state := (counterAction v (some (some (boolEmb b))) d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v (some (some (boolEmb b))) d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v (some (some (boolEmb b))) d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v (some (some (boolEmb b))) d q').workActions i).2 }.workTapePos i = (counterCfg cfg v bs' q' p').workTapePos i input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'i:Fin 4hi:i = counterTape v⊢ { state := (counterAction v (some (some (boolEmb b))) d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v (some (some (boolEmb b))) d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v (some (some (boolEmb b))) d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v (some (some (boolEmb b))) d q').workActions i).2 }.workTapePos i = (counterCfg cfg v bs' q' p').workTapePos iinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'i:Fin 4hi:¬i = counterTape v⊢ { state := (counterAction v (some (some (boolEmb b))) d q').q', inputPos := moveInputPos (counterCfg cfg v bs q p).inputPos (counterAction v (some (some (boolEmb b))) d q').inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v (some (some (boolEmb b))) d q').workActions i).1 with | none => (counterCfg cfg v bs q p).workTapes i | some s => Function.update ((counterCfg cfg v bs q p).workTapes i) ((counterCfg cfg v bs q p).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs q p).workTapePos i + ↑((counterAction v (some (some (boolEmb b))) d q').workActions i).2 }.workTapePos i = (counterCfg cfg v bs' q' p').workTapePos i All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'⊢ outputSymbol (counterCfg cfg v bs q p) = none input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'⊢ (machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols).outS = none input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolbs':List Boolq:Controlq':Controlp:ℕp':ℕd:SignTypeb:Boolhtr:machine.tr q (counterCfg cfg v bs q p).inputSymbol (counterCfg cfg v bs q p).workTapeSymbols = counterAction v (some (some (boolEmb b))) d q'hp:↑p + ↑d = ↑p'hw:Function.update (wordTape bs) (↑p) (some (boolEmb b)) = wordTape bs'⊢ (counterAction v (some (some (boolEmb b))) d q').outS = none All goals completed! 🐙

Countdown entry moves left from the right-hand blank without writing.

theorem step_decrement {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (v : Bool) (bs : List Bool) : machine.step (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) = counterCfg cfg v bs (stBorrow v false) bs.length := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Bool⊢ step (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) = counterCfg cfg v bs (stBorrow v false) bs.length input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Bool⊢ { state := (counterAction v none (-1) (stBorrow v false)).q', inputPos := moveInputPos (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).inputPos (counterAction v none (-1) (stBorrow v false)).inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none (-1) (stBorrow v false)).workActions i).1 with | none => (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i | some s => Function.update ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i) ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i + ↑((counterAction v none (-1) (stBorrow v false)).workActions i).2 } = counterCfg cfg v bs (stBorrow v false) bs.length input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Bool⊢ { state := (counterAction v none (-1) (stBorrow v false)).q', inputPos := moveInputPos (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).inputPos (counterAction v none (-1) (stBorrow v false)).inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none (-1) (stBorrow v false)).workActions i).1 with | none => (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i | some s => Function.update ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i) ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i + ↑((counterAction v none (-1) (stBorrow v false)).workActions i).2 }.workTapes = (counterCfg cfg v bs (stBorrow v false) bs.length).workTapesinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Bool⊢ { state := (counterAction v none (-1) (stBorrow v false)).q', inputPos := moveInputPos (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).inputPos (counterAction v none (-1) (stBorrow v false)).inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none (-1) (stBorrow v false)).workActions i).1 with | none => (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i | some s => Function.update ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i) ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i + ↑((counterAction v none (-1) (stBorrow v false)).workActions i).2 }.workTapePos = (counterCfg cfg v bs (stBorrow v false) bs.length).workTapePos input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Bool⊢ { state := (counterAction v none (-1) (stBorrow v false)).q', inputPos := moveInputPos (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).inputPos (counterAction v none (-1) (stBorrow v false)).inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none (-1) (stBorrow v false)).workActions i).1 with | none => (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i | some s => Function.update ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i) ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i + ↑((counterAction v none (-1) (stBorrow v false)).workActions i).2 }.workTapes = (counterCfg cfg v bs (stBorrow v false) bs.length).workTapes input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Booli:Fin 4z:ℤ⊢ { state := (counterAction v none (-1) (stBorrow v false)).q', inputPos := moveInputPos (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).inputPos (counterAction v none (-1) (stBorrow v false)).inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none (-1) (stBorrow v false)).workActions i).1 with | none => (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i | some s => Function.update ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i) ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i + ↑((counterAction v none (-1) (stBorrow v false)).workActions i).2 }.workTapes i z = (counterCfg cfg v bs (stBorrow v false) bs.length).workTapes i z input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Booli:Fin 4z:ℤhi:i = counterTape v⊢ { state := (counterAction v none (-1) (stBorrow v false)).q', inputPos := moveInputPos (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).inputPos (counterAction v none (-1) (stBorrow v false)).inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none (-1) (stBorrow v false)).workActions i).1 with | none => (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i | some s => Function.update ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i) ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i + ↑((counterAction v none (-1) (stBorrow v false)).workActions i).2 }.workTapes i z = (counterCfg cfg v bs (stBorrow v false) bs.length).workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Booli:Fin 4z:ℤhi:¬i = counterTape v⊢ { state := (counterAction v none (-1) (stBorrow v false)).q', inputPos := moveInputPos (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).inputPos (counterAction v none (-1) (stBorrow v false)).inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none (-1) (stBorrow v false)).workActions i).1 with | none => (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i | some s => Function.update ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i) ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i + ↑((counterAction v none (-1) (stBorrow v false)).workActions i).2 }.workTapes i z = (counterCfg cfg v bs (stBorrow v false) bs.length).workTapes i z input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Booli:Fin 4z:ℤhi:i = counterTape v⊢ { state := (counterAction v none (-1) (stBorrow v false)).q', inputPos := moveInputPos (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).inputPos (counterAction v none (-1) (stBorrow v false)).inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none (-1) (stBorrow v false)).workActions i).1 with | none => (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i | some s => Function.update ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i) ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i + ↑((counterAction v none (-1) (stBorrow v false)).workActions i).2 }.workTapes i z = (counterCfg cfg v bs (stBorrow v false) bs.length).workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Booli:Fin 4z:ℤhi:¬i = counterTape v⊢ { state := (counterAction v none (-1) (stBorrow v false)).q', inputPos := moveInputPos (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).inputPos (counterAction v none (-1) (stBorrow v false)).inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none (-1) (stBorrow v false)).workActions i).1 with | none => (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i | some s => Function.update ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i) ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i + ↑((counterAction v none (-1) (stBorrow v false)).workActions i).2 }.workTapes i z = (counterCfg cfg v bs (stBorrow v false) bs.length).workTapes i z All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Bool⊢ { state := (counterAction v none (-1) (stBorrow v false)).q', inputPos := moveInputPos (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).inputPos (counterAction v none (-1) (stBorrow v false)).inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none (-1) (stBorrow v false)).workActions i).1 with | none => (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i | some s => Function.update ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i) ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i + ↑((counterAction v none (-1) (stBorrow v false)).workActions i).2 }.workTapePos = (counterCfg cfg v bs (stBorrow v false) bs.length).workTapePos input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Booli:Fin 4⊢ { state := (counterAction v none (-1) (stBorrow v false)).q', inputPos := moveInputPos (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).inputPos (counterAction v none (-1) (stBorrow v false)).inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none (-1) (stBorrow v false)).workActions i).1 with | none => (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i | some s => Function.update ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i) ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i + ↑((counterAction v none (-1) (stBorrow v false)).workActions i).2 }.workTapePos i = (counterCfg cfg v bs (stBorrow v false) bs.length).workTapePos i input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Booli:Fin 4hi:i = counterTape v⊢ { state := (counterAction v none (-1) (stBorrow v false)).q', inputPos := moveInputPos (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).inputPos (counterAction v none (-1) (stBorrow v false)).inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none (-1) (stBorrow v false)).workActions i).1 with | none => (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i | some s => Function.update ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i) ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i + ↑((counterAction v none (-1) (stBorrow v false)).workActions i).2 }.workTapePos i = (counterCfg cfg v bs (stBorrow v false) bs.length).workTapePos iinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Booli:Fin 4hi:¬i = counterTape v⊢ { state := (counterAction v none (-1) (stBorrow v false)).q', inputPos := moveInputPos (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).inputPos (counterAction v none (-1) (stBorrow v false)).inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none (-1) (stBorrow v false)).workActions i).1 with | none => (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i | some s => Function.update ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i) ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i + ↑((counterAction v none (-1) (stBorrow v false)).workActions i).2 }.workTapePos i = (counterCfg cfg v bs (stBorrow v false) bs.length).workTapePos i input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Booli:Fin 4hi:i = counterTape v⊢ { state := (counterAction v none (-1) (stBorrow v false)).q', inputPos := moveInputPos (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).inputPos (counterAction v none (-1) (stBorrow v false)).inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none (-1) (stBorrow v false)).workActions i).1 with | none => (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i | some s => Function.update ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i) ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i + ↑((counterAction v none (-1) (stBorrow v false)).workActions i).2 }.workTapePos i = (counterCfg cfg v bs (stBorrow v false) bs.length).workTapePos iinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Booli:Fin 4hi:¬i = counterTape v⊢ { state := (counterAction v none (-1) (stBorrow v false)).q', inputPos := moveInputPos (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).inputPos (counterAction v none (-1) (stBorrow v false)).inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((counterAction v none (-1) (stBorrow v false)).workActions i).1 with | none => (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i | some s => Function.update ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapes i) ((counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i) s, workTapePos := fun i ↦ (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapePos i + ↑((counterAction v none (-1) (stBorrow v false)).workActions i).2 }.workTapePos i = (counterCfg cfg v bs (stBorrow v false) bs.length).workTapePos i All goals completed! 🐙

Countdown entry emits no output.

theorem outputSymbol_decrement {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (v : Bool) (bs : List Bool) : machine.outputSymbol (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) = none := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Bool⊢ outputSymbol (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) = none input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Bool⊢ (machine.tr (stDecrement v) (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).inputSymbol (counterCfg cfg v bs (stDecrement v) (bs.length + 1)).workTapeSymbols).outS = none input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Bool⊢ (counterAction v none (-1) (stBorrow v false)).outS = none All goals completed! 🐙

The leftward scan inspects the next higher digit and preserves the stored word.

theorem left_cons_run {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (v seen b : Bool) (lower higher : List Bool) : machine.step (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length ∧ machine.outputSymbol (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = none := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolb:Boollower:List Boolhigher:List Bool⊢ step (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length ∧ outputSymbol (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = none input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolb:Boollower:List Boolhigher:List Bool⊢ machine.tr (stLeft v seen) (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)).inputSymbol (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)).workTapeSymbols = counterAction v none ?d (stLeft v (seen || b))input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolb:Boollower:List Boolhigher:List Bool⊢ ↑(higher.length + 1) + ↑?d = ↑higher.lengthinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolb:Boollower:List Boolhigher:List Bool⊢ SignType input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolb:Boollower:List Boolhigher:List Bool⊢ machine.tr (stLeft v seen) (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)).inputSymbol (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)).workTapeSymbols = counterAction v none ?d (stLeft v (seen || b)) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolb:Boollower:List Boolhigher:List Bool⊢ sweepLeft v seen (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)).workTapeSymbols = counterAction v none ?d (stLeft v (seen || b)) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolb:Boollower:List Boolhigher:List Boolhr:(counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)).workTapeSymbols (counterTape v) = some (boolEmb b)⊢ sweepLeft v seen (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)).workTapeSymbols = counterAction v none ?d (stLeft v (seen || b)) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolb:Boollower:List Boolhigher:List Boolhr:(counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)).workTapeSymbols (counterTape v) = some (boolEmb b)⊢ (if (some (boolEmb b) == some 2) = true then counterAction v none 1 (stRight v seen) else counterAction v none (-1) (stLeft v (seen || some (boolEmb b) == some 1))) = counterAction v none ?d (stLeft v (seen || b)) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Boolhr:(counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) (higher.length + 1)).workTapeSymbols (counterTape v) = some (boolEmb false)⊢ (if (some (boolEmb false) == some 2) = true then counterAction v none 1 (stRight v seen) else counterAction v none (-1) (stLeft v (seen || some (boolEmb false) == some 1))) = counterAction v none (?m.109 false) (stLeft v (seen || false))input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Boolhr:(counterCfg cfg v (lower ++ true :: higher) (stLeft v seen) (higher.length + 1)).workTapeSymbols (counterTape v) = some (boolEmb true)⊢ (if (some (boolEmb true) == some 2) = true then counterAction v none 1 (stRight v seen) else counterAction v none (-1) (stLeft v (seen || some (boolEmb true) == some 1))) = counterAction v none (?m.109 true) (stLeft v (seen || true)) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Boolhr:(counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) (higher.length + 1)).workTapeSymbols (counterTape v) = some (boolEmb false)⊢ (if (some (boolEmb false) == some 2) = true then counterAction v none 1 (stRight v seen) else counterAction v none (-1) (stLeft v (seen || some (boolEmb false) == some 1))) = counterAction v none (?m.109 false) (stLeft v (seen || false))input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Boolhr:(counterCfg cfg v (lower ++ true :: higher) (stLeft v seen) (higher.length + 1)).workTapeSymbols (counterTape v) = some (boolEmb true)⊢ (if (some (boolEmb true) == some 2) = true then counterAction v none 1 (stRight v seen) else counterAction v none (-1) (stLeft v (seen || some (boolEmb true) == some 1))) = counterAction v none (?m.109 true) (stLeft v (seen || true)) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boollower:List Boolhigher:List Boolhr:(counterCfg cfg v (lower ++ true :: higher) (stLeft v false) (higher.length + 1)).workTapeSymbols (counterTape v) = some (boolEmb true)⊢ (if (some (boolEmb true) == some 2) = true then counterAction v none 1 (stRight v false) else counterAction v none (-1) (stLeft v (false || some (boolEmb true) == some 1))) = counterAction v none (?m.139 false true) (stLeft v (false || true))input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boollower:List Boolhigher:List Boolhr:(counterCfg cfg v (lower ++ true :: higher) (stLeft v true) (higher.length + 1)).workTapeSymbols (counterTape v) = some (boolEmb true)⊢ (if (some (boolEmb true) == some 2) = true then counterAction v none 1 (stRight v true) else counterAction v none (-1) (stLeft v (true || some (boolEmb true) == some 1))) = counterAction v none (?m.139 true true) (stLeft v (true || true)) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boollower:List Boolhigher:List Boolhr:(counterCfg cfg v (lower ++ false :: higher) (stLeft v false) (higher.length + 1)).workTapeSymbols (counterTape v) = some (boolEmb false)⊢ (if (some (boolEmb false) == some 2) = true then counterAction v none 1 (stRight v false) else counterAction v none (-1) (stLeft v (false || some (boolEmb false) == some 1))) = counterAction v none (?m.139 false false) (stLeft v (false || false))input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boollower:List Boolhigher:List Boolhr:(counterCfg cfg v (lower ++ false :: higher) (stLeft v true) (higher.length + 1)).workTapeSymbols (counterTape v) = some (boolEmb false)⊢ (if (some (boolEmb false) == some 2) = true then counterAction v none 1 (stRight v true) else counterAction v none (-1) (stLeft v (true || some (boolEmb false) == some 1))) = counterAction v none (?m.139 true false) (stLeft v (true || false))input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boollower:List Boolhigher:List Boolhr:(counterCfg cfg v (lower ++ true :: higher) (stLeft v false) (higher.length + 1)).workTapeSymbols (counterTape v) = some (boolEmb true)⊢ (if (some (boolEmb true) == some 2) = true then counterAction v none 1 (stRight v false) else counterAction v none (-1) (stLeft v (false || some (boolEmb true) == some 1))) = counterAction v none (?m.139 false true) (stLeft v (false || true))input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boollower:List Boolhigher:List Boolhr:(counterCfg cfg v (lower ++ true :: higher) (stLeft v true) (higher.length + 1)).workTapeSymbols (counterTape v) = some (boolEmb true)⊢ (if (some (boolEmb true) == some 2) = true then counterAction v none 1 (stRight v true) else counterAction v none (-1) (stLeft v (true || some (boolEmb true) == some 1))) = counterAction v none (?m.139 true true) (stLeft v (true || true)) All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolb:Boollower:List Boolhigher:List Bool⊢ ↑(higher.length + 1) + ↑(-1) = ↑higher.length All goals completed! 🐙

At the origin, the leftward scan turns right with its accumulated zero-test flag.

theorem left_zero_run {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (v seen : Bool) (bs : List Bool) : machine.step (counterCfg cfg v bs (stLeft v seen) 0) = counterCfg cfg v bs (stRight v seen) 1 ∧ machine.outputSymbol (counterCfg cfg v bs (stLeft v seen) 0) = none := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Bool⊢ step (counterCfg cfg v bs (stLeft v seen) 0) = counterCfg cfg v bs (stRight v seen) 1 ∧ outputSymbol (counterCfg cfg v bs (stLeft v seen) 0) = none input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Bool⊢ machine.tr (stLeft v seen) (counterCfg cfg v bs (stLeft v seen) 0).inputSymbol (counterCfg cfg v bs (stLeft v seen) 0).workTapeSymbols = counterAction v none 1 (stRight v seen)input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Bool⊢ ↑0 + ↑1 = ↑1 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Bool⊢ machine.tr (stLeft v seen) (counterCfg cfg v bs (stLeft v seen) 0).inputSymbol (counterCfg cfg v bs (stLeft v seen) 0).workTapeSymbols = counterAction v none 1 (stRight v seen) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Bool⊢ sweepLeft v seen (counterCfg cfg v bs (stLeft v seen) 0).workTapeSymbols = counterAction v none 1 (stRight v seen) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolhr:(counterCfg cfg v bs (stLeft v seen) 0).workTapeSymbols (counterTape v) = some 2⊢ sweepLeft v seen (counterCfg cfg v bs (stLeft v seen) 0).workTapeSymbols = counterAction v none 1 (stRight v seen) All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Bool⊢ ↑0 + ↑1 = ↑1 All goals completed! 🐙

The leftward scan accumulates the disjunction of all unvisited higher digits.

theorem configs_left {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (v : Bool) (higher : List Bool) : ∀ lower seen, machine.configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ higher) (stLeft v (seen || higher.any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = [] := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Bool⊢ ∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ higher) (stLeft v (seen || higher.any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Bool⊢ ∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ []) (stLeft v seen) [].length) [].length = counterCfg cfg v (lower ++ []) (stLeft v (seen || [].any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ []) (stLeft v seen) [].length) [].length = []input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Bool⊢ ∀ (head : Bool) (tail : List Bool), (∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ tail) (stLeft v seen) tail.length) tail.length = counterCfg cfg v (lower ++ tail) (stLeft v (seen || tail.any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ tail) (stLeft v seen) tail.length) tail.length = []) → ∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ head :: tail) (stLeft v seen) (head :: tail).length) (head :: tail).length = counterCfg cfg v (lower ++ head :: tail) (stLeft v (seen || (head :: tail).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ head :: tail) (stLeft v seen) (head :: tail).length) (head :: tail).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Bool⊢ ∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ []) (stLeft v seen) [].length) [].length = counterCfg cfg v (lower ++ []) (stLeft v (seen || [].any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ []) (stLeft v seen) [].length) [].length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Boollower:List Boolseen:Bool⊢ configs (counterCfg cfg v (lower ++ []) (stLeft v seen) [].length) [].length = counterCfg cfg v (lower ++ []) (stLeft v (seen || [].any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ []) (stLeft v seen) [].length) [].length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Boollower:List Boolseen:Bool⊢ True ∧ machine.outputString (counterCfg cfg v (lower ++ []) (stLeft v seen) 0) 0 = [] All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Bool⊢ ∀ (head : Bool) (tail : List Bool), (∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ tail) (stLeft v seen) tail.length) tail.length = counterCfg cfg v (lower ++ tail) (stLeft v (seen || tail.any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ tail) (stLeft v seen) tail.length) tail.length = []) → ∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ head :: tail) (stLeft v seen) (head :: tail).length) (head :: tail).length = counterCfg cfg v (lower ++ head :: tail) (stLeft v (seen || (head :: tail).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ head :: tail) (stLeft v seen) (head :: tail).length) (head :: tail).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ higher) (stLeft v (seen || higher.any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = []lower:List Boolseen:Bool⊢ configs (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (b :: higher).length) (b :: higher).length = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || (b :: higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (b :: higher).length) (b :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ higher) (stLeft v (seen || higher.any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = []lower:List Boolseen:Boolhs:step (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = none⊢ configs (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (b :: higher).length) (b :: higher).length = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || (b :: higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (b :: higher).length) (b :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ higher) (stLeft v (seen || higher.any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = []lower:List Boolseen:Boolhs:step (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ [b] ++ higher) (stLeft v (seen || b)) higher.length) higher.length = counterCfg cfg v (lower ++ [b] ++ higher) (stLeft v (seen || b || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ [b] ++ higher) (stLeft v (seen || b)) higher.length) higher.length = []⊢ configs (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (b :: higher).length) (b :: higher).length = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || (b :: higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (b :: higher).length) (b :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ higher) (stLeft v (seen || higher.any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = []lower:List Boolseen:Boolhs:step (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = []⊢ configs (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (b :: higher).length) (b :: higher).length = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || (b :: higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (b :: higher).length) (b :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ higher) (stLeft v (seen || higher.any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = []lower:List Boolseen:Boolhs:step (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = []⊢ configs (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (b :: higher).length) (b :: higher).length = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || (b :: higher).any id)) 0input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ higher) (stLeft v (seen || higher.any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = []lower:List Boolseen:Boolhs:step (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = []⊢ machine.outputString (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (b :: higher).length) (b :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ higher) (stLeft v (seen || higher.any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = []lower:List Boolseen:Boolhs:step (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = []⊢ configs (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (b :: higher).length) (b :: higher).length = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || (b :: higher).any id)) 0 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ higher) (stLeft v (seen || higher.any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = []lower:List Boolseen:Boolhs:step (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = []⊢ counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b || higher.any id)) 0 = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || (b :: higher).any id)) 0 All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ higher) (stLeft v (seen || higher.any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = []lower:List Boolseen:Boolhs:step (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = []⊢ machine.outputString (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (b :: higher).length) (b :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ higher) (stLeft v (seen || higher.any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = []lower:List Boolseen:Boolhs:step (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)⊢ machine.outputString (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (b :: higher).length) (b :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ higher) (stLeft v (seen || higher.any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = []lower:List Boolseen:Boolhs:step (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)⊢ machine.outputString current (higher.length + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ higher) (stLeft v (seen || higher.any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = []lower:List Boolseen:Boolhs:step (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)⊢ machine.outputString current 1 ++ machine.outputString (configs current 1) higher.length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ higher) (stLeft v (seen || higher.any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = []lower:List Boolseen:Boolhs:step (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)hone:machine.outputString current 1 = []⊢ machine.outputString current 1 ++ machine.outputString (configs current 1) higher.length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ higher) (stLeft v (seen || higher.any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = []lower:List Boolseen:Boolhs:step (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)hone:machine.outputString current 1 = []⊢ [] ++ machine.outputString (configs current 1) higher.length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ higher) (stLeft v (seen || higher.any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = []lower:List Boolseen:Boolhs:step (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)hone:machine.outputString current 1 = []⊢ [] ++ machine.outputString (step current) higher.length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ higher) (stLeft v (seen || higher.any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) higher.length = []lower:List Boolseen:Boolhs:step (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) higher.length = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (higher.length + 1)hone:machine.outputString current 1 = []⊢ [] ++ [] = [] All goals completed! 🐙

The rightward scan crosses every represented digit without inspecting its value.

theorem right_pos_run {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (v seen : Bool) (bs : List Bool) (j : ℕ) (hj : j < bs.length) : machine.step (counterCfg cfg v bs (stRight v seen) (j + 1)) = counterCfg cfg v bs (stRight v seen) (j + 2) ∧ machine.outputSymbol (counterCfg cfg v bs (stRight v seen) (j + 1)) = none := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolj:ℕhj:j < bs.length⊢ step (counterCfg cfg v bs (stRight v seen) (j + 1)) = counterCfg cfg v bs (stRight v seen) (j + 2) ∧ outputSymbol (counterCfg cfg v bs (stRight v seen) (j + 1)) = none input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolj:ℕhj:j < bs.length⊢ machine.tr (stRight v seen) (counterCfg cfg v bs (stRight v seen) (j + 1)).inputSymbol (counterCfg cfg v bs (stRight v seen) (j + 1)).workTapeSymbols = counterAction v none 1 (stRight v seen)input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolj:ℕhj:j < bs.length⊢ ↑(j + 1) + ↑1 = ↑(j + 2) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolj:ℕhj:j < bs.length⊢ machine.tr (stRight v seen) (counterCfg cfg v bs (stRight v seen) (j + 1)).inputSymbol (counterCfg cfg v bs (stRight v seen) (j + 1)).workTapeSymbols = counterAction v none 1 (stRight v seen) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolj:ℕhj:j < bs.length⊢ sweepRight v seen (counterCfg cfg v bs (stRight v seen) (j + 1)).workTapeSymbols = counterAction v none 1 (stRight v seen) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolj:ℕhj:j < bs.lengthhr:(counterCfg cfg v bs (stRight v seen) (j + 1)).workTapeSymbols (counterTape v) ≠ none⊢ sweepRight v seen (counterCfg cfg v bs (stRight v seen) (j + 1)).workTapeSymbols = counterAction v none 1 (stRight v seen) All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolj:ℕhj:j < bs.length⊢ ↑(j + 1) + ↑1 = ↑(j + 2) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolj:ℕhj:j < bs.length⊢ ↑j + 1 + 1 = ↑j + 2 All goals completed! 🐙

Reaching the right-hand blank completes the countdown.

theorem right_end_run {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (v seen : Bool) (bs : List Bool) : machine.step (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputSymbol (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) = none := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Bool⊢ step (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ outputSymbol (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) = none input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Bool⊢ machine.tr (stRight v seen) (counterCfg cfg v bs (stRight v seen) (bs.length + 1)).inputSymbol (counterCfg cfg v bs (stRight v seen) (bs.length + 1)).workTapeSymbols = counterAction v none 0 (afterDecrement v seen)input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Bool⊢ ↑(bs.length + 1) + ↑0 = ↑(bs.length + 1) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Bool⊢ machine.tr (stRight v seen) (counterCfg cfg v bs (stRight v seen) (bs.length + 1)).inputSymbol (counterCfg cfg v bs (stRight v seen) (bs.length + 1)).workTapeSymbols = counterAction v none 0 (afterDecrement v seen) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Bool⊢ sweepRight v seen (counterCfg cfg v bs (stRight v seen) (bs.length + 1)).workTapeSymbols = counterAction v none 0 (afterDecrement v seen) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolhr:(counterCfg cfg v bs (stRight v seen) (bs.length + 1)).workTapeSymbols (counterTape v) = none⊢ sweepRight v seen (counterCfg cfg v bs (stRight v seen) (bs.length + 1)).workTapeSymbols = counterAction v none 0 (afterDecrement v seen) All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Bool⊢ ↑(bs.length + 1) + ↑0 = ↑(bs.length + 1) All goals completed! 🐙

Starting inside the word, the rightward scan reaches its blank and resumes decoding.

theorem configs_right {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (v seen : Bool) (bs : List Bool) (t : ℕ) : ∀ p, 0 < p → p + t = bs.length + 1 → machine.configs (counterCfg cfg v bs (stRight v seen) p) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (t + 1) = [] := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt:ℕ⊢ ∀ (p : ℕ), 0 < p → p + t = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (t + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt:ℕ⊢ ∀ (p : ℕ), 0 < p → p + Nat.zero = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (Nat.zero + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (Nat.zero + 1) = []input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt:ℕ⊢ ∀ (n : ℕ), (∀ (p : ℕ), 0 < p → p + n = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (n + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (n + 1) = []) → ∀ (p : ℕ), 0 < p → p + n.succ = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (n.succ + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (n.succ + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt:ℕ⊢ ∀ (p : ℕ), 0 < p → p + Nat.zero = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (Nat.zero + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (Nat.zero + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt:ℕp:ℕa✝:0 < php:p + Nat.zero = bs.length + 1⊢ configs (counterCfg cfg v bs (stRight v seen) p) (Nat.zero + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (Nat.zero + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt:ℕp:ℕa✝:0 < php:p + Nat.zero = bs.length + 1he:p = bs.length + 1⊢ configs (counterCfg cfg v bs (stRight v seen) p) (Nat.zero + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (Nat.zero + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt:ℕa✝:0 < bs.length + 1hp:bs.length + 1 + Nat.zero = bs.length + 1⊢ configs (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) (Nat.zero + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) (Nat.zero + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt:ℕa✝:0 < bs.length + 1hp:bs.length + 1 + Nat.zero = bs.length + 1hs:step (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1)ho:outputSymbol (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) = none⊢ configs (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) (Nat.zero + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) (Nat.zero + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt:ℕa✝:0 < bs.length + 1hp:bs.length + 1 + Nat.zero = bs.length + 1hs:step (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1)ho:outputSymbol (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) = none⊢ configs (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) (Nat.zero + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1)input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt:ℕa✝:0 < bs.length + 1hp:bs.length + 1 + Nat.zero = bs.length + 1hs:step (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1)ho:outputSymbol (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) = none⊢ machine.outputString (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) (Nat.zero + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt:ℕa✝:0 < bs.length + 1hp:bs.length + 1 + Nat.zero = bs.length + 1hs:step (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1)ho:outputSymbol (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) = none⊢ configs (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) (Nat.zero + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt:ℕa✝:0 < bs.length + 1hp:bs.length + 1 + Nat.zero = bs.length + 1hs:step (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1)ho:outputSymbol (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) = none⊢ machine.outputString (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) (Nat.zero + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt:ℕa✝:0 < bs.length + 1hp:bs.length + 1 + Nat.zero = bs.length + 1hs:step (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1)ho:outputSymbol (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) = none⊢ machine.outputString (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) Nat.zero ++ none.toList = [] All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt:ℕ⊢ ∀ (n : ℕ), (∀ (p : ℕ), 0 < p → p + n = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (n + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (n + 1) = []) → ∀ (p : ℕ), 0 < p → p + n.succ = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (n.succ + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (n.succ + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt✝:ℕt:ℕih:∀ (p : ℕ), 0 < p → p + t = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (t + 1) = []p:ℕhp:0 < phpt:p + t.succ = bs.length + 1⊢ configs (counterCfg cfg v bs (stRight v seen) p) (t.succ + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (t.succ + 1) = [] cases p with input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt✝:ℕt:ℕih:∀ (p : ℕ), 0 < p → p + t = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (t + 1) = []hp:0 < 0hpt:0 + t.succ = bs.length + 1⊢ configs (counterCfg cfg v bs (stRight v seen) 0) (t.succ + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) 0) (t.succ + 1) = [] All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt✝:ℕt:ℕih:∀ (p : ℕ), 0 < p → p + t = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (t + 1) = []j:ℕhp:0 < j + 1hpt:j + 1 + t.succ = bs.length + 1⊢ configs (counterCfg cfg v bs (stRight v seen) (j + 1)) (t.succ + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) (j + 1)) (t.succ + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt✝:ℕt:ℕih:∀ (p : ℕ), 0 < p → p + t = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (t + 1) = []j:ℕhp:0 < j + 1hpt:j + 1 + t.succ = bs.length + 1hs:step (counterCfg cfg v bs (stRight v seen) (j + 1)) = counterCfg cfg v bs (stRight v seen) (j + 2)ho:outputSymbol (counterCfg cfg v bs (stRight v seen) (j + 1)) = none⊢ configs (counterCfg cfg v bs (stRight v seen) (j + 1)) (t.succ + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) (j + 1)) (t.succ + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt✝:ℕt:ℕih:∀ (p : ℕ), 0 < p → p + t = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (t + 1) = []j:ℕhp:0 < j + 1hpt:j + 1 + t.succ = bs.length + 1hs:step (counterCfg cfg v bs (stRight v seen) (j + 1)) = counterCfg cfg v bs (stRight v seen) (j + 2)ho:outputSymbol (counterCfg cfg v bs (stRight v seen) (j + 1)) = nonehc:configs (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1)hout:machine.outputString (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = []⊢ configs (counterCfg cfg v bs (stRight v seen) (j + 1)) (t.succ + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) (j + 1)) (t.succ + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt✝:ℕt:ℕih:∀ (p : ℕ), 0 < p → p + t = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (t + 1) = []j:ℕhp:0 < j + 1hpt:j + 1 + t.succ = bs.length + 1hs:step (counterCfg cfg v bs (stRight v seen) (j + 1)) = counterCfg cfg v bs (stRight v seen) (j + 2)ho:outputSymbol (counterCfg cfg v bs (stRight v seen) (j + 1)) = nonehc:configs (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1)hout:machine.outputString (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = []⊢ configs (counterCfg cfg v bs (stRight v seen) (j + 1)) (t.succ + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1)input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt✝:ℕt:ℕih:∀ (p : ℕ), 0 < p → p + t = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (t + 1) = []j:ℕhp:0 < j + 1hpt:j + 1 + t.succ = bs.length + 1hs:step (counterCfg cfg v bs (stRight v seen) (j + 1)) = counterCfg cfg v bs (stRight v seen) (j + 2)ho:outputSymbol (counterCfg cfg v bs (stRight v seen) (j + 1)) = nonehc:configs (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1)hout:machine.outputString (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = []⊢ machine.outputString (counterCfg cfg v bs (stRight v seen) (j + 1)) (t.succ + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt✝:ℕt:ℕih:∀ (p : ℕ), 0 < p → p + t = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (t + 1) = []j:ℕhp:0 < j + 1hpt:j + 1 + t.succ = bs.length + 1hs:step (counterCfg cfg v bs (stRight v seen) (j + 1)) = counterCfg cfg v bs (stRight v seen) (j + 2)ho:outputSymbol (counterCfg cfg v bs (stRight v seen) (j + 1)) = nonehc:configs (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1)hout:machine.outputString (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = []⊢ configs (counterCfg cfg v bs (stRight v seen) (j + 1)) (t.succ + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt✝:ℕt:ℕih:∀ (p : ℕ), 0 < p → p + t = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (t + 1) = []j:ℕhp:0 < j + 1hpt:j + 1 + t.succ = bs.length + 1hs:step (counterCfg cfg v bs (stRight v seen) (j + 1)) = counterCfg cfg v bs (stRight v seen) (j + 2)ho:outputSymbol (counterCfg cfg v bs (stRight v seen) (j + 1)) = nonehc:configs (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1)hout:machine.outputString (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = []⊢ machine.outputString (counterCfg cfg v bs (stRight v seen) (j + 1)) (t.succ + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt✝:ℕt:ℕih:∀ (p : ℕ), 0 < p → p + t = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (t + 1) = []j:ℕhp:0 < j + 1hpt:j + 1 + t.succ = bs.length + 1hs:step (counterCfg cfg v bs (stRight v seen) (j + 1)) = counterCfg cfg v bs (stRight v seen) (j + 2)ho:outputSymbol (counterCfg cfg v bs (stRight v seen) (j + 1)) = nonehc:configs (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1)hout:machine.outputString (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v bs (stRight v seen) (j + 1)⊢ machine.outputString (counterCfg cfg v bs (stRight v seen) (j + 1)) (t.succ + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt✝:ℕt:ℕih:∀ (p : ℕ), 0 < p → p + t = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (t + 1) = []j:ℕhp:0 < j + 1hpt:j + 1 + t.succ = bs.length + 1hs:step (counterCfg cfg v bs (stRight v seen) (j + 1)) = counterCfg cfg v bs (stRight v seen) (j + 2)ho:outputSymbol (counterCfg cfg v bs (stRight v seen) (j + 1)) = nonehc:configs (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1)hout:machine.outputString (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v bs (stRight v seen) (j + 1)⊢ machine.outputString current (t + 1 + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt✝:ℕt:ℕih:∀ (p : ℕ), 0 < p → p + t = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (t + 1) = []j:ℕhp:0 < j + 1hpt:j + 1 + t.succ = bs.length + 1hs:step (counterCfg cfg v bs (stRight v seen) (j + 1)) = counterCfg cfg v bs (stRight v seen) (j + 2)ho:outputSymbol (counterCfg cfg v bs (stRight v seen) (j + 1)) = nonehc:configs (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1)hout:machine.outputString (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v bs (stRight v seen) (j + 1)⊢ machine.outputString current 1 ++ machine.outputString (configs current 1) (t + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt✝:ℕt:ℕih:∀ (p : ℕ), 0 < p → p + t = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (t + 1) = []j:ℕhp:0 < j + 1hpt:j + 1 + t.succ = bs.length + 1hs:step (counterCfg cfg v bs (stRight v seen) (j + 1)) = counterCfg cfg v bs (stRight v seen) (j + 2)ho:outputSymbol (counterCfg cfg v bs (stRight v seen) (j + 1)) = nonehc:configs (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1)hout:machine.outputString (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v bs (stRight v seen) (j + 1)hone:machine.outputString current 1 = []⊢ machine.outputString current 1 ++ machine.outputString (configs current 1) (t + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt✝:ℕt:ℕih:∀ (p : ℕ), 0 < p → p + t = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (t + 1) = []j:ℕhp:0 < j + 1hpt:j + 1 + t.succ = bs.length + 1hs:step (counterCfg cfg v bs (stRight v seen) (j + 1)) = counterCfg cfg v bs (stRight v seen) (j + 2)ho:outputSymbol (counterCfg cfg v bs (stRight v seen) (j + 1)) = nonehc:configs (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1)hout:machine.outputString (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v bs (stRight v seen) (j + 1)hone:machine.outputString current 1 = []⊢ [] ++ machine.outputString (configs current 1) (t + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt✝:ℕt:ℕih:∀ (p : ℕ), 0 < p → p + t = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (t + 1) = []j:ℕhp:0 < j + 1hpt:j + 1 + t.succ = bs.length + 1hs:step (counterCfg cfg v bs (stRight v seen) (j + 1)) = counterCfg cfg v bs (stRight v seen) (j + 2)ho:outputSymbol (counterCfg cfg v bs (stRight v seen) (j + 1)) = nonehc:configs (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1)hout:machine.outputString (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v bs (stRight v seen) (j + 1)hone:machine.outputString current 1 = []⊢ [] ++ machine.outputString (step current) (t + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolt✝:ℕt:ℕih:∀ (p : ℕ), 0 < p → p + t = bs.length + 1 → configs (counterCfg cfg v bs (stRight v seen) p) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stRight v seen) p) (t + 1) = []j:ℕhp:0 < j + 1hpt:j + 1 + t.succ = bs.length + 1hs:step (counterCfg cfg v bs (stRight v seen) (j + 1)) = counterCfg cfg v bs (stRight v seen) (j + 2)ho:outputSymbol (counterCfg cfg v bs (stRight v seen) (j + 1)) = nonehc:configs (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1)hout:machine.outputString (counterCfg cfg v bs (stRight v seen) (j + 2)) (t + 1) = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v bs (stRight v seen) (j + 1)hone:machine.outputString current 1 = []⊢ [] ++ [] = [] All goals completed! 🐙

Borrowing across a zero sets that digit and continues toward the origin.

theorem borrow_false_run {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (v seen : Bool) (lower higher : List Bool) : machine.step (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length ∧ machine.outputSymbol (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = none := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Bool⊢ step (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length ∧ outputSymbol (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = none input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Bool⊢ machine.tr (stBorrow v seen) (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)).inputSymbol (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)).workTapeSymbols = counterAction v (some (some (boolEmb true))) (-1) (stBorrow v true)input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Bool⊢ ↑(higher.length + 1) + ↑(-1) = ↑higher.lengthinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Bool⊢ Function.update (wordTape (lower ++ false :: higher)) (↑(higher.length + 1)) (some (boolEmb true)) = wordTape (lower ++ true :: higher) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Bool⊢ machine.tr (stBorrow v seen) (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)).inputSymbol (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)).workTapeSymbols = counterAction v (some (some (boolEmb true))) (-1) (stBorrow v true) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Bool⊢ borrow v seen (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)).workTapeSymbols = counterAction v (some (some (boolEmb true))) (-1) (stBorrow v true) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Boolhr:(counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)).workTapeSymbols (counterTape v) = some (boolEmb false)⊢ borrow v seen (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)).workTapeSymbols = counterAction v (some (some (boolEmb true))) (-1) (stBorrow v true) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Boolhr:(counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)).workTapeSymbols (counterTape v) = some (boolEmb false)⊢ (if (some (boolEmb false) == some 2) = true then finish false else if (some (boolEmb false) == some 1) = true then counterAction v (some (some 0)) (-1) (stLeft v seen) else counterAction v (some (some 1)) (-1) (stBorrow v true)) = counterAction v (some (some (boolEmb true))) (-1) (stBorrow v true) All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Bool⊢ ↑(higher.length + 1) + ↑(-1) = ↑higher.length All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Bool⊢ Function.update (wordTape (lower ++ false :: higher)) (↑(higher.length + 1)) (some (boolEmb true)) = wordTape (lower ++ true :: higher) All goals completed! 🐙

Borrowing stops at the first one, clearing it before the leftward scan.

theorem borrow_true_run {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (v seen : Bool) (lower higher : List Bool) : machine.step (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length ∧ machine.outputSymbol (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = none := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Bool⊢ step (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length ∧ outputSymbol (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = none input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Bool⊢ machine.tr (stBorrow v seen) (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)).inputSymbol (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)).workTapeSymbols = counterAction v (some (some (boolEmb false))) (-1) (stLeft v seen)input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Bool⊢ ↑(higher.length + 1) + ↑(-1) = ↑higher.lengthinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Bool⊢ Function.update (wordTape (lower ++ true :: higher)) (↑(higher.length + 1)) (some (boolEmb false)) = wordTape (lower ++ false :: higher) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Bool⊢ machine.tr (stBorrow v seen) (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)).inputSymbol (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)).workTapeSymbols = counterAction v (some (some (boolEmb false))) (-1) (stLeft v seen) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Bool⊢ borrow v seen (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)).workTapeSymbols = counterAction v (some (some (boolEmb false))) (-1) (stLeft v seen) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Boolhr:(counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)).workTapeSymbols (counterTape v) = some (boolEmb true)⊢ borrow v seen (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)).workTapeSymbols = counterAction v (some (some (boolEmb false))) (-1) (stLeft v seen) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Boolhr:(counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)).workTapeSymbols (counterTape v) = some (boolEmb true)⊢ (if (some (boolEmb true) == some 2) = true then finish false else if (some (boolEmb true) == some 1) = true then counterAction v (some (some 0)) (-1) (stLeft v seen) else counterAction v (some (some 1)) (-1) (stBorrow v true)) = counterAction v (some (some (boolEmb false))) (-1) (stLeft v seen) All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Bool⊢ ↑(higher.length + 1) + ↑(-1) = ↑higher.length All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boollower:List Boolhigher:List Bool⊢ Function.update (wordTape (lower ++ true :: higher)) (↑(higher.length + 1)) (some (boolEmb false)) = wordTape (lower ++ false :: higher) All goals completed! 🐙

Borrowing and the subsequent scan together visit each remaining digit exactly once.

theorem configs_borrow {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (v : Bool) (higher : List Bool) : ∀ lower seen, 0 < Counter.value higher → machine.configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = [] := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Bool⊢ ∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Bool⊢ ∀ (lower : List Bool) (seen : Bool), 0 < Counter.value [] → configs (counterCfg cfg v (lower ++ []) (stBorrow v seen) [].length) [].length = counterCfg cfg v (lower ++ Counter.decrement []) (stLeft v (seen || (Counter.decrement []).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ []) (stBorrow v seen) [].length) [].length = []input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Bool⊢ ∀ (head : Bool) (tail : List Bool), (∀ (lower : List Bool) (seen : Bool), 0 < Counter.value tail → configs (counterCfg cfg v (lower ++ tail) (stBorrow v seen) tail.length) tail.length = counterCfg cfg v (lower ++ Counter.decrement tail) (stLeft v (seen || (Counter.decrement tail).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ tail) (stBorrow v seen) tail.length) tail.length = []) → ∀ (lower : List Bool) (seen : Bool), 0 < Counter.value (head :: tail) → configs (counterCfg cfg v (lower ++ head :: tail) (stBorrow v seen) (head :: tail).length) (head :: tail).length = counterCfg cfg v (lower ++ Counter.decrement (head :: tail)) (stLeft v (seen || (Counter.decrement (head :: tail)).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ head :: tail) (stBorrow v seen) (head :: tail).length) (head :: tail).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Bool⊢ ∀ (lower : List Bool) (seen : Bool), 0 < Counter.value [] → configs (counterCfg cfg v (lower ++ []) (stBorrow v seen) [].length) [].length = counterCfg cfg v (lower ++ Counter.decrement []) (stLeft v (seen || (Counter.decrement []).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ []) (stBorrow v seen) [].length) [].length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Boollower:List Boolseen:Boolh:0 < Counter.value []⊢ configs (counterCfg cfg v (lower ++ []) (stBorrow v seen) [].length) [].length = counterCfg cfg v (lower ++ Counter.decrement []) (stLeft v (seen || (Counter.decrement []).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ []) (stBorrow v seen) [].length) [].length = [] All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Bool⊢ ∀ (head : Bool) (tail : List Bool), (∀ (lower : List Bool) (seen : Bool), 0 < Counter.value tail → configs (counterCfg cfg v (lower ++ tail) (stBorrow v seen) tail.length) tail.length = counterCfg cfg v (lower ++ Counter.decrement tail) (stLeft v (seen || (Counter.decrement tail).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ tail) (stBorrow v seen) tail.length) tail.length = []) → ∀ (lower : List Bool) (seen : Bool), 0 < Counter.value (head :: tail) → configs (counterCfg cfg v (lower ++ head :: tail) (stBorrow v seen) (head :: tail).length) (head :: tail).length = counterCfg cfg v (lower ++ Counter.decrement (head :: tail)) (stLeft v (seen || (Counter.decrement (head :: tail)).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ head :: tail) (stBorrow v seen) (head :: tail).length) (head :: tail).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (b :: higher)⊢ configs (counterCfg cfg v (lower ++ b :: higher) (stBorrow v seen) (b :: higher).length) (b :: higher).length = counterCfg cfg v (lower ++ Counter.decrement (b :: higher)) (stLeft v (seen || (Counter.decrement (b :: higher)).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ b :: higher) (stBorrow v seen) (b :: higher).length) (b :: higher).length = [] cases b with input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (false :: higher)⊢ configs (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (false :: higher).length) (false :: higher).length = counterCfg cfg v (lower ++ Counter.decrement (false :: higher)) (stLeft v (seen || (Counter.decrement (false :: higher)).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (false :: higher).length) (false :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (false :: higher)hh:0 < Counter.value higher⊢ configs (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (false :: higher).length) (false :: higher).length = counterCfg cfg v (lower ++ Counter.decrement (false :: higher)) (stLeft v (seen || (Counter.decrement (false :: higher)).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (false :: higher).length) (false :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (false :: higher)hh:0 < Counter.value higherhs:step (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = none⊢ configs (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (false :: higher).length) (false :: higher).length = counterCfg cfg v (lower ++ Counter.decrement (false :: higher)) (stLeft v (seen || (Counter.decrement (false :: higher)).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (false :: higher).length) (false :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (false :: higher)hh:0 < Counter.value higherhs:step (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ [true] ++ higher) (stBorrow v true) higher.length) higher.length = counterCfg cfg v (lower ++ [true] ++ Counter.decrement higher) (stLeft v (true || (Counter.decrement higher).any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ [true] ++ higher) (stBorrow v true) higher.length) higher.length = []⊢ configs (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (false :: higher).length) (false :: higher).length = counterCfg cfg v (lower ++ Counter.decrement (false :: higher)) (stLeft v (seen || (Counter.decrement (false :: higher)).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (false :: higher).length) (false :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (false :: higher)hh:0 < Counter.value higherhs:step (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = counterCfg cfg v (lower ++ true :: Counter.decrement higher) (stLeft v true) 0hout:machine.outputString (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = []⊢ configs (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (false :: higher).length) (false :: higher).length = counterCfg cfg v (lower ++ Counter.decrement (false :: higher)) (stLeft v (seen || (Counter.decrement (false :: higher)).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (false :: higher).length) (false :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (false :: higher)hh:0 < Counter.value higherhs:step (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = counterCfg cfg v (lower ++ true :: Counter.decrement higher) (stLeft v true) 0hout:machine.outputString (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = []⊢ configs (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (false :: higher).length) (false :: higher).length = counterCfg cfg v (lower ++ Counter.decrement (false :: higher)) (stLeft v (seen || (Counter.decrement (false :: higher)).any id)) 0input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (false :: higher)hh:0 < Counter.value higherhs:step (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = counterCfg cfg v (lower ++ true :: Counter.decrement higher) (stLeft v true) 0hout:machine.outputString (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = []⊢ machine.outputString (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (false :: higher).length) (false :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (false :: higher)hh:0 < Counter.value higherhs:step (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = counterCfg cfg v (lower ++ true :: Counter.decrement higher) (stLeft v true) 0hout:machine.outputString (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = []⊢ configs (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (false :: higher).length) (false :: higher).length = counterCfg cfg v (lower ++ Counter.decrement (false :: higher)) (stLeft v (seen || (Counter.decrement (false :: higher)).any id)) 0 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (false :: higher)hh:0 < Counter.value higherhs:step (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = counterCfg cfg v (lower ++ true :: Counter.decrement higher) (stLeft v true) 0hout:machine.outputString (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = []⊢ counterCfg cfg v (lower ++ true :: Counter.decrement higher) (stLeft v true) 0 = counterCfg cfg v (lower ++ Counter.decrement (false :: higher)) (stLeft v (seen || (Counter.decrement (false :: higher)).any id)) 0 All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (false :: higher)hh:0 < Counter.value higherhs:step (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = counterCfg cfg v (lower ++ true :: Counter.decrement higher) (stLeft v true) 0hout:machine.outputString (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = []⊢ machine.outputString (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (false :: higher).length) (false :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (false :: higher)hh:0 < Counter.value higherhs:step (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = counterCfg cfg v (lower ++ true :: Counter.decrement higher) (stLeft v true) 0hout:machine.outputString (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)⊢ machine.outputString (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (false :: higher).length) (false :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (false :: higher)hh:0 < Counter.value higherhs:step (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = counterCfg cfg v (lower ++ true :: Counter.decrement higher) (stLeft v true) 0hout:machine.outputString (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)⊢ machine.outputString current (higher.length + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (false :: higher)hh:0 < Counter.value higherhs:step (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = counterCfg cfg v (lower ++ true :: Counter.decrement higher) (stLeft v true) 0hout:machine.outputString (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)⊢ machine.outputString current 1 ++ machine.outputString (configs current 1) higher.length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (false :: higher)hh:0 < Counter.value higherhs:step (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = counterCfg cfg v (lower ++ true :: Counter.decrement higher) (stLeft v true) 0hout:machine.outputString (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)hone:machine.outputString current 1 = []⊢ machine.outputString current 1 ++ machine.outputString (configs current 1) higher.length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (false :: higher)hh:0 < Counter.value higherhs:step (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = counterCfg cfg v (lower ++ true :: Counter.decrement higher) (stLeft v true) 0hout:machine.outputString (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)hone:machine.outputString current 1 = []⊢ [] ++ machine.outputString (configs current 1) higher.length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (false :: higher)hh:0 < Counter.value higherhs:step (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = counterCfg cfg v (lower ++ true :: Counter.decrement higher) (stLeft v true) 0hout:machine.outputString (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)hone:machine.outputString current 1 = []⊢ [] ++ machine.outputString (step current) higher.length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (false :: higher)hh:0 < Counter.value higherhs:step (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = counterCfg cfg v (lower ++ true :: Counter.decrement higher) (stLeft v true) 0hout:machine.outputString (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) higher.length = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (higher.length + 1)hone:machine.outputString current 1 = []⊢ [] ++ [] = [] All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (true :: higher)⊢ configs (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (true :: higher).length) (true :: higher).length = counterCfg cfg v (lower ++ Counter.decrement (true :: higher)) (stLeft v (seen || (Counter.decrement (true :: higher)).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (true :: higher).length) (true :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (true :: higher)hs:step (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = none⊢ configs (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (true :: higher).length) (true :: higher).length = counterCfg cfg v (lower ++ Counter.decrement (true :: higher)) (stLeft v (seen || (Counter.decrement (true :: higher)).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (true :: higher).length) (true :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (true :: higher)hs:step (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ [false] ++ higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ [false] ++ higher) (stLeft v (seen || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ [false] ++ higher) (stLeft v seen) higher.length) higher.length = []⊢ configs (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (true :: higher).length) (true :: higher).length = counterCfg cfg v (lower ++ Counter.decrement (true :: higher)) (stLeft v (seen || (Counter.decrement (true :: higher)).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (true :: higher).length) (true :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (true :: higher)hs:step (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ false :: higher) (stLeft v (seen || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = []⊢ configs (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (true :: higher).length) (true :: higher).length = counterCfg cfg v (lower ++ Counter.decrement (true :: higher)) (stLeft v (seen || (Counter.decrement (true :: higher)).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (true :: higher).length) (true :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (true :: higher)hs:step (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ false :: higher) (stLeft v (seen || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = []⊢ configs (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (true :: higher).length) (true :: higher).length = counterCfg cfg v (lower ++ Counter.decrement (true :: higher)) (stLeft v (seen || (Counter.decrement (true :: higher)).any id)) 0input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (true :: higher)hs:step (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ false :: higher) (stLeft v (seen || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = []⊢ machine.outputString (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (true :: higher).length) (true :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (true :: higher)hs:step (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ false :: higher) (stLeft v (seen || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = []⊢ configs (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (true :: higher).length) (true :: higher).length = counterCfg cfg v (lower ++ Counter.decrement (true :: higher)) (stLeft v (seen || (Counter.decrement (true :: higher)).any id)) 0 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (true :: higher)hs:step (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ false :: higher) (stLeft v (seen || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = []⊢ counterCfg cfg v (lower ++ false :: higher) (stLeft v (seen || higher.any id)) 0 = counterCfg cfg v (lower ++ Counter.decrement (true :: higher)) (stLeft v (seen || (Counter.decrement (true :: higher)).any id)) 0 All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (true :: higher)hs:step (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ false :: higher) (stLeft v (seen || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = []⊢ machine.outputString (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (true :: higher).length) (true :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (true :: higher)hs:step (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ false :: higher) (stLeft v (seen || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)⊢ machine.outputString (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (true :: higher).length) (true :: higher).length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (true :: higher)hs:step (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ false :: higher) (stLeft v (seen || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)⊢ machine.outputString current (higher.length + 1) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (true :: higher)hs:step (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ false :: higher) (stLeft v (seen || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)⊢ machine.outputString current 1 ++ machine.outputString (configs current 1) higher.length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (true :: higher)hs:step (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ false :: higher) (stLeft v (seen || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)hone:machine.outputString current 1 = []⊢ machine.outputString current 1 ++ machine.outputString (configs current 1) higher.length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (true :: higher)hs:step (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ false :: higher) (stLeft v (seen || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)hone:machine.outputString current 1 = []⊢ [] ++ machine.outputString (configs current 1) higher.length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (true :: higher)hs:step (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ false :: higher) (stLeft v (seen || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)hone:machine.outputString current 1 = []⊢ [] ++ machine.outputString (step current) higher.length = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = counterCfg cfg v (lower ++ Counter.decrement higher) (stLeft v (seen || (Counter.decrement higher).any id)) 0 ∧ machine.outputString (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) higher.length = []lower:List Boolseen:Boolh:0 < Counter.value (true :: higher)hs:step (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.lengthho:outputSymbol (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)) = nonehc:configs (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = counterCfg cfg v (lower ++ false :: higher) (stLeft v (seen || higher.any id)) 0hout:machine.outputString (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) higher.length = []current:Cfg 4 (Fin 3) Control input := counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (higher.length + 1)hone:machine.outputString current 1 = []⊢ [] ++ [] = [] All goals completed! 🐙

A single silent transition is a one-step execution with empty output.

theorem configs_output_one {input : List (Fin 3)} (cfg next : Cfg 4 (Fin 3) Control input) (hs : machine.step cfg = next) (ho : machine.outputSymbol cfg = none) : machine.configs cfg 1 = next ∧ machine.outputString cfg 1 = [] := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputnext:Cfg 4 (Fin 3) Control inpuths:step cfg = nextho:outputSymbol cfg = none⊢ configs cfg 1 = next ∧ machine.outputString cfg 1 = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputnext:Cfg 4 (Fin 3) Control inpuths:step cfg = nextho:outputSymbol cfg = none⊢ configs cfg 1 = nextinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputnext:Cfg 4 (Fin 3) Control inpuths:step cfg = nextho:outputSymbol cfg = none⊢ machine.outputString cfg 1 = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputnext:Cfg 4 (Fin 3) Control inpuths:step cfg = nextho:outputSymbol cfg = none⊢ configs cfg 1 = next All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputnext:Cfg 4 (Fin 3) Control inpuths:step cfg = nextho:outputSymbol cfg = none⊢ machine.outputString cfg 1 = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputnext:Cfg 4 (Fin 3) Control inpuths:step cfg = nextho:outputSymbol cfg = none⊢ machine.outputString cfg 0 ++ none.toList = [] All goals completed! 🐙

A positive fixed-width counter decrements and tests its result in twice its width plus three transitions, preserving the input and all other tapes and emitting nothing.

theorem configs_decrement {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (v : Bool) (bs : List Bool) (hbs : 0 < Counter.value bs) : machine.configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = counterCfg cfg v (Counter.decrement bs) (afterDecrement v ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = [] := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolhbs:0 < Counter.value bs⊢ configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = counterCfg cfg v (Counter.decrement bs) (afterDecrement v ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolhbs:0 < Counter.value bshentry:configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) 1 = counterCfg cfg v bs (stBorrow v false) bs.length ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) 1 = []⊢ configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = counterCfg cfg v (Counter.decrement bs) (afterDecrement v ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolhbs:0 < Counter.value bshentry:configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) 1 = counterCfg cfg v bs (stBorrow v false) bs.length ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) 1 = []hborrow:configs (counterCfg cfg v ([] ++ bs) (stBorrow v false) bs.length) bs.length = counterCfg cfg v ([] ++ Counter.decrement bs) (stLeft v (false || (Counter.decrement bs).any id)) 0 ∧ machine.outputString (counterCfg cfg v ([] ++ bs) (stBorrow v false) bs.length) bs.length = []⊢ configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = counterCfg cfg v (Counter.decrement bs) (afterDecrement v ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolhbs:0 < Counter.value bshentry:configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) 1 = counterCfg cfg v bs (stBorrow v false) bs.length ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) 1 = []hborrow:configs (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0 ∧ machine.outputString (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = []⊢ configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = counterCfg cfg v (Counter.decrement bs) (afterDecrement v ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolhbs:0 < Counter.value bshentry:configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) 1 = counterCfg cfg v bs (stBorrow v false) bs.length ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) 1 = []hborrow:configs (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0 ∧ machine.outputString (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = []hz:step (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) = counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1hoz:outputSymbol (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) = none⊢ configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = counterCfg cfg v (Counter.decrement bs) (afterDecrement v ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolhbs:0 < Counter.value bshentry:configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) 1 = counterCfg cfg v bs (stBorrow v false) bs.length ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) 1 = []hborrow:configs (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0 ∧ machine.outputString (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = []hz:step (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) = counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1hoz:outputSymbol (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) = nonehturn:configs (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) 1 = counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1 ∧ machine.outputString (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) 1 = []⊢ configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = counterCfg cfg v (Counter.decrement bs) (afterDecrement v ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolhbs:0 < Counter.value bshentry:configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) 1 = counterCfg cfg v bs (stBorrow v false) bs.length ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) 1 = []hborrow:configs (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0 ∧ machine.outputString (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = []hz:step (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) = counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1hoz:outputSymbol (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) = nonehturn:configs (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) 1 = counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1 ∧ machine.outputString (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) 1 = []hright:configs (counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1) (bs.length + 1) = counterCfg cfg v (Counter.decrement bs) (afterDecrement v ((Counter.decrement bs).any id)) ((Counter.decrement bs).length + 1) ∧ machine.outputString (counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1) (bs.length + 1) = []⊢ configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = counterCfg cfg v (Counter.decrement bs) (afterDecrement v ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolhbs:0 < Counter.value bshentry:configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) 1 = counterCfg cfg v bs (stBorrow v false) bs.length ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) 1 = []hborrow:configs (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0 ∧ machine.outputString (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = []hz:step (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) = counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1hoz:outputSymbol (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) = nonehturn:configs (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) 1 = counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1 ∧ machine.outputString (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) 1 = []hright:configs (counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1) (bs.length + 1) = counterCfg cfg v (Counter.decrement bs) (afterDecrement v ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1) (bs.length + 1) = []⊢ configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = counterCfg cfg v (Counter.decrement bs) (afterDecrement v ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolhbs:0 < Counter.value bshentry:configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) 1 = counterCfg cfg v bs (stBorrow v false) bs.length ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) 1 = []hborrow:configs (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0 ∧ machine.outputString (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = []hz:step (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) = counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1hoz:outputSymbol (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) = nonehturn:configs (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) 1 = counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1 ∧ machine.outputString (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) 1 = []hright:configs (counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1) (bs.length + 1) = counterCfg cfg v (Counter.decrement bs) (afterDecrement v ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1) (bs.length + 1) = []hfirst:configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (1 + bs.length) = counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0 ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (1 + bs.length) = []⊢ configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = counterCfg cfg v (Counter.decrement bs) (afterDecrement v ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolhbs:0 < Counter.value bshentry:configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) 1 = counterCfg cfg v bs (stBorrow v false) bs.length ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) 1 = []hborrow:configs (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0 ∧ machine.outputString (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = []hz:step (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) = counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1hoz:outputSymbol (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) = nonehturn:configs (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) 1 = counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1 ∧ machine.outputString (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) 1 = []hright:configs (counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1) (bs.length + 1) = counterCfg cfg v (Counter.decrement bs) (afterDecrement v ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1) (bs.length + 1) = []hfirst:configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (1 + bs.length) = counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0 ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (1 + bs.length) = []hsecond:configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (1 + bs.length + 1) = counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1 ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (1 + bs.length + 1) = []⊢ configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = counterCfg cfg v (Counter.decrement bs) (afterDecrement v ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = [] input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolhbs:0 < Counter.value bshentry:configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) 1 = counterCfg cfg v bs (stBorrow v false) bs.length ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) 1 = []hborrow:configs (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0 ∧ machine.outputString (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = []hz:step (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) = counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1hoz:outputSymbol (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) = nonehturn:configs (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) 1 = counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1 ∧ machine.outputString (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) 1 = []hright:configs (counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1) (bs.length + 1) = counterCfg cfg v (Counter.decrement bs) (afterDecrement v ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1) (bs.length + 1) = []hfirst:configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (1 + bs.length) = counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0 ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (1 + bs.length) = []hsecond:configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (1 + bs.length + 1) = counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1 ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (1 + bs.length + 1) = []hall:configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (1 + bs.length + 1 + (bs.length + 1)) = counterCfg cfg v (Counter.decrement bs) (afterDecrement v ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (1 + bs.length + 1 + (bs.length + 1)) = []⊢ configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = counterCfg cfg v (Counter.decrement bs) (afterDecrement v ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = [] simpa only [show 1 + bs.length + 1 + (bs.length + 1) = 2 * bs.length + 3 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolhbs:0 < Counter.value bs⊢ configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = counterCfg cfg v (Counter.decrement bs) (afterDecrement v ((Counter.decrement bs).any id)) (bs.length + 1) ∧ machine.outputString (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) (2 * bs.length + 3) = [] All goals completed! 🐙] using hall

A bounded starting configuration followed by a bounded tail gives a bounded successor run.

theorem headBound_succ {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (n width : ℕ) (hcfg : HeadBound width cfg) (hnext : ∀ t ≤ n, HeadBound width (machine.configs (machine.step cfg) t)) (t : ℕ) (ht : t ≤ n + 1) : HeadBound width (machine.configs cfg t) := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputn:ℕwidth:ℕhcfg:HeadBound width cfghnext:∀ t ≤ n, HeadBound width (configs (step cfg) t)t:ℕht:t ≤ n + 1⊢ HeadBound width (configs cfg t) cases t with input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputn:ℕwidth:ℕhcfg:HeadBound width cfghnext:∀ t ≤ n, HeadBound width (configs (step cfg) t)ht:0 ≤ n + 1⊢ HeadBound width (configs cfg 0) All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputn:ℕwidth:ℕhcfg:HeadBound width cfghnext:∀ t ≤ n, HeadBound width (configs (step cfg) t)t:ℕht:t + 1 ≤ n + 1⊢ HeadBound width (configs cfg (t + 1)) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputn:ℕwidth:ℕhcfg:HeadBound width cfghnext:∀ t ≤ n, HeadBound width (configs (step cfg) t)t:ℕht:t + 1 ≤ n + 1⊢ HeadBound width (configs (step cfg) t) exact hnext t (input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputn:ℕwidth:ℕhcfg:HeadBound width cfghnext:∀ t ≤ n, HeadBound width (configs (step cfg) t)t:ℕht:t + 1 ≤ n + 1⊢ t ≤ n All goals completed! 🐙)

Every prefix of the leftward scan stays between the origin and its starting head.

theorem configs_left_headBound {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (v : Bool) (higher : List Bool) (width : ℕ) (hcfg : HeadBound width cfg) : ∀ lower seen, higher.length ≤ width → ∀ t ≤ higher.length, HeadBound width (machine.configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) t) := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Boolwidth:ℕhcfg:HeadBound width cfg⊢ ∀ (lower : List Bool) (seen : Bool), higher.length ≤ width → ∀ t ≤ higher.length, HeadBound width (configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Boolwidth:ℕhcfg:HeadBound width cfg⊢ ∀ (lower : List Bool) (seen : Bool), [].length ≤ width → ∀ t ≤ [].length, HeadBound width (configs (counterCfg cfg v (lower ++ []) (stLeft v seen) [].length) t)input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Boolwidth:ℕhcfg:HeadBound width cfg⊢ ∀ (head : Bool) (tail : List Bool), (∀ (lower : List Bool) (seen : Bool), tail.length ≤ width → ∀ t ≤ tail.length, HeadBound width (configs (counterCfg cfg v (lower ++ tail) (stLeft v seen) tail.length) t)) → ∀ (lower : List Bool) (seen : Bool), (head :: tail).length ≤ width → ∀ t ≤ (head :: tail).length, HeadBound width (configs (counterCfg cfg v (lower ++ head :: tail) (stLeft v seen) (head :: tail).length) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Boolwidth:ℕhcfg:HeadBound width cfg⊢ ∀ (lower : List Bool) (seen : Bool), [].length ≤ width → ∀ t ≤ [].length, HeadBound width (configs (counterCfg cfg v (lower ++ []) (stLeft v seen) [].length) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Boolwidth:ℕhcfg:HeadBound width cfglower:List Boolseen:Boolhw:[].length ≤ widtht:ℕht:t ≤ [].length⊢ HeadBound width (configs (counterCfg cfg v (lower ++ []) (stLeft v seen) [].length) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Boolwidth:ℕhcfg:HeadBound width cfglower:List Boolseen:Boolhw:[].length ≤ widtht:ℕht:t ≤ [].lengthhe:t = 0⊢ HeadBound width (configs (counterCfg cfg v (lower ++ []) (stLeft v seen) [].length) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Boolwidth:ℕhcfg:HeadBound width cfglower:List Boolseen:Boolhw:[].length ≤ widthht:0 ≤ [].length⊢ HeadBound width (configs (counterCfg cfg v (lower ++ []) (stLeft v seen) [].length) 0) All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Boolwidth:ℕhcfg:HeadBound width cfg⊢ ∀ (head : Bool) (tail : List Bool), (∀ (lower : List Bool) (seen : Bool), tail.length ≤ width → ∀ t ≤ tail.length, HeadBound width (configs (counterCfg cfg v (lower ++ tail) (stLeft v seen) tail.length) t)) → ∀ (lower : List Bool) (seen : Bool), (head :: tail).length ≤ width → ∀ t ≤ (head :: tail).length, HeadBound width (configs (counterCfg cfg v (lower ++ head :: tail) (stLeft v seen) (head :: tail).length) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolwidth:ℕhcfg:HeadBound width cfgb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), higher.length ≤ width → ∀ t ≤ higher.length, HeadBound width (configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) t)lower:List Boolseen:Boolhw:(b :: higher).length ≤ widtht:ℕht:t ≤ (b :: higher).length⊢ HeadBound width (configs (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (b :: higher).length) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolwidth:ℕhcfg:HeadBound width cfgb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), higher.length ≤ width → ∀ t ≤ higher.length, HeadBound width (configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) t)lower:List Boolseen:Boolhw:(b :: higher).length ≤ widtht:ℕht:t ≤ (b :: higher).length⊢ ∀ t ≤ higher.length, HeadBound width (configs (step (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (b :: higher).length)) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolwidth:ℕhcfg:HeadBound width cfgb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), higher.length ≤ width → ∀ t ≤ higher.length, HeadBound width (configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) t)lower:List Boolseen:Boolhw:(b :: higher).length ≤ widtht:ℕht:t ≤ (b :: higher).lengthr:ℕhr:r ≤ higher.length⊢ HeadBound width (configs (step (counterCfg cfg v (lower ++ b :: higher) (stLeft v seen) (b :: higher).length)) r) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolwidth:ℕhcfg:HeadBound width cfgb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), higher.length ≤ width → ∀ t ≤ higher.length, HeadBound width (configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) t)lower:List Boolseen:Boolhw:(b :: higher).length ≤ widtht:ℕht:t ≤ (b :: higher).lengthr:ℕhr:r ≤ higher.length⊢ HeadBound width (configs (counterCfg cfg v (lower ++ b :: higher) (stLeft v (seen || b)) higher.length) r) simpa only [List.append_assoc, List.singleton_append] using ih (lower ++ [b]) (seen || b) (input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolwidth:ℕhcfg:HeadBound width cfgb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), higher.length ≤ width → ∀ t ≤ higher.length, HeadBound width (configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) t)lower:List Boolseen:Boolhw:(b :: higher).length ≤ widtht:ℕht:t ≤ (b :: higher).lengthr:ℕhr:r ≤ higher.length⊢ higher.length ≤ width input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolwidth:ℕhcfg:HeadBound width cfgb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), higher.length ≤ width → ∀ t ≤ higher.length, HeadBound width (configs (counterCfg cfg v (lower ++ higher) (stLeft v seen) higher.length) t)lower:List Boolseen:Boolhw:higher.length + 1 ≤ widtht:ℕht:t ≤ (b :: higher).lengthr:ℕhr:r ≤ higher.length⊢ higher.length ≤ width; All goals completed! 🐙) r hr

Borrowing and its leftward scan stay in the initial head interval.

theorem configs_borrow_headBound {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (v : Bool) (higher : List Bool) (width : ℕ) (hcfg : HeadBound width cfg) : ∀ lower seen, 0 < Counter.value higher → higher.length ≤ width → ∀ t ≤ higher.length, HeadBound width (machine.configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) t) := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Boolwidth:ℕhcfg:HeadBound width cfg⊢ ∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → higher.length ≤ width → ∀ t ≤ higher.length, HeadBound width (configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Boolwidth:ℕhcfg:HeadBound width cfg⊢ ∀ (lower : List Bool) (seen : Bool), 0 < Counter.value [] → [].length ≤ width → ∀ t ≤ [].length, HeadBound width (configs (counterCfg cfg v (lower ++ []) (stBorrow v seen) [].length) t)input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Boolwidth:ℕhcfg:HeadBound width cfg⊢ ∀ (head : Bool) (tail : List Bool), (∀ (lower : List Bool) (seen : Bool), 0 < Counter.value tail → tail.length ≤ width → ∀ t ≤ tail.length, HeadBound width (configs (counterCfg cfg v (lower ++ tail) (stBorrow v seen) tail.length) t)) → ∀ (lower : List Bool) (seen : Bool), 0 < Counter.value (head :: tail) → (head :: tail).length ≤ width → ∀ t ≤ (head :: tail).length, HeadBound width (configs (counterCfg cfg v (lower ++ head :: tail) (stBorrow v seen) (head :: tail).length) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Boolwidth:ℕhcfg:HeadBound width cfg⊢ ∀ (lower : List Bool) (seen : Bool), 0 < Counter.value [] → [].length ≤ width → ∀ t ≤ [].length, HeadBound width (configs (counterCfg cfg v (lower ++ []) (stBorrow v seen) [].length) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Boolwidth:ℕhcfg:HeadBound width cfglower:List Boolseen:Boolh:0 < Counter.value []⊢ [].length ≤ width → ∀ t ≤ [].length, HeadBound width (configs (counterCfg cfg v (lower ++ []) (stBorrow v seen) [].length) t) All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher:List Boolwidth:ℕhcfg:HeadBound width cfg⊢ ∀ (head : Bool) (tail : List Bool), (∀ (lower : List Bool) (seen : Bool), 0 < Counter.value tail → tail.length ≤ width → ∀ t ≤ tail.length, HeadBound width (configs (counterCfg cfg v (lower ++ tail) (stBorrow v seen) tail.length) t)) → ∀ (lower : List Bool) (seen : Bool), 0 < Counter.value (head :: tail) → (head :: tail).length ≤ width → ∀ t ≤ (head :: tail).length, HeadBound width (configs (counterCfg cfg v (lower ++ head :: tail) (stBorrow v seen) (head :: tail).length) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolwidth:ℕhcfg:HeadBound width cfgb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → higher.length ≤ width → ∀ t ≤ higher.length, HeadBound width (configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) t)lower:List Boolseen:Boolh:0 < Counter.value (b :: higher)hw:(b :: higher).length ≤ widtht:ℕht:t ≤ (b :: higher).length⊢ HeadBound width (configs (counterCfg cfg v (lower ++ b :: higher) (stBorrow v seen) (b :: higher).length) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolwidth:ℕhcfg:HeadBound width cfgb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → higher.length ≤ width → ∀ t ≤ higher.length, HeadBound width (configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) t)lower:List Boolseen:Boolh:0 < Counter.value (b :: higher)hw:(b :: higher).length ≤ widtht:ℕht:t ≤ (b :: higher).length⊢ ∀ t ≤ higher.length, HeadBound width (configs (step (counterCfg cfg v (lower ++ b :: higher) (stBorrow v seen) (b :: higher).length)) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolwidth:ℕhcfg:HeadBound width cfgb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → higher.length ≤ width → ∀ t ≤ higher.length, HeadBound width (configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) t)lower:List Boolseen:Boolh:0 < Counter.value (b :: higher)hw:(b :: higher).length ≤ widtht:ℕht:t ≤ (b :: higher).lengthr:ℕhr:r ≤ higher.length⊢ HeadBound width (configs (step (counterCfg cfg v (lower ++ b :: higher) (stBorrow v seen) (b :: higher).length)) r) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolwidth:ℕhcfg:HeadBound width cfgb:Boolhigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → higher.length ≤ width → ∀ t ≤ higher.length, HeadBound width (configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) t)lower:List Boolseen:Boolh:0 < Counter.value (b :: higher)hw:(b :: higher).length ≤ widtht:ℕht:t ≤ (b :: higher).lengthr:ℕhr:r ≤ higher.lengthhwidth:higher.length ≤ width⊢ HeadBound width (configs (step (counterCfg cfg v (lower ++ b :: higher) (stBorrow v seen) (b :: higher).length)) r) cases b with input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolwidth:ℕhcfg:HeadBound width cfghigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → higher.length ≤ width → ∀ t ≤ higher.length, HeadBound width (configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) t)lower:List Boolseen:Boolt:ℕr:ℕhr:r ≤ higher.lengthhwidth:higher.length ≤ widthh:0 < Counter.value (false :: higher)hw:(false :: higher).length ≤ widthht:t ≤ (false :: higher).length⊢ HeadBound width (configs (step (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (false :: higher).length)) r) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolwidth:ℕhcfg:HeadBound width cfghigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → higher.length ≤ width → ∀ t ≤ higher.length, HeadBound width (configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) t)lower:List Boolseen:Boolt:ℕr:ℕhr:r ≤ higher.lengthhwidth:higher.length ≤ widthh:0 < Counter.value (false :: higher)hw:(false :: higher).length ≤ widthht:t ≤ (false :: higher).lengthhh:0 < Counter.value higher⊢ HeadBound width (configs (step (counterCfg cfg v (lower ++ false :: higher) (stBorrow v seen) (false :: higher).length)) r) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolwidth:ℕhcfg:HeadBound width cfghigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → higher.length ≤ width → ∀ t ≤ higher.length, HeadBound width (configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) t)lower:List Boolseen:Boolt:ℕr:ℕhr:r ≤ higher.lengthhwidth:higher.length ≤ widthh:0 < Counter.value (false :: higher)hw:(false :: higher).length ≤ widthht:t ≤ (false :: higher).lengthhh:0 < Counter.value higher⊢ HeadBound width (configs (counterCfg cfg v (lower ++ true :: higher) (stBorrow v true) higher.length) r) All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolwidth:ℕhcfg:HeadBound width cfghigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → higher.length ≤ width → ∀ t ≤ higher.length, HeadBound width (configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) t)lower:List Boolseen:Boolt:ℕr:ℕhr:r ≤ higher.lengthhwidth:higher.length ≤ widthh:0 < Counter.value (true :: higher)hw:(true :: higher).length ≤ widthht:t ≤ (true :: higher).length⊢ HeadBound width (configs (step (counterCfg cfg v (lower ++ true :: higher) (stBorrow v seen) (true :: higher).length)) r) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolhigher✝:List Boolwidth:ℕhcfg:HeadBound width cfghigher:List Boolih:∀ (lower : List Bool) (seen : Bool), 0 < Counter.value higher → higher.length ≤ width → ∀ t ≤ higher.length, HeadBound width (configs (counterCfg cfg v (lower ++ higher) (stBorrow v seen) higher.length) t)lower:List Boolseen:Boolt:ℕr:ℕhr:r ≤ higher.lengthhwidth:higher.length ≤ widthh:0 < Counter.value (true :: higher)hw:(true :: higher).length ≤ widthht:t ≤ (true :: higher).length⊢ HeadBound width (configs (counterCfg cfg v (lower ++ false :: higher) (stLeft v seen) higher.length) r) All goals completed! 🐙

Every prefix of the rightward scan stays at or before the right-hand blank.

theorem configs_right_headBound {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (v seen : Bool) (bs : List Bool) (width : ℕ) (hcfg : HeadBound width cfg) (hw : bs.length + 1 ≤ width) (n : ℕ) : ∀ p, 0 < p → p + n = bs.length + 1 → ∀ t ≤ n + 1, HeadBound width (machine.configs (counterCfg cfg v bs (stRight v seen) p) t) := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthn:ℕ⊢ ∀ (p : ℕ), 0 < p → p + n = bs.length + 1 → ∀ t ≤ n + 1, HeadBound width (configs (counterCfg cfg v bs (stRight v seen) p) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthn:ℕ⊢ ∀ (p : ℕ), 0 < p → p + Nat.zero = bs.length + 1 → ∀ t ≤ Nat.zero + 1, HeadBound width (configs (counterCfg cfg v bs (stRight v seen) p) t)input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthn:ℕ⊢ ∀ (n : ℕ), (∀ (p : ℕ), 0 < p → p + n = bs.length + 1 → ∀ t ≤ n + 1, HeadBound width (configs (counterCfg cfg v bs (stRight v seen) p) t)) → ∀ (p : ℕ), 0 < p → p + n.succ = bs.length + 1 → ∀ t ≤ n.succ + 1, HeadBound width (configs (counterCfg cfg v bs (stRight v seen) p) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthn:ℕ⊢ ∀ (p : ℕ), 0 < p → p + Nat.zero = bs.length + 1 → ∀ t ≤ Nat.zero + 1, HeadBound width (configs (counterCfg cfg v bs (stRight v seen) p) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthn:ℕp:ℕa✝:0 < php:p + Nat.zero = bs.length + 1t:ℕht:t ≤ Nat.zero + 1⊢ HeadBound width (configs (counterCfg cfg v bs (stRight v seen) p) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthn:ℕp:ℕa✝:0 < php:p + Nat.zero = bs.length + 1t:ℕht:t ≤ Nat.zero + 1he:p = bs.length + 1⊢ HeadBound width (configs (counterCfg cfg v bs (stRight v seen) p) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthn:ℕt:ℕht:t ≤ Nat.zero + 1a✝:0 < bs.length + 1hp:bs.length + 1 + Nat.zero = bs.length + 1⊢ HeadBound width (configs (counterCfg cfg v bs (stRight v seen) (bs.length + 1)) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthn:ℕt:ℕht:t ≤ Nat.zero + 1a✝:0 < bs.length + 1hp:bs.length + 1 + Nat.zero = bs.length + 1⊢ ∀ t ≤ 0, HeadBound width (configs (step (counterCfg cfg v bs (stRight v seen) (bs.length + 1))) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthn:ℕt:ℕht:t ≤ Nat.zero + 1a✝:0 < bs.length + 1hp:bs.length + 1 + Nat.zero = bs.length + 1r:ℕhr:r ≤ 0⊢ HeadBound width (configs (step (counterCfg cfg v bs (stRight v seen) (bs.length + 1))) r) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthn:ℕt:ℕht:t ≤ Nat.zero + 1a✝:0 < bs.length + 1hp:bs.length + 1 + Nat.zero = bs.length + 1r:ℕhr:r ≤ 0he:r = 0⊢ HeadBound width (configs (step (counterCfg cfg v bs (stRight v seen) (bs.length + 1))) r) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthn:ℕt:ℕht:t ≤ Nat.zero + 1a✝:0 < bs.length + 1hp:bs.length + 1 + Nat.zero = bs.length + 1hr:0 ≤ 0⊢ HeadBound width (configs (step (counterCfg cfg v bs (stRight v seen) (bs.length + 1))) 0) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthn:ℕt:ℕht:t ≤ Nat.zero + 1a✝:0 < bs.length + 1hp:bs.length + 1 + Nat.zero = bs.length + 1hr:0 ≤ 0⊢ HeadBound width (counterCfg cfg v bs (afterDecrement v seen) (bs.length + 1)) All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthn:ℕ⊢ ∀ (n : ℕ), (∀ (p : ℕ), 0 < p → p + n = bs.length + 1 → ∀ t ≤ n + 1, HeadBound width (configs (counterCfg cfg v bs (stRight v seen) p) t)) → ∀ (p : ℕ), 0 < p → p + n.succ = bs.length + 1 → ∀ t ≤ n.succ + 1, HeadBound width (configs (counterCfg cfg v bs (stRight v seen) p) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthn✝:ℕn:ℕih:∀ (p : ℕ), 0 < p → p + n = bs.length + 1 → ∀ t ≤ n + 1, HeadBound width (configs (counterCfg cfg v bs (stRight v seen) p) t)p:ℕhp:0 < phn:p + n.succ = bs.length + 1t:ℕht:t ≤ n.succ + 1⊢ HeadBound width (configs (counterCfg cfg v bs (stRight v seen) p) t) cases p with input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthn✝:ℕn:ℕih:∀ (p : ℕ), 0 < p → p + n = bs.length + 1 → ∀ t ≤ n + 1, HeadBound width (configs (counterCfg cfg v bs (stRight v seen) p) t)t:ℕht:t ≤ n.succ + 1hp:0 < 0hn:0 + n.succ = bs.length + 1⊢ HeadBound width (configs (counterCfg cfg v bs (stRight v seen) 0) t) All goals completed! 🐙 input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthn✝:ℕn:ℕih:∀ (p : ℕ), 0 < p → p + n = bs.length + 1 → ∀ t ≤ n + 1, HeadBound width (configs (counterCfg cfg v bs (stRight v seen) p) t)t:ℕht:t ≤ n.succ + 1j:ℕhp:0 < j + 1hn:j + 1 + n.succ = bs.length + 1⊢ HeadBound width (configs (counterCfg cfg v bs (stRight v seen) (j + 1)) t) apply headBound_succ _ (n + 1) width (headBound_counterCfg cfg v _ _ _ width hcfg (input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthn✝:ℕn:ℕih:∀ (p : ℕ), 0 < p → p + n = bs.length + 1 → ∀ t ≤ n + 1, HeadBound width (configs (counterCfg cfg v bs (stRight v seen) p) t)t:ℕht:t ≤ n.succ + 1j:ℕhp:0 < j + 1hn:j + 1 + n.succ = bs.length + 1⊢ j + 1 ≤ width All goals completed! 🐙)) ?_ t ht input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthn✝:ℕn:ℕih:∀ (p : ℕ), 0 < p → p + n = bs.length + 1 → ∀ t ≤ n + 1, HeadBound width (configs (counterCfg cfg v bs (stRight v seen) p) t)t:ℕht:t ≤ n.succ + 1j:ℕhp:0 < j + 1hn:j + 1 + n.succ = bs.length + 1r:ℕhr:r ≤ n + 1⊢ HeadBound width (configs (step (counterCfg cfg v bs (stRight v seen) (j + 1))) r) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthn✝:ℕn:ℕih:∀ (p : ℕ), 0 < p → p + n = bs.length + 1 → ∀ t ≤ n + 1, HeadBound width (configs (counterCfg cfg v bs (stRight v seen) p) t)t:ℕht:t ≤ n.succ + 1j:ℕhp:0 < j + 1hn:j + 1 + n.succ = bs.length + 1r:ℕhr:r ≤ n + 1⊢ HeadBound width (configs (counterCfg cfg v bs (stRight v seen) (j + 2)) r) exact ih (j + 2) (input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthn✝:ℕn:ℕih:∀ (p : ℕ), 0 < p → p + n = bs.length + 1 → ∀ t ≤ n + 1, HeadBound width (configs (counterCfg cfg v bs (stRight v seen) p) t)t:ℕht:t ≤ n.succ + 1j:ℕhp:0 < j + 1hn:j + 1 + n.succ = bs.length + 1r:ℕhr:r ≤ n + 1⊢ 0 < j + 2 All goals completed! 🐙) (input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolseen:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthn✝:ℕn:ℕih:∀ (p : ℕ), 0 < p → p + n = bs.length + 1 → ∀ t ≤ n + 1, HeadBound width (configs (counterCfg cfg v bs (stRight v seen) p) t)t:ℕht:t ≤ n.succ + 1j:ℕhp:0 < j + 1hn:j + 1 + n.succ = bs.length + 1r:ℕhr:r ≤ n + 1⊢ j + 2 + n = bs.length + 1 All goals completed! 🐙) r hr

All countdown prefixes preserve any nonnegative head bound containing the represented word and its right-hand blank.

theorem configs_decrement_headBound {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (v : Bool) (bs : List Bool) (width : ℕ) (hcfg : HeadBound width cfg) (hw : bs.length + 1 ≤ width) (hbs : 0 < Counter.value bs) (t : ℕ) (ht : t ≤ 2 * bs.length + 3) : HeadBound width (machine.configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) t) := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthhbs:0 < Counter.value bst:ℕht:t ≤ 2 * bs.length + 3⊢ HeadBound width (configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthhbs:0 < Counter.value bst:ℕht:t ≤ 2 * bs.length + 3hborrow:configs (counterCfg cfg v ([] ++ bs) (stBorrow v false) bs.length) bs.length = counterCfg cfg v ([] ++ Counter.decrement bs) (stLeft v (false || (Counter.decrement bs).any id)) 0⊢ HeadBound width (configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthhbs:0 < Counter.value bst:ℕht:t ≤ 2 * bs.length + 3hborrow:configs (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0⊢ HeadBound width (configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthhbs:0 < Counter.value bst:ℕht:t ≤ 2 * bs.length + 3hborrow:configs (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0hright:∀ r ≤ bs.length + 1, HeadBound width (configs (counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1) r)⊢ HeadBound width (configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthhbs:0 < Counter.value bst:ℕht:t ≤ 2 * bs.length + 3hborrow:configs (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0hright:∀ r ≤ bs.length + 1, HeadBound width (configs (counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1) r)hturn:∀ r ≤ 1 + (bs.length + 1), HeadBound width (configs (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) r)⊢ HeadBound width (configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) t) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthhbs:0 < Counter.value bst:ℕht:t ≤ 2 * bs.length + 3hborrow:configs (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0hright:∀ r ≤ bs.length + 1, HeadBound width (configs (counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1) r)hturn:∀ r ≤ 1 + (bs.length + 1), HeadBound width (configs (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) r)htail:∀ r ≤ bs.length + (1 + (bs.length + 1)), HeadBound width (configs (counterCfg cfg v bs (stBorrow v false) bs.length) r)⊢ HeadBound width (configs (counterCfg cfg v bs (stDecrement v) (bs.length + 1)) t) apply headBound_succ _ (bs.length + (1 + (bs.length + 1))) width (headBound_counterCfg cfg v _ _ _ width hcfg hw) ?_ t (input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthhbs:0 < Counter.value bst:ℕht:t ≤ 2 * bs.length + 3hborrow:configs (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0hright:∀ r ≤ bs.length + 1, HeadBound width (configs (counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1) r)hturn:∀ r ≤ 1 + (bs.length + 1), HeadBound width (configs (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) r)htail:∀ r ≤ bs.length + (1 + (bs.length + 1)), HeadBound width (configs (counterCfg cfg v bs (stBorrow v false) bs.length) r)⊢ t ≤ bs.length + (1 + (bs.length + 1)) + 1 All goals completed! 🐙) input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolwidth:ℕhcfg:HeadBound width cfghw:bs.length + 1 ≤ widthhbs:0 < Counter.value bst:ℕht:t ≤ 2 * bs.length + 3hborrow:configs (counterCfg cfg v bs (stBorrow v false) bs.length) bs.length = counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0hright:∀ r ≤ bs.length + 1, HeadBound width (configs (counterCfg cfg v (Counter.decrement bs) (stRight v ((Counter.decrement bs).any id)) 1) r)hturn:∀ r ≤ 1 + (bs.length + 1), HeadBound width (configs (counterCfg cfg v (Counter.decrement bs) (stLeft v ((Counter.decrement bs).any id)) 0) r)htail:∀ r ≤ bs.length + (1 + (bs.length + 1)), HeadBound width (configs (counterCfg cfg v bs (stBorrow v false) bs.length) r)⊢ ∀ r ≤ bs.length + (1 + (bs.length + 1)), HeadBound width (configs (counterCfg cfg v bs (stBorrow v false) bs.length) r) All goals completed! 🐙
end Geb.BitTree.Elias.Machine