1. Geb
  2. Prototypes
  3. Computability
  4. BitTree
  5. Elias
  6. MachineRead
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.MachineModel public import Geb.Prototypes.Computability.BitTree.Elias.MachineConfig public import Geb.Prototypes.Computability.TreeScanner.Steps public import Mathlib.Tactic.FinCases
set_option doc.verso true

Reading input at delta-decoder boundaries

Each external reading transition advances the input once and emits nothing. The results below expose its writes as updates of the two finite binary words; the countdown and cleanup proofs then compose with those boundaries directly.

Main statements

  • step_read resolves a reading transition on an arbitrary configuration.

  • step_tree, step_zeros, step_size and step_length describe the four kinds of header input transitions.

Implementation notes

These statements concern the Cslib execution functions and their input reader, whose implementation uses Classical.choice.

Tags

Elias delta code, Turing machine, input, simulation

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

Resolve one external reading step while leaving its work actions explicit.

theorem step_read {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (q : Control) (b : Bool) (hq : cfg.state = some q) (hin : cfg.inputSymbol = some (boolEmb b)) (hr : q = stTree ∨ q = stZeros ∨ q = stSizeBit ∨ q = stLengthBit ∨ q = stPayloadBit ∨ q = stDone ∨ q = stDead) : machine.step cfg = { state := (read q (boolEmb b)).q' inputPos := moveInputPos cfg.inputPos 1 workTapes := fun i ↦ match ((read q (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s workTapePos := fun i ↦ cfg.workTapePos i + ((read q (boolEmb b)).workActions i).2 } := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputq:Controlb:Boolhq:cfg.state = some qhin:cfg.inputSymbol = some (boolEmb b)hr:q = stTree ∨ q = stZeros ∨ q = stSizeBit ∨ q = stLengthBit ∨ q = stPayloadBit ∨ q = stDone ∨ q = stDead⊢ step cfg = { state := (read q (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read q (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read q (boolEmb b)).workActions i).2 } input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputq:Controlb:Boolhq:cfg.state = some qhin:cfg.inputSymbol = some (boolEmb b)hr:q = stTree ∨ q = stZeros ∨ q = stSizeBit ∨ q = stLengthBit ∨ q = stPayloadBit ∨ q = stDone ∨ q = stDead⊢ { state := (read q (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read q (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read q (boolEmb b)).workActions i).2 } = { state := (read q (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read q (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read q (boolEmb b)).workActions i).2 } input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputq:Controlb:Boolhq:cfg.state = some qhin:cfg.inputSymbol = some (boolEmb b)hr:q = stTree ∨ q = stZeros ∨ q = stSizeBit ∨ q = stLengthBit ∨ q = stPayloadBit ∨ q = stDone ∨ q = stDead⊢ { state := (read q (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read q (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read q (boolEmb b)).workActions i).2 }.workTapes = { state := (read q (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read q (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read q (boolEmb b)).workActions i).2 }.workTapes input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputq:Controlb:Boolhq:cfg.state = some qhin:cfg.inputSymbol = some (boolEmb b)hr:q = stTree ∨ q = stZeros ∨ q = stSizeBit ∨ q = stLengthBit ∨ q = stPayloadBit ∨ q = stDone ∨ q = stDeadi:Fin 4z:ℤ⊢ { state := (read q (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read q (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read q (boolEmb b)).workActions i).2 }.workTapes i z = { state := (read q (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read q (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read q (boolEmb b)).workActions i).2 }.workTapes i z input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputb:Boolhin:cfg.inputSymbol = some (boolEmb b)i:Fin 4z:ℤhq:cfg.state = some stTree⊢ { state := (read stTree (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb b)).workActions i).2 }.workTapes i z = { state := (read stTree (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb b)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputb:Boolhin:cfg.inputSymbol = some (boolEmb b)i:Fin 4z:ℤhq:cfg.state = some stZeros⊢ { state := (read stZeros (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb b)).workActions i).2 }.workTapes i z = { state := (read stZeros (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb b)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputb:Boolhin:cfg.inputSymbol = some (boolEmb b)i:Fin 4z:ℤhq:cfg.state = some stSizeBit⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapes i z = { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputb:Boolhin:cfg.inputSymbol = some (boolEmb b)i:Fin 4z:ℤhq:cfg.state = some stLengthBit⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapes i z = { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputb:Boolhin:cfg.inputSymbol = some (boolEmb b)i:Fin 4z:ℤhq:cfg.state = some stPayloadBit⊢ { state := (read stPayloadBit (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb b)).workActions i).2 }.workTapes i z = { state := (read stPayloadBit (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb b)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputb:Boolhin:cfg.inputSymbol = some (boolEmb b)i:Fin 4z:ℤhq:cfg.state = some stDone⊢ { state := (read stDone (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb b)).workActions i).2 }.workTapes i z = { state := (read stDone (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb b)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputb:Boolhin:cfg.inputSymbol = some (boolEmb b)i:Fin 4z:ℤhq:cfg.state = some stDead⊢ { state := (read stDead (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb b)).workActions i).2 }.workTapes i z = { state := (read stDead (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb b)).workActions i).2 }.workTapes i z input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputb:Boolhin:cfg.inputSymbol = some (boolEmb b)i:Fin 4z:ℤhq:cfg.state = some stTree⊢ { state := (read stTree (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb b)).workActions i).2 }.workTapes i z = { state := (read stTree (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb b)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputb:Boolhin:cfg.inputSymbol = some (boolEmb b)i:Fin 4z:ℤhq:cfg.state = some stZeros⊢ { state := (read stZeros (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb b)).workActions i).2 }.workTapes i z = { state := (read stZeros (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb b)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputb:Boolhin:cfg.inputSymbol = some (boolEmb b)i:Fin 4z:ℤhq:cfg.state = some stSizeBit⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapes i z = { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputb:Boolhin:cfg.inputSymbol = some (boolEmb b)i:Fin 4z:ℤhq:cfg.state = some stLengthBit⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapes i z = { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputb:Boolhin:cfg.inputSymbol = some (boolEmb b)i:Fin 4z:ℤhq:cfg.state = some stPayloadBit⊢ { state := (read stPayloadBit (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb b)).workActions i).2 }.workTapes i z = { state := (read stPayloadBit (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb b)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputb:Boolhin:cfg.inputSymbol = some (boolEmb b)i:Fin 4z:ℤhq:cfg.state = some stDone⊢ { state := (read stDone (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb b)).workActions i).2 }.workTapes i z = { state := (read stDone (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb b)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputb:Boolhin:cfg.inputSymbol = some (boolEmb b)i:Fin 4z:ℤhq:cfg.state = some stDead⊢ { state := (read stDead (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb b)).workActions i).2 }.workTapes i z = { state := (read stDead (boolEmb b)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb b)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb b)).workActions i).2 }.workTapes i z input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputi:Fin 4z:ℤhq:cfg.state = some stDeadhin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stDead (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb false)).workActions i).2 }.workTapes i z = { state := (read stDead (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb false)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputi:Fin 4z:ℤhq:cfg.state = some stDeadhin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stDead (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb true)).workActions i).2 }.workTapes i z = { state := (read stDead (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb true)).workActions i).2 }.workTapes i z input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputi:Fin 4z:ℤhq:cfg.state = some stTreehin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapes i z = { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputi:Fin 4z:ℤhq:cfg.state = some stTreehin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapes i z = { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputi:Fin 4z:ℤhq:cfg.state = some stZeroshin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 }.workTapes i z = { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputi:Fin 4z:ℤhq:cfg.state = some stZeroshin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapes i z = { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputi:Fin 4z:ℤhq:cfg.state = some stSizeBithin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stSizeBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb false)).workActions i).2 }.workTapes i z = { state := (read stSizeBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb false)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputi:Fin 4z:ℤhq:cfg.state = some stSizeBithin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stSizeBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb true)).workActions i).2 }.workTapes i z = { state := (read stSizeBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb true)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputi:Fin 4z:ℤhq:cfg.state = some stLengthBithin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stLengthBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb false)).workActions i).2 }.workTapes i z = { state := (read stLengthBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb false)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputi:Fin 4z:ℤhq:cfg.state = some stLengthBithin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stLengthBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb true)).workActions i).2 }.workTapes i z = { state := (read stLengthBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb true)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputi:Fin 4z:ℤhq:cfg.state = some stPayloadBithin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stPayloadBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb false)).workActions i).2 }.workTapes i z = { state := (read stPayloadBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb false)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputi:Fin 4z:ℤhq:cfg.state = some stPayloadBithin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stPayloadBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb true)).workActions i).2 }.workTapes i z = { state := (read stPayloadBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb true)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputi:Fin 4z:ℤhq:cfg.state = some stDonehin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stDone (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb false)).workActions i).2 }.workTapes i z = { state := (read stDone (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb false)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputi:Fin 4z:ℤhq:cfg.state = some stDonehin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stDone (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb true)).workActions i).2 }.workTapes i z = { state := (read stDone (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb true)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputi:Fin 4z:ℤhq:cfg.state = some stDeadhin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stDead (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb false)).workActions i).2 }.workTapes i z = { state := (read stDead (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb false)).workActions i).2 }.workTapes i zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputi:Fin 4z:ℤhq:cfg.state = some stDeadhin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stDead (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb true)).workActions i).2 }.workTapes i z = { state := (read stDead (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb true)).workActions i).2 }.workTapes i z input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stDeadhin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stDead (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) z = { state := (read stDead (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stDeadhin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stDead (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) z = { state := (read stDead (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stDeadhin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stDead (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) z = { state := (read stDead (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stDeadhin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stDead (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) z = { state := (read stDead (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) z input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stTreehin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) z = { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stTreehin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) z = { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stTreehin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) z = { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stTreehin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) z = { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stTreehin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) z = { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stTreehin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) z = { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stTreehin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) z = { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stTreehin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) z = { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stZeroshin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) z = { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stZeroshin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) z = { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stZeroshin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) z = { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stZeroshin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) z = { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stZeroshin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) z = { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stZeroshin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) z = { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stZeroshin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) z = { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stZeroshin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) z = { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stSizeBithin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stSizeBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) z = { state := (read stSizeBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stSizeBithin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stSizeBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) z = { state := (read stSizeBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stSizeBithin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stSizeBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) z = { state := (read stSizeBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stSizeBithin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stSizeBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) z = { state := (read stSizeBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stSizeBithin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stSizeBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) z = { state := (read stSizeBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stSizeBithin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stSizeBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) z = { state := (read stSizeBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stSizeBithin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stSizeBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) z = { state := (read stSizeBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stSizeBithin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stSizeBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) z = { state := (read stSizeBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stSizeBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stLengthBithin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stLengthBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) z = { state := (read stLengthBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stLengthBithin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stLengthBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) z = { state := (read stLengthBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stLengthBithin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stLengthBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) z = { state := (read stLengthBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stLengthBithin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stLengthBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) z = { state := (read stLengthBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stLengthBithin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stLengthBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) z = { state := (read stLengthBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stLengthBithin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stLengthBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) z = { state := (read stLengthBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stLengthBithin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stLengthBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) z = { state := (read stLengthBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stLengthBithin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stLengthBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) z = { state := (read stLengthBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stLengthBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stPayloadBithin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stPayloadBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) z = { state := (read stPayloadBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stPayloadBithin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stPayloadBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) z = { state := (read stPayloadBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stPayloadBithin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stPayloadBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) z = { state := (read stPayloadBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stPayloadBithin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stPayloadBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) z = { state := (read stPayloadBit (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stPayloadBithin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stPayloadBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) z = { state := (read stPayloadBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stPayloadBithin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stPayloadBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) z = { state := (read stPayloadBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stPayloadBithin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stPayloadBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) z = { state := (read stPayloadBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stPayloadBithin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stPayloadBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) z = { state := (read stPayloadBit (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stPayloadBit (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stDonehin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stDone (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) z = { state := (read stDone (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stDonehin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stDone (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) z = { state := (read stDone (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stDonehin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stDone (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) z = { state := (read stDone (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stDonehin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stDone (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) z = { state := (read stDone (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stDonehin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stDone (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) z = { state := (read stDone (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stDonehin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stDone (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) z = { state := (read stDone (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stDonehin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stDone (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) z = { state := (read stDone (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stDonehin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stDone (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) z = { state := (read stDone (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDone (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDone (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stDeadhin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stDead (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) z = { state := (read stDead (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stDeadhin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stDead (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) z = { state := (read stDead (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stDeadhin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stDead (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) z = { state := (read stDead (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stDeadhin:cfg.inputSymbol = some (boolEmb false)⊢ { state := (read stDead (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) z = { state := (read stDead (boolEmb false)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb false)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stDeadhin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stDead (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) z = { state := (read stDead (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stDeadhin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stDead (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) z = { state := (read stDead (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stDeadhin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stDead (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) z = { state := (read stDead (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) zinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputz:ℤhq:cfg.state = some stDeadhin:cfg.inputSymbol = some (boolEmb true)⊢ { state := (read stDead (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) z = { state := (read stDead (boolEmb true)).q', inputPos := moveInputPos cfg.inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stDead (boolEmb true)).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i ↦ cfg.workTapePos i + ↑((read stDead (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) z All goals completed! 🐙

Reading an external bit emits nothing.

theorem outputSymbol_read {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (q : Control) (b : Bool) (hq : cfg.state = some q) (hin : cfg.inputSymbol = some (boolEmb b)) (hr : q = stTree ∨ q = stZeros ∨ q = stSizeBit ∨ q = stLengthBit ∨ q = stPayloadBit ∨ q = stDone ∨ q = stDead) : machine.outputSymbol cfg = none := input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputq:Controlb:Boolhq:cfg.state = some qhin:cfg.inputSymbol = some (boolEmb b)hr:q = stTree ∨ q = stZeros ∨ q = stSizeBit ∨ q = stLengthBit ∨ q = stPayloadBit ∨ q = stDone ∨ q = stDead⊢ outputSymbol cfg = none input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputq:Controlb:Boolhq:cfg.state = some qhin:cfg.inputSymbol = some (boolEmb b)hr:q = stTree ∨ q = stZeros ∨ q = stSizeBit ∨ q = stLengthBit ∨ q = stPayloadBit ∨ q = stDone ∨ q = stDead⊢ (match cfg.state with | none => none | some q => (machine.tr q cfg.inputSymbol cfg.workTapeSymbols).outS) = none input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputq:Controlb:Boolhq:cfg.state = some qhin:cfg.inputSymbol = some (boolEmb b)hr:q = stTree ∨ q = stZeros ∨ q = stSizeBit ∨ q = stLengthBit ∨ q = stPayloadBit ∨ q = stDone ∨ q = stDead⊢ (match some q with | none => none | some q => (machine.tr q cfg.inputSymbol cfg.workTapeSymbols).outS) = none input:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputq:Controlb:Boolhq:cfg.state = some qhin:cfg.inputSymbol = some (boolEmb b)hr:q = stTree ∨ q = stZeros ∨ q = stSizeBit ∨ q = stLengthBit ∨ q = stPayloadBit ∨ q = stDone ∨ q = stDead⊢ (machine.tr q cfg.inputSymbol cfg.workTapeSymbols).outS = none All goals completed! 🐙

A fork increases pending trees; a leaf initializes its implicit leading length bit.

theorem step_tree (input : List (Fin 3)) (pos : Fin (input.length + 2)) (pending zeros : ℕ) (bs cs : List Bool) (b : Bool) (hin : (scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb b)) : machine.step (scanCfg input pos stTree pending zeros bs cs) = if b then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs) := input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ step (scanCfg input pos stTree pending zeros bs cs) = if b = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stTree (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb b)).workActions i).2 } = if b = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 } = if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 } = if true = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 } = if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 } = if true = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapes = (if true = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapesinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapePos = (if true = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapePos input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapes = (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapes input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)i:Fin 4⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapes i = (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapes i input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapes ((fun i ↦ i) ⟨0, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapes ((fun i ↦ i) ⟨1, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapes ((fun i ↦ i) ⟨2, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapes ((fun i ↦ i) ⟨3, ⋯⟩) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapes ((fun i ↦ i) ⟨0, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapes ((fun i ↦ i) ⟨1, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapes ((fun i ↦ i) ⟨2, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapes ((fun i ↦ i) ⟨3, ⋯⟩) first | input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapes ((fun i ↦ i) ⟨3, ⋯⟩) | All goals completed! 🐙 input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapePos = (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapePos input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)i:Fin 4⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapePos i = (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapePos i input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨0, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapePos ((fun i ↦ i) ⟨0, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨1, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapePos ((fun i ↦ i) ⟨1, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨0, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapePos ((fun i ↦ i) ⟨0, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨1, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapePos ((fun i ↦ i) ⟨1, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stTree (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb false)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) All goals completed! 🐙 input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapes = (if true = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapes All goals completed! 🐙 input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapePos = (if true = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapePos input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb true)i:Fin 4⊢ { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapePos i = (if true = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapePos i input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨0, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapePos ((fun i ↦ i) ⟨0, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨1, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapePos ((fun i ↦ i) ⟨1, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨0, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapePos ((fun i ↦ i) ⟨0, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨1, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapePos ((fun i ↦ i) ⟨1, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stTree pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stTree (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stTree pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stTree (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stTree pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stTree pending zeros bs cs).workTapes i) ((scanCfg input pos stTree pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stTree pending zeros bs cs).workTapePos i + ↑((read stTree (boolEmb true)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stTree (pending + 1) zeros bs cs else scanCfg input (moveInputPos pos 1) stZeros pending zeros bs (true :: cs)).workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) All goals completed! 🐙

Zeros increase the unary header count; its first one initializes the width field.

theorem step_zeros (input : List (Fin 3)) (pos : Fin (input.length + 2)) (pending zeros : ℕ) (bs cs : List Bool) (b : Bool) (hin : (scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb b)) : machine.step (scanCfg input pos stZeros pending zeros bs cs) = if b then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs := input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ step (scanCfg input pos stZeros pending zeros bs cs) = if b = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stZeros (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb b)).workActions i).2 } = if b = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 } = if false = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs csinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 } = if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 } = if false = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs csinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 } = if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapes = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapesinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapePos = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapePos input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 }.workTapes = (if false = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapes All goals completed! 🐙 input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 }.workTapePos = (if false = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapePos input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb false)i:Fin 4⊢ { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 }.workTapePos i = (if false = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapePos i input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨0, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapePos ((fun i ↦ i) ⟨0, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨1, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapePos ((fun i ↦ i) ⟨1, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨0, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapePos ((fun i ↦ i) ⟨0, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨1, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapePos ((fun i ↦ i) ⟨1, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb false)⊢ { state := (read stZeros (boolEmb false)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb false)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb false)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) = (if false = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) All goals completed! 🐙 input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapes = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapes input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)i:Fin 4⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapes i = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapes i input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapes ((fun i ↦ i) ⟨0, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapes ((fun i ↦ i) ⟨1, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapes ((fun i ↦ i) ⟨2, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapes ((fun i ↦ i) ⟨3, ⋯⟩) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapes ((fun i ↦ i) ⟨0, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapes ((fun i ↦ i) ⟨1, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapes ((fun i ↦ i) ⟨2, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapes ((fun i ↦ i) ⟨3, ⋯⟩) first | All goals completed! 🐙 | All goals completed! 🐙 input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapePos = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapePos input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)i:Fin 4⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapePos i = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapePos i input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨0, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapePos ((fun i ↦ i) ⟨0, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨1, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapePos ((fun i ↦ i) ⟨1, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨0, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapePos ((fun i ↦ i) ⟨0, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨1, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapePos ((fun i ↦ i) ⟨1, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolhin:(scanCfg input pos stZeros pending zeros bs cs).inputSymbol = some (boolEmb true)⊢ { state := (read stZeros (boolEmb true)).q', inputPos := moveInputPos (scanCfg input pos stZeros pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stZeros (boolEmb true)).workActions i).1 with | none => (scanCfg input pos stZeros pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stZeros pending zeros bs cs).workTapes i) ((scanCfg input pos stZeros pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stZeros pending zeros bs cs).workTapePos i + ↑((read stZeros (boolEmb true)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) = (if true = true then scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (true :: bs) cs else scanCfg input (moveInputPos pos 1) stZeros pending (zeros + 1) bs cs).workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) All goals completed! 🐙

A width-field bit appends one digit and consumes one unary count position.

theorem step_size (input : List (Fin 3)) (pos : Fin (input.length + 2)) (pending zeros : ℕ) (bs cs : List Bool) (b : Bool) (hin : (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)) : machine.step (scanCfg input pos stSizeBit pending (zeros + 1) bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs := input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ step (scanCfg input pos stSizeBit pending (zeros + 1) bs cs) = scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 } = scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapes = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapesinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapePos = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapePos input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapes = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapes input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)i:Fin 4⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapes i = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapes i input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapes ((fun i ↦ i) ⟨0, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapes ((fun i ↦ i) ⟨1, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapes ((fun i ↦ i) ⟨2, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapes ((fun i ↦ i) ⟨3, ⋯⟩) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapes ((fun i ↦ i) ⟨0, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapes ((fun i ↦ i) ⟨1, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapes ((fun i ↦ i) ⟨2, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapes ((fun i ↦ i) ⟨3, ⋯⟩) All goals completed! 🐙 All goals completed! 🐙 input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapePos = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapePos input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)i:Fin 4⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapePos i = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapePos i input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨0, ⋯⟩) = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapePos ((fun i ↦ i) ⟨0, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨1, ⋯⟩) = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapePos ((fun i ↦ i) ⟨1, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨0, ⋯⟩) = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapePos ((fun i ↦ i) ⟨0, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨1, ⋯⟩) = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapePos ((fun i ↦ i) ⟨1, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stSizeBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stSizeBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapes i) ((scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeBit pending (zeros + 1) bs cs).workTapePos i + ↑((read stSizeBit (boolEmb b)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) = (scanCfg input (moveInputPos pos 1) stSizeCheck pending zeros (b :: bs) cs).workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) All goals completed! 🐙

A payload-length bit appends one digit and enters the width countdown.

theorem step_length (input : List (Fin 3)) (pos : Fin (input.length + 2)) (pending zeros : ℕ) (bs cs : List Bool) (b : Bool) (hin : (scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)) : machine.step (scanCfg input pos stLengthBit pending zeros bs cs) = scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs) := input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ step (scanCfg input pos stLengthBit pending zeros bs cs) = scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 } = scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapes = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapesinput:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapePos = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapePos input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapes = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapes input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)i:Fin 4⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapes i = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapes i input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapes ((fun i ↦ i) ⟨0, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapes ((fun i ↦ i) ⟨1, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapes ((fun i ↦ i) ⟨2, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapes ((fun i ↦ i) ⟨3, ⋯⟩) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨0, ⋯⟩) = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapes ((fun i ↦ i) ⟨0, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨1, ⋯⟩) = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapes ((fun i ↦ i) ⟨1, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨2, ⋯⟩) = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapes ((fun i ↦ i) ⟨2, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapes ((fun i ↦ i) ⟨3, ⋯⟩) = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapes ((fun i ↦ i) ⟨3, ⋯⟩) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ Function.update (wordTape cs) (↑cs.length + 1) (some (if b = true then 1 else 0)) = wordTape (b :: cs) All goals completed! 🐙 input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapePos = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapePos input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)i:Fin 4⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapePos i = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapePos i input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨0, ⋯⟩) = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapePos ((fun i ↦ i) ⟨0, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨1, ⋯⟩) = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapePos ((fun i ↦ i) ⟨1, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨0, ⋯⟩) = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapePos ((fun i ↦ i) ⟨0, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨1, ⋯⟩) = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapePos ((fun i ↦ i) ⟨1, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩)input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stLengthBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stLengthBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stLengthBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stLengthBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stLengthBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stLengthBit pending zeros bs cs).workTapes i) ((scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stLengthBit pending zeros bs cs).workTapePos i + ↑((read stLengthBit (boolEmb b)).workActions i).2 }.workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) = (scanCfg input (moveInputPos pos 1) (stDecrement false) pending zeros bs (b :: cs)).workTapePos ((fun i ↦ i) ⟨3, ⋯⟩) All goals completed! 🐙

A raw payload bit enters the payload countdown without changing either field.

theorem step_payload (input : List (Fin 3)) (pos : Fin (input.length + 2)) (pending zeros : ℕ) (bs cs : List Bool) (b : Bool) (hin : (scanCfg input pos stPayloadBit pending zeros bs cs).inputSymbol = some (boolEmb b)) : machine.step (scanCfg input pos stPayloadBit pending zeros bs cs) = scanCfg input (moveInputPos pos 1) (stDecrement true) pending zeros bs cs := input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stPayloadBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ step (scanCfg input pos stPayloadBit pending zeros bs cs) = scanCfg input (moveInputPos pos 1) (stDecrement true) pending zeros bs cs input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stPayloadBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stPayloadBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stPayloadBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stPayloadBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stPayloadBit pending zeros bs cs).workTapes i) ((scanCfg input pos stPayloadBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stPayloadBit pending zeros bs cs).workTapePos i + ↑((read stPayloadBit (boolEmb b)).workActions i).2 } = scanCfg input (moveInputPos pos 1) (stDecrement true) pending zeros bs cs input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stPayloadBit pending zeros bs cs).inputSymbol = some (boolEmb b)⊢ { state := (read stPayloadBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stPayloadBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stPayloadBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stPayloadBit pending zeros bs cs).workTapes i) ((scanCfg input pos stPayloadBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stPayloadBit pending zeros bs cs).workTapePos i + ↑((read stPayloadBit (boolEmb b)).workActions i).2 }.workTapePos = (scanCfg input (moveInputPos pos 1) (stDecrement true) pending zeros bs cs).workTapePos input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stPayloadBit pending zeros bs cs).inputSymbol = some (boolEmb b)i:Fin 4⊢ { state := (read stPayloadBit (boolEmb b)).q', inputPos := moveInputPos (scanCfg input pos stPayloadBit pending zeros bs cs).inputPos 1, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((read stPayloadBit (boolEmb b)).workActions i).1 with | none => (scanCfg input pos stPayloadBit pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stPayloadBit pending zeros bs cs).workTapes i) ((scanCfg input pos stPayloadBit pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stPayloadBit pending zeros bs cs).workTapePos i + ↑((read stPayloadBit (boolEmb b)).workActions i).2 }.workTapePos i = (scanCfg input (moveInputPos pos 1) (stDecrement true) pending zeros bs cs).workTapePos i input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolb:Boolhin:(scanCfg input pos stPayloadBit pending zeros bs cs).inputSymbol = some (boolEmb b)i:Fin 4⊢ (scanCfg input pos stPayloadBit pending zeros bs cs).workTapePos i + 0 = (scanCfg input (moveInputPos pos 1) (stDecrement true) pending zeros bs cs).workTapePos i All goals completed! 🐙

The unary origin test selects the next width bit or begins its countdown.

theorem step_sizeCheck (input : List (Fin 3)) (pos : Fin (input.length + 2)) (pending zeros : ℕ) (bs cs : List Bool) : machine.step (scanCfg input pos stSizeCheck pending zeros bs cs) = scanCfg input pos (if zeros = 0 then stDecrement false else stSizeBit) pending zeros bs cs := input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Bool⊢ step (scanCfg input pos stSizeCheck pending zeros bs cs) = scanCfg input pos (if zeros = 0 then stDecrement false else stSizeBit) pending zeros bs cs input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolht:machine.tr stSizeCheck (scanCfg input pos stSizeCheck pending zeros bs cs).inputSymbol (scanCfg input pos stSizeCheck pending zeros bs cs).workTapeSymbols = jump (if zeros = 0 then stDecrement false else stSizeBit)⊢ step (scanCfg input pos stSizeCheck pending zeros bs cs) = scanCfg input pos (if zeros = 0 then stDecrement false else stSizeBit) pending zeros bs cs input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolht:machine.tr stSizeCheck (scanCfg input pos stSizeCheck pending zeros bs cs).inputSymbol (scanCfg input pos stSizeCheck pending zeros bs cs).workTapeSymbols = jump (if zeros = 0 then stDecrement false else stSizeBit)⊢ { state := (jump (if zeros = 0 then stDecrement false else stSizeBit)).q', inputPos := moveInputPos (scanCfg input pos stSizeCheck pending zeros bs cs).inputPos (jump (if zeros = 0 then stDecrement false else stSizeBit)).inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((jump (if zeros = 0 then stDecrement false else stSizeBit)).workActions i).1 with | none => (scanCfg input pos stSizeCheck pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeCheck pending zeros bs cs).workTapes i) ((scanCfg input pos stSizeCheck pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeCheck pending zeros bs cs).workTapePos i + ↑((jump (if zeros = 0 then stDecrement false else stSizeBit)).workActions i).2 } = scanCfg input pos (if zeros = 0 then stDecrement false else stSizeBit) pending zeros bs cs input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolht:machine.tr stSizeCheck (scanCfg input pos stSizeCheck pending zeros bs cs).inputSymbol (scanCfg input pos stSizeCheck pending zeros bs cs).workTapeSymbols = jump (if zeros = 0 then stDecrement false else stSizeBit)⊢ { state := (jump (if zeros = 0 then stDecrement false else stSizeBit)).q', inputPos := moveInputPos (scanCfg input pos stSizeCheck pending zeros bs cs).inputPos (jump (if zeros = 0 then stDecrement false else stSizeBit)).inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((jump (if zeros = 0 then stDecrement false else stSizeBit)).workActions i).1 with | none => (scanCfg input pos stSizeCheck pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeCheck pending zeros bs cs).workTapes i) ((scanCfg input pos stSizeCheck pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeCheck pending zeros bs cs).workTapePos i + ↑((jump (if zeros = 0 then stDecrement false else stSizeBit)).workActions i).2 }.workTapePos = (scanCfg input pos (if zeros = 0 then stDecrement false else stSizeBit) pending zeros bs cs).workTapePos input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolht:machine.tr stSizeCheck (scanCfg input pos stSizeCheck pending zeros bs cs).inputSymbol (scanCfg input pos stSizeCheck pending zeros bs cs).workTapeSymbols = jump (if zeros = 0 then stDecrement false else stSizeBit)i:Fin 4⊢ { state := (jump (if zeros = 0 then stDecrement false else stSizeBit)).q', inputPos := moveInputPos (scanCfg input pos stSizeCheck pending zeros bs cs).inputPos (jump (if zeros = 0 then stDecrement false else stSizeBit)).inputMove, workTapes := fun i ↦ match (motive := Option (Option (Fin 3)) → ℤ → Option (Fin 3)) ((jump (if zeros = 0 then stDecrement false else stSizeBit)).workActions i).1 with | none => (scanCfg input pos stSizeCheck pending zeros bs cs).workTapes i | some s => Function.update ((scanCfg input pos stSizeCheck pending zeros bs cs).workTapes i) ((scanCfg input pos stSizeCheck pending zeros bs cs).workTapePos i) s, workTapePos := fun i ↦ (scanCfg input pos stSizeCheck pending zeros bs cs).workTapePos i + ↑((jump (if zeros = 0 then stDecrement false else stSizeBit)).workActions i).2 }.workTapePos i = (scanCfg input pos (if zeros = 0 then stDecrement false else stSizeBit) pending zeros bs cs).workTapePos i input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Boolht:machine.tr stSizeCheck (scanCfg input pos stSizeCheck pending zeros bs cs).inputSymbol (scanCfg input pos stSizeCheck pending zeros bs cs).workTapeSymbols = jump (if zeros = 0 then stDecrement false else stSizeBit)i:Fin 4⊢ (scanCfg input pos stSizeCheck pending zeros bs cs).workTapePos i + 0 = (scanCfg input pos (if zeros = 0 then stDecrement false else stSizeBit) pending zeros bs cs).workTapePos i All goals completed! 🐙

Checking the unary header counter emits nothing.

theorem outputSymbol_sizeCheck (input : List (Fin 3)) (pos : Fin (input.length + 2)) (pending zeros : ℕ) (bs cs : List Bool) : machine.outputSymbol (scanCfg input pos stSizeCheck pending zeros bs cs) = none := input:List (Fin 3)pos:Fin (input.length + 2)pending:ℕzeros:ℕbs:List Boolcs:List Bool⊢ outputSymbol (scanCfg input pos stSizeCheck pending zeros bs cs) = none All goals completed! 🐙
end Geb.BitTree.Elias.Machine