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.BinaryMachine.Accounting
public import Geb.Prototypes.Computability.BitTree.BinaryMachine.Simulation
public import Geb.Prototypes.Computability.BitTree.BinaryMachine.Macroset_option doc.verso trueOne input bit of the binary-counter recognizer
An input transition is followed by a counter increment exactly at a fork tag or a leaf terminator. The combined segment realizes one accounting update.
Main statements
-
configs_bitimplements one bit without emitting output. -
configs_bit_head_boundsbounds the heads throughout that segment.
Tags
Turing machine, simulation, binary counter
@[expose] public sectionnamespace Geb.BitTree.BinaryMachineopen Turing MultiTapeTMThe complete segment for one bit preserves the representation and bounds its heads.
theorem configs_bit_aux {input : List (Fin 4)}
(cfg : Cfg 3 (Fin 4) (Fin 10) input) (s : Account) (b : Bool) (width : ℕ)
(hv : AccountValid s) (h : Represents width cfg (modeState s.mode) s.forks s.leaves)
(hi : cfg.inputSymbol = some (boolEmb b))
(ha : (accountStep s b).forks.size ≤ width)
(hb : (accountStep s b).leaves.size ≤ width) :
let cost := macroCost s b
let next := accountStep s b
Represents width (machine.configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(machine.configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧
∀ u ≤ cost, HeadBound width (machine.configs cfg u) := input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputs:Accountb:Boolwidth:ℕhv:AccountValid sh:Represents width cfg (modeState s.mode) s.forks s.leaveshi:cfg.inputSymbol = some (boolEmb b)ha:(accountStep s b).forks.size ≤ widthhb:(accountStep s b).leaves.size ≤ width⊢ let cost := macroCost s b;
let next := accountStep s b;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputs:Accountb:Boolwidth:ℕhv:AccountValid sh:Represents width cfg (modeState s.mode) s.forks s.leaveshi:cfg.inputSymbol = some (boolEmb b)ha:(accountStep s b).forks.size ≤ widthhb:(accountStep s b).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState s.mode b)⊢ let cost := macroCost s b;
let next := accountStep s b;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputs:Accountb:Boolwidth:ℕhv:AccountValid sh:Represents width cfg (modeState s.mode) s.forks s.leaveshi:cfg.inputSymbol = some (boolEmb b)ha:(accountStep s b).forks.size ≤ widthhb:(accountStep s b).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState s.mode b)hc:configs cfg 1 = after⊢ let cost := macroCost s b;
let next := accountStep s b;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputs:Accountb:Boolwidth:ℕhv:AccountValid sh:Represents width cfg (modeState s.mode) s.forks s.leaveshi:cfg.inputSymbol = some (boolEmb b)ha:(accountStep s b).forks.size ≤ widthhb:(accountStep s b).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState s.mode b)hc:configs cfg 1 = afterhr:Represents width after (postReadState s.mode b) s.forks s.leaves⊢ let cost := macroCost s b;
let next := accountStep s b;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputs:Accountb:Boolwidth:ℕhv:AccountValid sh:Represents width cfg (modeState s.mode) s.forks s.leaveshi:cfg.inputSymbol = some (boolEmb b)ha:(accountStep s b).forks.size ≤ widthhb:(accountStep s b).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState s.mode b)hc:configs cfg 1 = afterhr:Represents width after (postReadState s.mode b) s.forks s.leavesho:machine.outputString cfg 1 = []⊢ let cost := macroCost s b;
let next := accountStep s b;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputs:Accountb:Boolwidth:ℕhv:AccountValid sh:Represents width cfg (modeState s.mode) s.forks s.leaveshi:cfg.inputSymbol = some (boolEmb b)ha:(accountStep s b).forks.size ≤ widthhb:(accountStep s b).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState s.mode b)hc:configs cfg 1 = afterhr:Represents width after (postReadState s.mode b) s.forks s.leavesho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)⊢ let cost := macroCost s b;
let next := accountStep s b;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputb:Boolwidth:ℕhi:cfg.inputSymbol = some (boolEmb b)ho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)m:Modea:ℕc:ℕhv:AccountValid { mode := m, forks := a, leaves := c }h:Represents width cfg (modeState { mode := m, forks := a, leaves := c }.mode)
{ mode := m, forks := a, leaves := c }.forks { mode := m, forks := a, leaves := c }.leavesha:(accountStep { mode := m, forks := a, leaves := c } b).forks.size ≤ widthhb:(accountStep { mode := m, forks := a, leaves := c } b).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := m, forks := a, leaves := c }.mode b)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := m, forks := a, leaves := c }.mode b)
{ mode := m, forks := a, leaves := c }.forks { mode := m, forks := a, leaves := c }.leaves⊢ let cost := macroCost { mode := m, forks := a, leaves := c } b;
let next := accountStep { mode := m, forks := a, leaves := c } b;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputb:Boolwidth:ℕhi:cfg.inputSymbol = some (boolEmb b)ho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leavesha:(accountStep { mode := Mode.tree, forks := a, leaves := c } b).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } b).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode b)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode b)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaves⊢ let cost := macroCost { mode := Mode.tree, forks := a, leaves := c } b;
let next := accountStep { mode := Mode.tree, forks := a, leaves := c } b;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputb:Boolwidth:ℕhi:cfg.inputSymbol = some (boolEmb b)ho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leavesha:(accountStep { mode := Mode.string, forks := a, leaves := c } b).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } b).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode b)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode b)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaves⊢ let cost := macroCost { mode := Mode.string, forks := a, leaves := c } b;
let next := accountStep { mode := Mode.string, forks := a, leaves := c } b;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputb:Boolwidth:ℕhi:cfg.inputSymbol = some (boolEmb b)ho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.bit, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.bit, forks := a, leaves := c }.mode)
{ mode := Mode.bit, forks := a, leaves := c }.forks { mode := Mode.bit, forks := a, leaves := c }.leavesha:(accountStep { mode := Mode.bit, forks := a, leaves := c } b).forks.size ≤ widthhb:(accountStep { mode := Mode.bit, forks := a, leaves := c } b).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.bit, forks := a, leaves := c }.mode b)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.bit, forks := a, leaves := c }.mode b)
{ mode := Mode.bit, forks := a, leaves := c }.forks { mode := Mode.bit, forks := a, leaves := c }.leaves⊢ let cost := macroCost { mode := Mode.bit, forks := a, leaves := c } b;
let next := accountStep { mode := Mode.bit, forks := a, leaves := c } b;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputb:Boolwidth:ℕhi:cfg.inputSymbol = some (boolEmb b)ho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.done, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.done, forks := a, leaves := c }.mode)
{ mode := Mode.done, forks := a, leaves := c }.forks { mode := Mode.done, forks := a, leaves := c }.leavesha:(accountStep { mode := Mode.done, forks := a, leaves := c } b).forks.size ≤ widthhb:(accountStep { mode := Mode.done, forks := a, leaves := c } b).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.done, forks := a, leaves := c }.mode b)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.done, forks := a, leaves := c }.mode b)
{ mode := Mode.done, forks := a, leaves := c }.forks { mode := Mode.done, forks := a, leaves := c }.leaves⊢ let cost := macroCost { mode := Mode.done, forks := a, leaves := c } b;
let next := accountStep { mode := Mode.done, forks := a, leaves := c } b;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputb:Boolwidth:ℕhi:cfg.inputSymbol = some (boolEmb b)ho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.dead, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.dead, forks := a, leaves := c }.mode)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leavesha:(accountStep { mode := Mode.dead, forks := a, leaves := c } b).forks.size ≤ widthhb:(accountStep { mode := Mode.dead, forks := a, leaves := c } b).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode b)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode b)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leaves⊢ let cost := macroCost { mode := Mode.dead, forks := a, leaves := c } b;
let next := accountStep { mode := Mode.dead, forks := a, leaves := c } b;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputb:Boolwidth:ℕhi:cfg.inputSymbol = some (boolEmb b)ho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leavesha:(accountStep { mode := Mode.tree, forks := a, leaves := c } b).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } b).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode b)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode b)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaves⊢ let cost := macroCost { mode := Mode.tree, forks := a, leaves := c } b;
let next := accountStep { mode := Mode.tree, forks := a, leaves := c } b;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputb:Boolwidth:ℕhi:cfg.inputSymbol = some (boolEmb b)ho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leavesha:(accountStep { mode := Mode.string, forks := a, leaves := c } b).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } b).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode b)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode b)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaves⊢ let cost := macroCost { mode := Mode.string, forks := a, leaves := c } b;
let next := accountStep { mode := Mode.string, forks := a, leaves := c } b;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputb:Boolwidth:ℕhi:cfg.inputSymbol = some (boolEmb b)ho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.bit, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.bit, forks := a, leaves := c }.mode)
{ mode := Mode.bit, forks := a, leaves := c }.forks { mode := Mode.bit, forks := a, leaves := c }.leavesha:(accountStep { mode := Mode.bit, forks := a, leaves := c } b).forks.size ≤ widthhb:(accountStep { mode := Mode.bit, forks := a, leaves := c } b).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.bit, forks := a, leaves := c }.mode b)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.bit, forks := a, leaves := c }.mode b)
{ mode := Mode.bit, forks := a, leaves := c }.forks { mode := Mode.bit, forks := a, leaves := c }.leaves⊢ let cost := macroCost { mode := Mode.bit, forks := a, leaves := c } b;
let next := accountStep { mode := Mode.bit, forks := a, leaves := c } b;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputb:Boolwidth:ℕhi:cfg.inputSymbol = some (boolEmb b)ho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.done, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.done, forks := a, leaves := c }.mode)
{ mode := Mode.done, forks := a, leaves := c }.forks { mode := Mode.done, forks := a, leaves := c }.leavesha:(accountStep { mode := Mode.done, forks := a, leaves := c } b).forks.size ≤ widthhb:(accountStep { mode := Mode.done, forks := a, leaves := c } b).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.done, forks := a, leaves := c }.mode b)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.done, forks := a, leaves := c }.mode b)
{ mode := Mode.done, forks := a, leaves := c }.forks { mode := Mode.done, forks := a, leaves := c }.leaves⊢ let cost := macroCost { mode := Mode.done, forks := a, leaves := c } b;
let next := accountStep { mode := Mode.done, forks := a, leaves := c } b;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputb:Boolwidth:ℕhi:cfg.inputSymbol = some (boolEmb b)ho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.dead, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.dead, forks := a, leaves := c }.mode)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leavesha:(accountStep { mode := Mode.dead, forks := a, leaves := c } b).forks.size ≤ widthhb:(accountStep { mode := Mode.dead, forks := a, leaves := c } b).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode b)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode b)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leaves⊢ let cost := macroCost { mode := Mode.dead, forks := a, leaves := c } b;
let next := accountStep { mode := Mode.dead, forks := a, leaves := c } b;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.dead, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.dead, forks := a, leaves := c }.mode)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.dead, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.dead, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode false)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leaves⊢ let cost := macroCost { mode := Mode.dead, forks := a, leaves := c } false;
let next := accountStep { mode := Mode.dead, forks := a, leaves := c } false;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.dead, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.dead, forks := a, leaves := c }.mode)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.dead, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.dead, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode true)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leaves⊢ let cost := macroCost { mode := Mode.dead, forks := a, leaves := c } true;
let next := accountStep { mode := Mode.dead, forks := a, leaves := c } true;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)
case tree.true input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaves⊢ let cost := macroCost { mode := Mode.tree, forks := a, leaves := c } true;
let next := accountStep { mode := Mode.tree, forks := a, leaves := c } true;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshnext:(a + 1).size ≤ width⊢ let cost := macroCost { mode := Mode.tree, forks := a, leaves := c } true;
let next := accountStep { mode := Mode.tree, forks := a, leaves := c } true;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshnext:(a + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips (if false = true then c else a).bits + 1))
(if (if false = true then a else a + 1) = if false = true then c + 1 else c then stDone else stTree)
(if false = true then a else a + 1) (if false = true then c + 1 else c)hp':(configs after (2 * Counter.flips (if false = true then c else a).bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips (if false = true then c else a).bits + 1) = []⊢ let cost := macroCost { mode := Mode.tree, forks := a, leaves := c } true;
let next := accountStep { mode := Mode.tree, forks := a, leaves := c } true;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshnext:(a + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips a.bits + 1)) (if a + 1 = c then stDone else stTree) (a + 1) chp':(configs after (2 * Counter.flips a.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips a.bits + 1) = []⊢ let cost := macroCost { mode := Mode.tree, forks := a, leaves := c } true;
let next := accountStep { mode := Mode.tree, forks := a, leaves := c } true;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshnext:(a + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips a.bits + 1)) (if a + 1 = c then stDone else stTree) (a + 1) chp':(configs after (2 * Counter.flips a.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips a.bits + 1) = []hne:a + 1 ≠ c⊢ let cost := macroCost { mode := Mode.tree, forks := a, leaves := c } true;
let next := accountStep { mode := Mode.tree, forks := a, leaves := c } true;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshnext:(a + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips a.bits + 1)) (if a + 1 = c then stDone else stTree) (a + 1) chp':(configs after (2 * Counter.flips a.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips a.bits + 1) = []hne:a + 1 ≠ chc':configs cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true) =
configs after (2 * Counter.flips a.bits + 1)⊢ let cost := macroCost { mode := Mode.tree, forks := a, leaves := c } true;
let next := accountStep { mode := Mode.tree, forks := a, leaves := c } true;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshnext:(a + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips a.bits + 1)) (if a + 1 = c then stDone else stTree) (a + 1) chp':(configs after (2 * Counter.flips a.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips a.bits + 1) = []hne:a + 1 ≠ chc':configs cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true) =
configs after (2 * Counter.flips a.bits + 1)⊢ Represents width (configs cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true))
(modeState (accountStep { mode := Mode.tree, forks := a, leaves := c } true).mode)
(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks
(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leavesinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshnext:(a + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips a.bits + 1)) (if a + 1 = c then stDone else stTree) (a + 1) chp':(configs after (2 * Counter.flips a.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips a.bits + 1) = []hne:a + 1 ≠ chc':configs cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true) =
configs after (2 * Counter.flips a.bits + 1)⊢ (configs cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true)).inputPos = moveInputPos cfg.inputPos 1input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshnext:(a + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips a.bits + 1)) (if a + 1 = c then stDone else stTree) (a + 1) chp':(configs after (2 * Counter.flips a.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips a.bits + 1) = []hne:a + 1 ≠ chc':configs cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true) =
configs after (2 * Counter.flips a.bits + 1)⊢ machine.outputString cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true) = []input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshnext:(a + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips a.bits + 1)) (if a + 1 = c then stDone else stTree) (a + 1) chp':(configs after (2 * Counter.flips a.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips a.bits + 1) = []hne:a + 1 ≠ chc':configs cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true) =
configs after (2 * Counter.flips a.bits + 1)⊢ ∀ u ≤ macroCost { mode := Mode.tree, forks := a, leaves := c } true, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshnext:(a + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips a.bits + 1)) (if a + 1 = c then stDone else stTree) (a + 1) chp':(configs after (2 * Counter.flips a.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips a.bits + 1) = []hne:a + 1 ≠ chc':configs cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true) =
configs after (2 * Counter.flips a.bits + 1)⊢ Represents width (configs cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true))
(modeState (accountStep { mode := Mode.tree, forks := a, leaves := c } true).mode)
(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks
(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshnext:(a + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips a.bits + 1)) (if a + 1 = c then stDone else stTree) (a + 1) chp':(configs after (2 * Counter.flips a.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips a.bits + 1) = []hne:a + 1 ≠ chc':configs cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true) =
configs after (2 * Counter.flips a.bits + 1)⊢ Represents width (configs after (2 * Counter.flips a.bits + 1))
(modeState (accountStep { mode := Mode.tree, forks := a, leaves := c } true).mode)
(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks
(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves
All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshnext:(a + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips a.bits + 1)) (if a + 1 = c then stDone else stTree) (a + 1) chp':(configs after (2 * Counter.flips a.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips a.bits + 1) = []hne:a + 1 ≠ chc':configs cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true) =
configs after (2 * Counter.flips a.bits + 1)⊢ (configs cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true)).inputPos = moveInputPos cfg.inputPos 1 input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshnext:(a + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips a.bits + 1)) (if a + 1 = c then stDone else stTree) (a + 1) chp':(configs after (2 * Counter.flips a.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips a.bits + 1) = []hne:a + 1 ≠ chc':configs cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true) =
configs after (2 * Counter.flips a.bits + 1)⊢ after.inputPos = moveInputPos cfg.inputPos 1
All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshnext:(a + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips a.bits + 1)) (if a + 1 = c then stDone else stTree) (a + 1) chp':(configs after (2 * Counter.flips a.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips a.bits + 1) = []hne:a + 1 ≠ chc':configs cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true) =
configs after (2 * Counter.flips a.bits + 1)⊢ machine.outputString cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshnext:(a + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips a.bits + 1)) (if a + 1 = c then stDone else stTree) (a + 1) chp':(configs after (2 * Counter.flips a.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips a.bits + 1) = []hne:a + 1 ≠ chc':configs cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true) =
configs after (2 * Counter.flips a.bits + 1)⊢ machine.outputString cfg (1 + (2 * Counter.flips a.bits + 1)) = []
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshnext:(a + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips a.bits + 1)) (if a + 1 = c then stDone else stTree) (a + 1) chp':(configs after (2 * Counter.flips a.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips a.bits + 1) = []hne:a + 1 ≠ chc':configs cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true) =
configs after (2 * Counter.flips a.bits + 1)⊢ [] ++ [] = []
All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshnext:(a + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips a.bits + 1)) (if a + 1 = c then stDone else stTree) (a + 1) chp':(configs after (2 * Counter.flips a.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips a.bits + 1) = []hne:a + 1 ≠ chc':configs cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true) =
configs after (2 * Counter.flips a.bits + 1)⊢ ∀ u ≤ macroCost { mode := Mode.tree, forks := a, leaves := c } true, HeadBound width (configs cfg u) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshnext:(a + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips a.bits + 1)) (if a + 1 = c then stDone else stTree) (a + 1) chp':(configs after (2 * Counter.flips a.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips a.bits + 1) = []hne:a + 1 ≠ chc':configs cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true) =
configs after (2 * Counter.flips a.bits + 1)⊢ ∀ t ≤ 2 * Counter.flips a.bits + 1, HeadBound width (configs (configs cfg 1) t)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshnext:(a + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips a.bits + 1)) (if a + 1 = c then stDone else stTree) (a + 1) chp':(configs after (2 * Counter.flips a.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips a.bits + 1) = []hne:a + 1 ≠ chc':configs cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true) =
configs after (2 * Counter.flips a.bits + 1)u:ℕhu:u ≤ 2 * Counter.flips a.bits + 1⊢ HeadBound width (configs (configs cfg 1) u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.tree, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.tree, forks := a, leaves := c }.mode)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.tree, forks := a, leaves := c }.mode true)
{ mode := Mode.tree, forks := a, leaves := c }.forks { mode := Mode.tree, forks := a, leaves := c }.leaveshnext:(a + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips a.bits + 1)) (if a + 1 = c then stDone else stTree) (a + 1) chp':(configs after (2 * Counter.flips a.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips a.bits + 1) = []hne:a + 1 ≠ chc':configs cfg (macroCost { mode := Mode.tree, forks := a, leaves := c } true) =
configs after (2 * Counter.flips a.bits + 1)u:ℕhu:u ≤ 2 * Counter.flips a.bits + 1⊢ HeadBound width (configs after u)
All goals completed! 🐙
case string.false input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaves⊢ let cost := macroCost { mode := Mode.string, forks := a, leaves := c } false;
let next := accountStep { mode := Mode.string, forks := a, leaves := c } false;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshnext:(c + 1).size ≤ width⊢ let cost := macroCost { mode := Mode.string, forks := a, leaves := c } false;
let next := accountStep { mode := Mode.string, forks := a, leaves := c } false;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshnext:(c + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips (if true = true then c else a).bits + 1))
(if (if true = true then a else a + 1) = if true = true then c + 1 else c then stDone else stTree)
(if true = true then a else a + 1) (if true = true then c + 1 else c)hp':(configs after (2 * Counter.flips (if true = true then c else a).bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips (if true = true then c else a).bits + 1) = []⊢ let cost := macroCost { mode := Mode.string, forks := a, leaves := c } false;
let next := accountStep { mode := Mode.string, forks := a, leaves := c } false;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshnext:(c + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips c.bits + 1)) (if a = c + 1 then stDone else stTree) a (c + 1)hp':(configs after (2 * Counter.flips c.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips c.bits + 1) = []⊢ let cost := macroCost { mode := Mode.string, forks := a, leaves := c } false;
let next := accountStep { mode := Mode.string, forks := a, leaves := c } false;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshnext:(c + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips c.bits + 1)) (if a = c + 1 then stDone else stTree) a (c + 1)hp':(configs after (2 * Counter.flips c.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips c.bits + 1) = []hmode:modeState (accountStep { mode := Mode.string, forks := a, leaves := c } false).mode =
if a = c + 1 then stDone else stTree⊢ let cost := macroCost { mode := Mode.string, forks := a, leaves := c } false;
let next := accountStep { mode := Mode.string, forks := a, leaves := c } false;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshnext:(c + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips c.bits + 1)) (if a = c + 1 then stDone else stTree) a (c + 1)hp':(configs after (2 * Counter.flips c.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips c.bits + 1) = []hmode:modeState (accountStep { mode := Mode.string, forks := a, leaves := c } false).mode =
if a = c + 1 then stDone else stTreehc':configs cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false) =
configs after (2 * Counter.flips c.bits + 1)⊢ let cost := macroCost { mode := Mode.string, forks := a, leaves := c } false;
let next := accountStep { mode := Mode.string, forks := a, leaves := c } false;
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(configs cfg cost).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg cost = [] ∧ ∀ u ≤ cost, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshnext:(c + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips c.bits + 1)) (if a = c + 1 then stDone else stTree) a (c + 1)hp':(configs after (2 * Counter.flips c.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips c.bits + 1) = []hmode:modeState (accountStep { mode := Mode.string, forks := a, leaves := c } false).mode =
if a = c + 1 then stDone else stTreehc':configs cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false) =
configs after (2 * Counter.flips c.bits + 1)⊢ Represents width (configs cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false))
(modeState (accountStep { mode := Mode.string, forks := a, leaves := c } false).mode)
(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks
(accountStep { mode := Mode.string, forks := a, leaves := c } false).leavesinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshnext:(c + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips c.bits + 1)) (if a = c + 1 then stDone else stTree) a (c + 1)hp':(configs after (2 * Counter.flips c.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips c.bits + 1) = []hmode:modeState (accountStep { mode := Mode.string, forks := a, leaves := c } false).mode =
if a = c + 1 then stDone else stTreehc':configs cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false) =
configs after (2 * Counter.flips c.bits + 1)⊢ (configs cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false)).inputPos = moveInputPos cfg.inputPos 1input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshnext:(c + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips c.bits + 1)) (if a = c + 1 then stDone else stTree) a (c + 1)hp':(configs after (2 * Counter.flips c.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips c.bits + 1) = []hmode:modeState (accountStep { mode := Mode.string, forks := a, leaves := c } false).mode =
if a = c + 1 then stDone else stTreehc':configs cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false) =
configs after (2 * Counter.flips c.bits + 1)⊢ machine.outputString cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false) = []input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshnext:(c + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips c.bits + 1)) (if a = c + 1 then stDone else stTree) a (c + 1)hp':(configs after (2 * Counter.flips c.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips c.bits + 1) = []hmode:modeState (accountStep { mode := Mode.string, forks := a, leaves := c } false).mode =
if a = c + 1 then stDone else stTreehc':configs cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false) =
configs after (2 * Counter.flips c.bits + 1)⊢ ∀ u ≤ macroCost { mode := Mode.string, forks := a, leaves := c } false, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshnext:(c + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips c.bits + 1)) (if a = c + 1 then stDone else stTree) a (c + 1)hp':(configs after (2 * Counter.flips c.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips c.bits + 1) = []hmode:modeState (accountStep { mode := Mode.string, forks := a, leaves := c } false).mode =
if a = c + 1 then stDone else stTreehc':configs cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false) =
configs after (2 * Counter.flips c.bits + 1)⊢ Represents width (configs cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false))
(modeState (accountStep { mode := Mode.string, forks := a, leaves := c } false).mode)
(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks
(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshnext:(c + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips c.bits + 1)) (if a = c + 1 then stDone else stTree) a (c + 1)hp':(configs after (2 * Counter.flips c.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips c.bits + 1) = []hmode:modeState (accountStep { mode := Mode.string, forks := a, leaves := c } false).mode =
if a = c + 1 then stDone else stTreehc':configs cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false) =
configs after (2 * Counter.flips c.bits + 1)⊢ Represents width (configs after (2 * Counter.flips c.bits + 1)) (if a = c + 1 then stDone else stTree)
(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks
(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves
All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshnext:(c + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips c.bits + 1)) (if a = c + 1 then stDone else stTree) a (c + 1)hp':(configs after (2 * Counter.flips c.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips c.bits + 1) = []hmode:modeState (accountStep { mode := Mode.string, forks := a, leaves := c } false).mode =
if a = c + 1 then stDone else stTreehc':configs cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false) =
configs after (2 * Counter.flips c.bits + 1)⊢ (configs cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false)).inputPos = moveInputPos cfg.inputPos 1 input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshnext:(c + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips c.bits + 1)) (if a = c + 1 then stDone else stTree) a (c + 1)hp':(configs after (2 * Counter.flips c.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips c.bits + 1) = []hmode:modeState (accountStep { mode := Mode.string, forks := a, leaves := c } false).mode =
if a = c + 1 then stDone else stTreehc':configs cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false) =
configs after (2 * Counter.flips c.bits + 1)⊢ after.inputPos = moveInputPos cfg.inputPos 1
All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshnext:(c + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips c.bits + 1)) (if a = c + 1 then stDone else stTree) a (c + 1)hp':(configs after (2 * Counter.flips c.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips c.bits + 1) = []hmode:modeState (accountStep { mode := Mode.string, forks := a, leaves := c } false).mode =
if a = c + 1 then stDone else stTreehc':configs cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false) =
configs after (2 * Counter.flips c.bits + 1)⊢ machine.outputString cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshnext:(c + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips c.bits + 1)) (if a = c + 1 then stDone else stTree) a (c + 1)hp':(configs after (2 * Counter.flips c.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips c.bits + 1) = []hmode:modeState (accountStep { mode := Mode.string, forks := a, leaves := c } false).mode =
if a = c + 1 then stDone else stTreehc':configs cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false) =
configs after (2 * Counter.flips c.bits + 1)⊢ machine.outputString cfg (1 + (2 * Counter.flips c.bits + 1)) = []
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshnext:(c + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips c.bits + 1)) (if a = c + 1 then stDone else stTree) a (c + 1)hp':(configs after (2 * Counter.flips c.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips c.bits + 1) = []hmode:modeState (accountStep { mode := Mode.string, forks := a, leaves := c } false).mode =
if a = c + 1 then stDone else stTreehc':configs cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false) =
configs after (2 * Counter.flips c.bits + 1)⊢ [] ++ [] = []
All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshnext:(c + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips c.bits + 1)) (if a = c + 1 then stDone else stTree) a (c + 1)hp':(configs after (2 * Counter.flips c.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips c.bits + 1) = []hmode:modeState (accountStep { mode := Mode.string, forks := a, leaves := c } false).mode =
if a = c + 1 then stDone else stTreehc':configs cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false) =
configs after (2 * Counter.flips c.bits + 1)⊢ ∀ u ≤ macroCost { mode := Mode.string, forks := a, leaves := c } false, HeadBound width (configs cfg u) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshnext:(c + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips c.bits + 1)) (if a = c + 1 then stDone else stTree) a (c + 1)hp':(configs after (2 * Counter.flips c.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips c.bits + 1) = []hmode:modeState (accountStep { mode := Mode.string, forks := a, leaves := c } false).mode =
if a = c + 1 then stDone else stTreehc':configs cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false) =
configs after (2 * Counter.flips c.bits + 1)⊢ ∀ t ≤ 2 * Counter.flips c.bits + 1, HeadBound width (configs (configs cfg 1) t)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshnext:(c + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips c.bits + 1)) (if a = c + 1 then stDone else stTree) a (c + 1)hp':(configs after (2 * Counter.flips c.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips c.bits + 1) = []hmode:modeState (accountStep { mode := Mode.string, forks := a, leaves := c } false).mode =
if a = c + 1 then stDone else stTreehc':configs cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false) =
configs after (2 * Counter.flips c.bits + 1)u:ℕhu:u ≤ 2 * Counter.flips c.bits + 1⊢ HeadBound width (configs (configs cfg 1) u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.string, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.string, forks := a, leaves := c }.mode)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb false)ha:(accountStep { mode := Mode.string, forks := a, leaves := c } false).forks.size ≤ widthhb:(accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.string, forks := a, leaves := c }.mode false)
{ mode := Mode.string, forks := a, leaves := c }.forks { mode := Mode.string, forks := a, leaves := c }.leaveshnext:(c + 1).size ≤ widthhr':Represents width (configs after (2 * Counter.flips c.bits + 1)) (if a = c + 1 then stDone else stTree) a (c + 1)hp':(configs after (2 * Counter.flips c.bits + 1)).inputPos = after.inputPosho':machine.outputString after (2 * Counter.flips c.bits + 1) = []hmode:modeState (accountStep { mode := Mode.string, forks := a, leaves := c } false).mode =
if a = c + 1 then stDone else stTreehc':configs cfg (macroCost { mode := Mode.string, forks := a, leaves := c } false) =
configs after (2 * Counter.flips c.bits + 1)u:ℕhu:u ≤ 2 * Counter.flips c.bits + 1⊢ HeadBound width (configs after u)
All goals completed! 🐙
all_goals
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.dead, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.dead, forks := a, leaves := c }.mode)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.dead, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.dead, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode true)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leaves⊢ Represents width (configs cfg 1) (modeState (accountStep { mode := Mode.dead, forks := a, leaves := c } true).mode) a
c ∧
(configs cfg 1).inputPos = moveInputPos cfg.inputPos 1 ∧
machine.outputString cfg 1 = [] ∧ ∀ u ≤ 1, HeadBound width (configs cfg u)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.dead, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.dead, forks := a, leaves := c }.mode)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.dead, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.dead, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode true)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leaves⊢ Represents width (configs cfg 1) (modeState (accountStep { mode := Mode.dead, forks := a, leaves := c } true).mode) a cinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.dead, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.dead, forks := a, leaves := c }.mode)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.dead, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.dead, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode true)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leaves⊢ (configs cfg 1).inputPos = moveInputPos cfg.inputPos 1
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.dead, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.dead, forks := a, leaves := c }.mode)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.dead, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.dead, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode true)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leaves⊢ Represents width (configs cfg 1) (modeState (accountStep { mode := Mode.dead, forks := a, leaves := c } true).mode) a c input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.dead, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.dead, forks := a, leaves := c }.mode)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.dead, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.dead, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode true)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leaves⊢ Represents width after (modeState (accountStep { mode := Mode.dead, forks := a, leaves := c } true).mode) a c
All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.dead, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.dead, forks := a, leaves := c }.mode)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.dead, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.dead, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode true)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leaves⊢ (configs cfg 1).inputPos = moveInputPos cfg.inputPos 1 input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕho:machine.outputString cfg 1 = []hh:∀ u ≤ 1, HeadBound width (configs cfg u)a:ℕc:ℕhv:AccountValid { mode := Mode.dead, forks := a, leaves := c }h:Represents width cfg (modeState { mode := Mode.dead, forks := a, leaves := c }.mode)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leaveshi:cfg.inputSymbol = some (boolEmb true)ha:(accountStep { mode := Mode.dead, forks := a, leaves := c } true).forks.size ≤ widthhb:(accountStep { mode := Mode.dead, forks := a, leaves := c } true).leaves.size ≤ widthafter:Cfg 3 (Fin 4) (Fin 10) input := consumeCfg cfg (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode true)hc:configs cfg 1 = afterhr:Represents width after (postReadState { mode := Mode.dead, forks := a, leaves := c }.mode true)
{ mode := Mode.dead, forks := a, leaves := c }.forks { mode := Mode.dead, forks := a, leaves := c }.leaves⊢ after.inputPos = moveInputPos cfg.inputPos 1
All goals completed! 🐙One input bit realizes the accounting update in its prescribed macro cost.
theorem configs_bit (w : List Bool) (t : ℕ) (ht : t < w.length)
(cfg : Cfg 3 (Fin 4) (Fin 10) (w.map boolEmb)) (hp : cfg.inputPos.val = t + 1)
(s : Account) (width : ℕ) (hv : AccountValid s)
(h : Represents width cfg (modeState s.mode) s.forks s.leaves)
(ha : (accountStep s w[t]).forks.size ≤ width)
(hb : (accountStep s w[t]).leaves.size ≤ width) :
let cost := macroCost s w[t]
let next := accountStep s w[t]
Represents width (machine.configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
(machine.configs cfg cost).inputPos.val = t + 2 ∧ machine.outputString cfg cost = [] := w:List Boolt:ℕht:t < w.lengthcfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w)hp:↑cfg.inputPos = t + 1s:Accountwidth:ℕhv:AccountValid sh:Represents width cfg (modeState s.mode) s.forks s.leavesha:(accountStep s w[t]).forks.size ≤ widthhb:(accountStep s w[t]).leaves.size ≤ width⊢ let cost := macroCost s w[t];
let next := accountStep s w[t];
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
↑(configs cfg cost).inputPos = t + 2 ∧ machine.outputString cfg cost = []
w:List Boolt:ℕht:t < w.lengthcfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w)hp:↑cfg.inputPos = t + 1s:Accountwidth:ℕhv:AccountValid sh:Represents width cfg (modeState s.mode) s.forks s.leavesha:(accountStep s w[t]).forks.size ≤ widthhb:(accountStep s w[t]).leaves.size ≤ widthhr:Represents width (configs cfg (macroCost s w[t])) (modeState (accountStep s w[t]).mode) (accountStep s w[t]).forks
(accountStep s w[t]).leaveshp':(configs cfg (macroCost s w[t])).inputPos = moveInputPos cfg.inputPos 1ho:machine.outputString cfg (macroCost s w[t]) = []right✝:∀ u ≤ macroCost s w[t], HeadBound width (configs cfg u)⊢ let cost := macroCost s w[t];
let next := accountStep s w[t];
Represents width (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
↑(configs cfg cost).inputPos = t + 2 ∧ machine.outputString cfg cost = []
w:List Boolt:ℕht:t < w.lengthcfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w)hp:↑cfg.inputPos = t + 1s:Accountwidth:ℕhv:AccountValid sh:Represents width cfg (modeState s.mode) s.forks s.leavesha:(accountStep s w[t]).forks.size ≤ widthhb:(accountStep s w[t]).leaves.size ≤ widthhr:Represents width (configs cfg (macroCost s w[t])) (modeState (accountStep s w[t]).mode) (accountStep s w[t]).forks
(accountStep s w[t]).leaveshp':(configs cfg (macroCost s w[t])).inputPos = moveInputPos cfg.inputPos 1ho:machine.outputString cfg (macroCost s w[t]) = []right✝:∀ u ≤ macroCost s w[t], HeadBound width (configs cfg u)⊢ ↑(configs cfg (macroCost s w[t])).inputPos = t + 2
w:List Boolt:ℕht:t < w.lengthcfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w)hp:↑cfg.inputPos = t + 1s:Accountwidth:ℕhv:AccountValid sh:Represents width cfg (modeState s.mode) s.forks s.leavesha:(accountStep s w[t]).forks.size ≤ widthhb:(accountStep s w[t]).leaves.size ≤ widthhr:Represents width (configs cfg (macroCost s w[t])) (modeState (accountStep s w[t]).mode) (accountStep s w[t]).forks
(accountStep s w[t]).leaveshp':(configs cfg (macroCost s w[t])).inputPos = moveInputPos cfg.inputPos 1ho:machine.outputString cfg (macroCost s w[t]) = []right✝:∀ u ≤ macroCost s w[t], HeadBound width (configs cfg u)⊢ ↑(moveInputPos cfg.inputPos 1) = t + 2
w:List Boolt:ℕht:t < w.lengthcfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w)hp:↑cfg.inputPos = t + 1s:Accountwidth:ℕhv:AccountValid sh:Represents width cfg (modeState s.mode) s.forks s.leavesha:(accountStep s w[t]).forks.size ≤ widthhb:(accountStep s w[t]).leaves.size ≤ widthhr:Represents width (configs cfg (macroCost s w[t])) (modeState (accountStep s w[t]).mode) (accountStep s w[t]).forks
(accountStep s w[t]).leaveshp':(configs cfg (macroCost s w[t])).inputPos = moveInputPos cfg.inputPos 1ho:machine.outputString cfg (macroCost s w[t]) = []right✝:∀ u ≤ macroCost s w[t], HeadBound width (configs cfg u)hm:↑(consumeCfg cfg (postReadState s.mode w[t])).inputPos = ↑cfg.inputPos + 1⊢ ↑(moveInputPos cfg.inputPos 1) = t + 2
w:List Boolt:ℕht:t < w.lengthcfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w)hp:↑cfg.inputPos = t + 1s:Accountwidth:ℕhv:AccountValid sh:Represents width cfg (modeState s.mode) s.forks s.leavesha:(accountStep s w[t]).forks.size ≤ widthhb:(accountStep s w[t]).leaves.size ≤ widthhr:Represents width (configs cfg (macroCost s w[t])) (modeState (accountStep s w[t]).mode) (accountStep s w[t]).forks
(accountStep s w[t]).leaveshp':(configs cfg (macroCost s w[t])).inputPos = moveInputPos cfg.inputPos 1ho:machine.outputString cfg (macroCost s w[t]) = []right✝:∀ u ≤ macroCost s w[t], HeadBound width (configs cfg u)hm:↑(moveInputPos cfg.inputPos 1) = ↑cfg.inputPos + 1⊢ ↑(moveInputPos cfg.inputPos 1) = t + 2
All goals completed! 🐙Every head remains within the chosen binary width during a complete input-bit segment.
theorem configs_bit_head_bounds (w : List Bool) (t : ℕ) (ht : t < w.length)
(cfg : Cfg 3 (Fin 4) (Fin 10) (w.map boolEmb)) (hp : cfg.inputPos.val = t + 1)
(s : Account) (width : ℕ) (hv : AccountValid s)
(h : Represents width cfg (modeState s.mode) s.forks s.leaves)
(ha : (accountStep s w[t]).forks.size ≤ width)
(hb : (accountStep s w[t]).leaves.size ≤ width) :
∀ u ≤ macroCost s w[t], HeadBound width (machine.configs cfg u) :=
(configs_bit_aux cfg s w[t] width hv h (inputSymbol_at w t ht cfg hp) ha hb).2.2.2end Geb.BitTree.BinaryMachine