1. Geb
  2. Prototypes
  3. Computability
  4. BitTree
  5. BinaryMachine
  6. Macro
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.Carry public import Geb.Prototypes.Computability.BitTree.BinaryMachine.Return public import Geb.Prototypes.Computability.BitTree.BinaryMachine.Representation
set_option doc.verso true

Complete counter increments

A carry followed by the return is one counter increment. The marker and mismatch invariants connect its final state to equality of the represented counter values.

Main statements

  • configs_carry_invariants maintains marker and mismatch invariants.

  • configs_increment implements one increment in twice its bit-change count plus one step.

  • configs_increment_head_bounds bounds every visited work-tape position.

Tags

Turing machine, simulation, binary counter

@[expose] public sectionnamespace Geb.BitTree.BinaryMachineopen Turing MultiTapeTM

The marker and mismatch invariants survive every carry prefix, including its last step.

theorem configs_carry_invariants {input : List (Fin 4)} (cfg : Cfg 3 (Fin 4) (Fin 10) input) (leaf : Bool) (p k width : ℕ) (hq : cfg.state = some (if leaf then stCarryLeaf else stCarryFork)) (hp0 : cfg.workTapePos 0 = p) (hp1 : cfg.workTapePos 1 = p) (hones : ∀ j < k, digits cfg (if leaf then 1 else 0) (p + j) = true) (hw : p + k < width) (hm : cfg.workTapePos 2 = (mismatchCount width (digits cfg 0) (digits cfg 1) : ℤ)) (t : ℕ) (ht : t ≤ k + 1) : let now := machine.configs cfg t (∀ z, origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = (mismatchCount width (digits now 0) (digits now 1) : ℤ) := input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehw:p + k < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t:ℕht:t ≤ k + 1⊢ let now := configs cfg t; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1)) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehw:p + k < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t:ℕ⊢ t ≤ k + 1 → let now := configs cfg t; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1)) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehw:p + k < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t:ℕ⊢ Nat.zero ≤ k + 1 → let now := configs cfg Nat.zero; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1))input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehw:p + k < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t:ℕ⊢ ∀ (n : ℕ), (n ≤ k + 1 → let now := configs cfg n; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1))) → n.succ ≤ k + 1 → let now := configs cfg n.succ; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1)) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehw:p + k < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t:ℕ⊢ Nat.zero ≤ k + 1 → let now := configs cfg Nat.zero; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1)) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehw:p + k < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t:ℕa✝:Nat.zero ≤ k + 1⊢ let now := configs cfg Nat.zero; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1)) All goals completed! 🐙 input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehw:p + k < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t:ℕ⊢ ∀ (n : ℕ), (n ≤ k + 1 → let now := configs cfg n; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1))) → n.succ ≤ k + 1 → let now := configs cfg n.succ; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1)) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehw:p + k < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t✝:ℕt:ℕih:t ≤ k + 1 → let now := configs cfg t; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1))ht:t.succ ≤ k + 1⊢ let now := configs cfg t.succ; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1)) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehw:p + k < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t✝:ℕt:ℕih:t ≤ k + 1 → let now := configs cfg t; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1))ht:t.succ ≤ k + 1ho:∀ (z : ℤ), origin ((configs cfg t).workTapes 0 z) = origin (cfg.workTapes 0 z)hmark:(configs cfg t).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))⊢ let now := configs cfg t.succ; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1)) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehw:p + k < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t✝:ℕt:ℕih:t ≤ k + 1 → let now := configs cfg t; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1))ht:t.succ ≤ k + 1ho:∀ (z : ℤ), origin ((configs cfg t).workTapes 0 z) = origin (cfg.workTapes 0 z)hmark:(configs cfg t).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)right✝:(configs cfg t).inputPos = cfg.inputPos ∧ (digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧ digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ let now := configs cfg t.succ; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1)) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehw:p + k < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t✝:ℕt:ℕih:t ≤ k + 1 → let now := configs cfg t; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1))ht:t.succ ≤ k + 1ho:∀ (z : ℤ), origin ((configs cfg t).workTapes 0 z) = origin (cfg.workTapes 0 z)hmark:(configs cfg t).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)right✝:(configs cfg t).inputPos = cfg.inputPos ∧ (digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧ digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ let now := MultiTapeTM.step (configs cfg t); (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1)) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehw:p + k < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t✝:ℕt:ℕih:t ≤ k + 1 → let now := configs cfg t; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1))ht:t.succ ≤ k + 1ho:∀ (z : ℤ), origin ((configs cfg t).workTapes 0 z) = origin (cfg.workTapes 0 z)hmark:(configs cfg t).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)right✝:(configs cfg t).inputPos = cfg.inputPos ∧ (digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧ digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ ∀ (z : ℤ), origin ((MultiTapeTM.step (configs cfg t)).workTapes 0 z) = origin (cfg.workTapes 0 z)input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehw:p + k < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t✝:ℕt:ℕih:t ≤ k + 1 → let now := configs cfg t; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1))ht:t.succ ≤ k + 1ho:∀ (z : ℤ), origin ((configs cfg t).workTapes 0 z) = origin (cfg.workTapes 0 z)hmark:(configs cfg t).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)right✝:(configs cfg t).inputPos = cfg.inputPos ∧ (digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧ digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ (MultiTapeTM.step (configs cfg t)).workTapes 2 = cfg.workTapes 2input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehw:p + k < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t✝:ℕt:ℕih:t ≤ k + 1 → let now := configs cfg t; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1))ht:t.succ ≤ k + 1ho:∀ (z : ℤ), origin ((configs cfg t).workTapes 0 z) = origin (cfg.workTapes 0 z)hmark:(configs cfg t).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)right✝:(configs cfg t).inputPos = cfg.inputPos ∧ (digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧ digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ (MultiTapeTM.step (configs cfg t)).workTapePos 2 = ↑(mismatchCount width (digits (MultiTapeTM.step (configs cfg t)) 0) (digits (MultiTapeTM.step (configs cfg t)) 1)) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehw:p + k < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t✝:ℕt:ℕih:t ≤ k + 1 → let now := configs cfg t; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1))ht:t.succ ≤ k + 1ho:∀ (z : ℤ), origin ((configs cfg t).workTapes 0 z) = origin (cfg.workTapes 0 z)hmark:(configs cfg t).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)right✝:(configs cfg t).inputPos = cfg.inputPos ∧ (digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧ digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ ∀ (z : ℤ), origin ((MultiTapeTM.step (configs cfg t)).workTapes 0 z) = origin (cfg.workTapes 0 z) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehw:p + k < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t✝:ℕt:ℕih:t ≤ k + 1 → let now := configs cfg t; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1))ht:t.succ ≤ k + 1ho:∀ (z : ℤ), origin ((configs cfg t).workTapes 0 z) = origin (cfg.workTapes 0 z)hmark:(configs cfg t).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)right✝:(configs cfg t).inputPos = cfg.inputPos ∧ (digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧ digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)z:ℤ⊢ origin ((MultiTapeTM.step (configs cfg t)).workTapes 0 z) = origin (cfg.workTapes 0 z) All goals completed! 🐙 input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehw:p + k < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t✝:ℕt:ℕih:t ≤ k + 1 → let now := configs cfg t; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1))ht:t.succ ≤ k + 1ho:∀ (z : ℤ), origin ((configs cfg t).workTapes 0 z) = origin (cfg.workTapes 0 z)hmark:(configs cfg t).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)right✝:(configs cfg t).inputPos = cfg.inputPos ∧ (digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧ digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ (MultiTapeTM.step (configs cfg t)).workTapes 2 = cfg.workTapes 2 All goals completed! 🐙 input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehw:p + k < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t✝:ℕt:ℕih:t ≤ k + 1 → let now := configs cfg t; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1))ht:t.succ ≤ k + 1ho:∀ (z : ℤ), origin ((configs cfg t).workTapes 0 z) = origin (cfg.workTapes 0 z)hmark:(configs cfg t).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)right✝:(configs cfg t).inputPos = cfg.inputPos ∧ (digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧ digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ (MultiTapeTM.step (configs cfg t)).workTapePos 2 = ↑(mismatchCount width (digits (MultiTapeTM.step (configs cfg t)) 0) (digits (MultiTapeTM.step (configs cfg t)) 1)) exact step_carry_mismatch _ leaf width (p + t) hstate hpos0 hpos1 (input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehw:p + k < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t✝:ℕt:ℕih:t ≤ k + 1 → let now := configs cfg t; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1))ht:t.succ ≤ k + 1ho:∀ (z : ℤ), origin ((configs cfg t).workTapes 0 z) = origin (cfg.workTapes 0 z)hmark:(configs cfg t).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)right✝:(configs cfg t).inputPos = cfg.inputPos ∧ (digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧ digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ p + t < width All goals completed! 🐙) hmismatch

Marker and mismatch invariants throughout the carry of a represented bit list.

theorem configs_carry_bits_invariants {input : List (Fin 4)} (cfg : Cfg 3 (Fin 4) (Fin 10) input) (leaf : Bool) (bs : List Bool) (width : ℕ) (hq : cfg.state = some (if leaf then stCarryLeaf else stCarryFork)) (hp0 : cfg.workTapePos 0 = 0) (hp1 : cfg.workTapePos 1 = 0) (hbits : ∀ j, digits cfg (if leaf then 1 else 0) j = bs[j]?.getD false) (hw : Counter.flips bs ≤ width) (hm : cfg.workTapePos 2 = (mismatchCount width (digits cfg 0) (digits cfg 1) : ℤ)) (t : ℕ) (ht : t ≤ Counter.flips bs) : let now := machine.configs cfg t (∀ z, origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = (mismatchCount width (digits now 0) (digits now 1) : ℤ) := input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehw:Counter.flips bs ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t:ℕht:t ≤ Counter.flips bs⊢ let now := configs cfg t; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1)) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehw:Counter.flips bs ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t:ℕht:t ≤ Counter.flips bshpos:0 < Counter.flips bs⊢ let now := configs cfg t; (∀ (z : ℤ), origin (now.workTapes 0 z) = origin (cfg.workTapes 0 z)) ∧ now.workTapes 2 = cfg.workTapes 2 ∧ now.workTapePos 2 = ↑(mismatchCount width (digits now 0) (digits now 1)) apply configs_carry_invariants cfg leaf 0 (Counter.flips bs - 1) width hq hp0 hp1 ?_ (input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehw:Counter.flips bs ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t:ℕht:t ≤ Counter.flips bshpos:0 < Counter.flips bs⊢ 0 + (Counter.flips bs - 1) < width All goals completed! 🐙) hm t (input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehw:Counter.flips bs ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t:ℕht:t ≤ Counter.flips bshpos:0 < Counter.flips bs⊢ t ≤ Counter.flips bs - 1 + 1 All goals completed! 🐙) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehw:Counter.flips bs ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t:ℕht:t ≤ Counter.flips bshpos:0 < Counter.flips bsj:ℕhj:j < Counter.flips bs - 1⊢ digits cfg (if leaf = true then 1 else 0) (0 + j) = true input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehw:Counter.flips bs ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t:ℕht:t ≤ Counter.flips bshpos:0 < Counter.flips bsj:ℕhj:j < Counter.flips bs - 1⊢ bs[j]?.getD false = true exact Counter.getD_eq_true_of_lt_flips bs j (input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolwidth:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehw:Counter.flips bs ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))t:ℕht:t ≤ Counter.flips bshpos:0 < Counter.flips bsj:ℕhj:j < Counter.flips bs - 1⊢ j + 1 < Counter.flips bs All goals completed! 🐙)

A complete carry and return implements one increment and tests equality.

theorem configs_increment {input : List (Fin 4)} (cfg : Cfg 3 (Fin 4) (Fin 10) input) (leaf : Bool) (width a b : ℕ) (h : Represents width cfg (if leaf then stCarryLeaf else stCarryFork) a b) (hnext : ((if leaf then b else a) + 1).size ≤ width) : let f := Counter.flips (if leaf then b else a).bits let a' := if leaf then a else a + 1 let b' := if leaf then b + 1 else b let now := machine.configs cfg (2 * f + 1) Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] := input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ width⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else a⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bits⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else b⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg f⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD false⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehstate:(configs cfg (Counter.flips n.bits)).state = some stReturnhpos0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hpos1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)hin:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD falsehother:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)hout:machine.outputString cfg (Counter.flips n.bits) = []⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehstate:(configs cfg (Counter.flips n.bits)).state = some stReturnhpos0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hpos1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)hin:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD falsehother:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)hout:machine.outputString cfg (Counter.flips n.bits) = []hw:f ≤ width⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehstate:(configs cfg (Counter.flips n.bits)).state = some stReturnhpos0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hpos1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)hin:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD falsehother:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)hout:machine.outputString cfg (Counter.flips n.bits) = []hw:f ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehstate:(configs cfg (Counter.flips n.bits)).state = some stReturnhpos0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hpos1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)hin:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD falsehother:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)hout:machine.outputString cfg (Counter.flips n.bits) = []hw:f ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)hmarker:(configs cfg f).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehstate:(configs cfg (Counter.flips n.bits)).state = some stReturnhpos0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hpos1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)hin:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD falsehother:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)hout:machine.outputString cfg (Counter.flips n.bits) = []hw:f ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)hmarker:(configs cfg f).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))hd0:digits after 0 = bitsAt a'⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehstate:(configs cfg (Counter.flips n.bits)).state = some stReturnhpos0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hpos1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)hin:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD falsehother:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)hout:machine.outputString cfg (Counter.flips n.bits) = []hw:f ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)hmarker:(configs cfg f).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))hd0:digits after 0 = bitsAt a'hd1:digits after 1 = bitsAt b'⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehstate:(configs cfg (Counter.flips n.bits)).state = some stReturnhpos0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hpos1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)hin:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD falsehother:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)hout:machine.outputString cfg (Counter.flips n.bits) = []hw:f ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)hmarker:(configs cfg f).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))hd0:digits after 0 = bitsAt a'hd1:digits after 1 = bitsAt b'ho:∀ (z : ℤ), origin (after.workTapes 0 z) = decide (z = 0)⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehstate:(configs cfg (Counter.flips n.bits)).state = some stReturnhpos0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hpos1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)hin:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD falsehother:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)hout:machine.outputString cfg (Counter.flips n.bits) = []hw:f ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)hmarker:(configs cfg f).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))hd0:digits after 0 = bitsAt a'hd1:digits after 1 = bitsAt b'ho:∀ (z : ℤ), origin (after.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), after.workTapes 2 z = if z = 0 then some 0 else none⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehstate:(configs cfg (Counter.flips n.bits)).state = some stReturnhpos0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hpos1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)hin:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD falsehother:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)hout:machine.outputString cfg (Counter.flips n.bits) = []hw:f ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)hmarker:(configs cfg f).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))hd0:digits after 0 = bitsAt a'hd1:digits after 1 = bitsAt b'ho:∀ (z : ℤ), origin (after.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), after.workTapes 2 z = if z = 0 then some 0 else nonehm':after.workTapePos 2 = ↑(mismatchCount width (bitsAt a') (bitsAt b'))⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehstate:(configs cfg (Counter.flips n.bits)).state = some stReturnhpos0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hpos1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)hin:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD falsehother:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)hout:machine.outputString cfg (Counter.flips n.bits) = []hw:f ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)hmarker:(configs cfg f).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))hd0:digits after 0 = bitsAt a'hd1:digits after 1 = bitsAt b'ho:∀ (z : ℤ), origin (after.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), after.workTapes 2 z = if z = 0 then some 0 else nonehm':after.workTapePos 2 = ↑(mismatchCount width (bitsAt a') (bitsAt b'))ha':a'.size ≤ width⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehstate:(configs cfg (Counter.flips n.bits)).state = some stReturnhpos0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hpos1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)hin:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD falsehother:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)hout:machine.outputString cfg (Counter.flips n.bits) = []hw:f ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)hmarker:(configs cfg f).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))hd0:digits after 0 = bitsAt a'hd1:digits after 1 = bitsAt b'ho:∀ (z : ℤ), origin (after.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), after.workTapes 2 z = if z = 0 then some 0 else nonehm':after.workTapePos 2 = ↑(mismatchCount width (bitsAt a') (bitsAt b'))ha':a'.size ≤ widthhb':b'.size ≤ width⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehstate:(configs cfg (Counter.flips n.bits)).state = some stReturnhpos0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hpos1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)hin:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD falsehother:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)hout:machine.outputString cfg (Counter.flips n.bits) = []hw:f ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)hmarker:(configs cfg f).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))hd0:digits after 0 = bitsAt a'hd1:digits after 1 = bitsAt b'ho:∀ (z : ℤ), origin (after.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), after.workTapes 2 z = if z = 0 then some 0 else nonehm':after.workTapePos 2 = ↑(mismatchCount width (bitsAt a') (bitsAt b'))ha':a'.size ≤ widthhb':b'.size ≤ widthhr:Represents width (returnedCfg after) (if a' = b' then stDone else stTree) a' b'⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehstate:(configs cfg (Counter.flips n.bits)).state = some stReturnhpos0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hpos1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)hin:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD falsehother:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)hout:machine.outputString cfg (Counter.flips n.bits) = []hw:f ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)hmarker:(configs cfg f).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))hd0:digits after 0 = bitsAt a'hd1:digits after 1 = bitsAt b'ho:∀ (z : ℤ), origin (after.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), after.workTapes 2 z = if z = 0 then some 0 else nonehm':after.workTapePos 2 = ↑(mismatchCount width (bitsAt a') (bitsAt b'))ha':a'.size ≤ widthhb':b'.size ≤ widthhr:Represents width (returnedCfg after) (if a' = b' then stDone else stTree) a' b'he:returnCfg after f = after⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehstate:(configs cfg (Counter.flips n.bits)).state = some stReturnhpos0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hpos1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)hin:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD falsehother:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)hout:machine.outputString cfg (Counter.flips n.bits) = []hw:f ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)hmarker:(configs cfg f).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))hd0:digits after 0 = bitsAt a'hd1:digits after 1 = bitsAt b'ho:∀ (z : ℤ), origin (after.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), after.workTapes 2 z = if z = 0 then some 0 else nonehm':after.workTapePos 2 = ↑(mismatchCount width (bitsAt a') (bitsAt b'))ha':a'.size ≤ widthhb':b'.size ≤ widthhr:Represents width (returnedCfg after) (if a' = b' then stDone else stTree) a' b'he:returnCfg after f = afterhc:configs (returnCfg after f) (f + 1) = returnedCfg afterho':machine.outputString (returnCfg after f) (f + 1) = []⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehstate:(configs cfg (Counter.flips n.bits)).state = some stReturnhpos0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hpos1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)hin:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD falsehother:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)hout:machine.outputString cfg (Counter.flips n.bits) = []hw:f ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)hmarker:(configs cfg f).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))hd0:digits after 0 = bitsAt a'hd1:digits after 1 = bitsAt b'ho:∀ (z : ℤ), origin (after.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), after.workTapes 2 z = if z = 0 then some 0 else nonehm':after.workTapePos 2 = ↑(mismatchCount width (bitsAt a') (bitsAt b'))ha':a'.size ≤ widthhb':b'.size ≤ widthhr:Represents width (returnedCfg after) (if a' = b' then stDone else stTree) a' b'he:returnCfg after f = afterhc:configs after (f + 1) = returnedCfg afterho':machine.outputString after (f + 1) = []⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehstate:(configs cfg (Counter.flips n.bits)).state = some stReturnhpos0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hpos1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)hin:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD falsehother:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)hout:machine.outputString cfg (Counter.flips n.bits) = []hw:f ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)hmarker:(configs cfg f).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))hd0:digits after 0 = bitsAt a'hd1:digits after 1 = bitsAt b'ho:∀ (z : ℤ), origin (after.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), after.workTapes 2 z = if z = 0 then some 0 else nonehm':after.workTapePos 2 = ↑(mismatchCount width (bitsAt a') (bitsAt b'))ha':a'.size ≤ widthhb':b'.size ≤ widthhr:Represents width (returnedCfg after) (if a' = b' then stDone else stTree) a' b'he:returnCfg after f = afterhc:configs after (f + 1) = returnedCfg afterho':machine.outputString after (f + 1) = []hfinal:configs cfg (2 * f + 1) = returnedCfg after⊢ let f := Counter.flips (if leaf = true then b else a).bits; let a' := if leaf = true then a else a + 1; let b' := if leaf = true then b + 1 else b; let now := configs cfg (2 * f + 1); Represents width now (if a' = b' then stDone else stTree) a' b' ∧ now.inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * f + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehstate:(configs cfg (Counter.flips n.bits)).state = some stReturnhpos0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hpos1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)hin:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD falsehother:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)hout:machine.outputString cfg (Counter.flips n.bits) = []hw:f ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)hmarker:(configs cfg f).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))hd0:digits after 0 = bitsAt a'hd1:digits after 1 = bitsAt b'ho:∀ (z : ℤ), origin (after.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), after.workTapes 2 z = if z = 0 then some 0 else nonehm':after.workTapePos 2 = ↑(mismatchCount width (bitsAt a') (bitsAt b'))ha':a'.size ≤ widthhb':b'.size ≤ widthhr:Represents width (returnedCfg after) (if a' = b' then stDone else stTree) a' b'he:returnCfg after f = afterhc:configs after (f + 1) = returnedCfg afterho':machine.outputString after (f + 1) = []hfinal:configs cfg (2 * f + 1) = returnedCfg after⊢ Represents width (configs cfg (2 * Counter.flips (if leaf = true then b else a).bits + 1)) (if (if leaf = true then a else a + 1) = if leaf = true then b + 1 else b then stDone else stTree) a' b' ∧ (configs cfg (2 * Counter.flips (if leaf = true then b else a).bits + 1)).inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * Counter.flips (if leaf = true then b else a).bits + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehstate:(configs cfg (Counter.flips n.bits)).state = some stReturnhpos0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hpos1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)hin:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD falsehother:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)hout:machine.outputString cfg (Counter.flips n.bits) = []hw:f ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)hmarker:(configs cfg f).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))hd0:digits after 0 = bitsAt a'hd1:digits after 1 = bitsAt b'ho:∀ (z : ℤ), origin (after.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), after.workTapes 2 z = if z = 0 then some 0 else nonehm':after.workTapePos 2 = ↑(mismatchCount width (bitsAt a') (bitsAt b'))ha':a'.size ≤ widthhb':b'.size ≤ widthhr:Represents width (returnedCfg after) (if a' = b' then stDone else stTree) a' b'he:returnCfg after f = afterhc:configs after (f + 1) = returnedCfg afterho':machine.outputString after (f + 1) = []hfinal:configs cfg (2 * f + 1) = returnedCfg after⊢ Represents width (returnedCfg after) (if (if leaf = true then a else a + 1) = if leaf = true then b + 1 else b then stDone else stTree) a' b' ∧ (returnedCfg after).inputPos = cfg.inputPos ∧ machine.outputString cfg (2 * Counter.flips (if leaf = true then b else a).bits + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehstate:(configs cfg (Counter.flips n.bits)).state = some stReturnhpos0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hpos1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)hin:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD falsehother:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)hout:machine.outputString cfg (Counter.flips n.bits) = []hw:f ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)hmarker:(configs cfg f).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))hd0:digits after 0 = bitsAt a'hd1:digits after 1 = bitsAt b'ho:∀ (z : ℤ), origin (after.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), after.workTapes 2 z = if z = 0 then some 0 else nonehm':after.workTapePos 2 = ↑(mismatchCount width (bitsAt a') (bitsAt b'))ha':a'.size ≤ widthhb':b'.size ≤ widthhr:Represents width (returnedCfg after) (if a' = b' then stDone else stTree) a' b'he:returnCfg after f = afterhc:configs after (f + 1) = returnedCfg afterho':machine.outputString after (f + 1) = []hfinal:configs cfg (2 * f + 1) = returnedCfg after⊢ machine.outputString cfg (2 * Counter.flips (if leaf = true then b else a).bits + 1) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widthn:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitsa':ℕ := if leaf = true then a else a + 1b':ℕ := if leaf = true then b + 1 else bafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehstate:(configs cfg (Counter.flips n.bits)).state = some stReturnhpos0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hpos1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)hin:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD falsehother:digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)hout:machine.outputString cfg (Counter.flips n.bits) = []hw:f ≤ widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)hmarker:(configs cfg f).workTapes 2 = cfg.workTapes 2hmismatch:(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))hd0:digits after 0 = bitsAt a'hd1:digits after 1 = bitsAt b'ho:∀ (z : ℤ), origin (after.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), after.workTapes 2 z = if z = 0 then some 0 else nonehm':after.workTapePos 2 = ↑(mismatchCount width (bitsAt a') (bitsAt b'))ha':a'.size ≤ widthhb':b'.size ≤ widthhr:Represents width (returnedCfg after) (if a' = b' then stDone else stTree) a' b'he:returnCfg after f = afterhc:configs after (f + 1) = returnedCfg afterho':machine.outputString after (f + 1) = []hfinal:configs cfg (2 * f + 1) = returnedCfg after⊢ [] ++ [] = [] All goals completed! 🐙

Every work head stays within the fixed width during a complete increment.

theorem configs_increment_head_bounds {input : List (Fin 4)} (cfg : Cfg 3 (Fin 4) (Fin 10) input) (leaf : Bool) (width a b : ℕ) (h : Represents width cfg (if leaf then stCarryLeaf else stCarryFork) a b) (hnext : ((if leaf then b else a) + 1).size ≤ width) (t : ℕ) (ht : t ≤ 2 * Counter.flips (if leaf then b else a).bits + 1) (i : Fin 3) : 0 ≤ (machine.configs cfg t).workTapePos i ∧ (machine.configs cfg t).workTapePos i ≤ width := input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else a⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bits⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ width⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD false⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:t ≤ f⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑widthinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:¬t ≤ f⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:t ≤ f⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:t ≤ fhp0:(configs cfg t).workTapePos 0 = ↑thp1:(configs cfg t).workTapePos 1 = ↑t⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:t ≤ fhp0:(configs cfg t).workTapePos 0 = ↑thp1:(configs cfg t).workTapePos 1 = ↑thm':(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:t ≤ fhp0:(configs cfg t).workTapePos 0 = ↑thp1:(configs cfg t).workTapePos 1 = ↑thm':(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hcount:mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1) ≤ width⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:t ≤ fhp0:(configs cfg t).workTapePos 0 = ↑thp1:(configs cfg t).workTapePos 1 = ↑thm':(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hcount:mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1) ≤ width⊢ 0 ≤ (configs cfg t).workTapePos ((fun i ↦ i) ⟨0, ⋯⟩) ∧ (configs cfg t).workTapePos ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ↑widthinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:t ≤ fhp0:(configs cfg t).workTapePos 0 = ↑thp1:(configs cfg t).workTapePos 1 = ↑thm':(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hcount:mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1) ≤ width⊢ 0 ≤ (configs cfg t).workTapePos ((fun i ↦ i) ⟨1, ⋯⟩) ∧ (configs cfg t).workTapePos ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ↑widthinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:t ≤ fhp0:(configs cfg t).workTapePos 0 = ↑thp1:(configs cfg t).workTapePos 1 = ↑thm':(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hcount:mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1) ≤ width⊢ 0 ≤ (configs cfg t).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) ∧ (configs cfg t).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:t ≤ fhp0:(configs cfg t).workTapePos 0 = ↑thp1:(configs cfg t).workTapePos 1 = ↑thm':(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hcount:mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1) ≤ width⊢ 0 ≤ (configs cfg t).workTapePos ((fun i ↦ i) ⟨0, ⋯⟩) ∧ (configs cfg t).workTapePos ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:t ≤ fhp0:(configs cfg t).workTapePos 0 = ↑thp1:(configs cfg t).workTapePos 1 = ↑thm':(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hcount:mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1) ≤ width⊢ 0 ≤ (configs cfg t).workTapePos 0 ∧ (configs cfg t).workTapePos 0 ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:t ≤ fhp0:(configs cfg t).workTapePos 0 = ↑thp1:(configs cfg t).workTapePos 1 = ↑thm':(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hcount:mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1) ≤ width⊢ 0 ≤ ↑t ∧ ↑t ≤ ↑width All goals completed! 🐙 input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:t ≤ fhp0:(configs cfg t).workTapePos 0 = ↑thp1:(configs cfg t).workTapePos 1 = ↑thm':(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hcount:mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1) ≤ width⊢ 0 ≤ (configs cfg t).workTapePos ((fun i ↦ i) ⟨1, ⋯⟩) ∧ (configs cfg t).workTapePos ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:t ≤ fhp0:(configs cfg t).workTapePos 0 = ↑thp1:(configs cfg t).workTapePos 1 = ↑thm':(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hcount:mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1) ≤ width⊢ 0 ≤ (configs cfg t).workTapePos 1 ∧ (configs cfg t).workTapePos 1 ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:t ≤ fhp0:(configs cfg t).workTapePos 0 = ↑thp1:(configs cfg t).workTapePos 1 = ↑thm':(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hcount:mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1) ≤ width⊢ 0 ≤ ↑t ∧ ↑t ≤ ↑width All goals completed! 🐙 input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:t ≤ fhp0:(configs cfg t).workTapePos 0 = ↑thp1:(configs cfg t).workTapePos 1 = ↑thm':(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hcount:mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1) ≤ width⊢ 0 ≤ (configs cfg t).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) ∧ (configs cfg t).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:t ≤ fhp0:(configs cfg t).workTapePos 0 = ↑thp1:(configs cfg t).workTapePos 1 = ↑thm':(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hcount:mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1) ≤ width⊢ 0 ≤ (configs cfg t).workTapePos 2 ∧ (configs cfg t).workTapePos 2 ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:t ≤ fhp0:(configs cfg t).workTapePos 0 = ↑thp1:(configs cfg t).workTapePos 1 = ↑thm':(configs cfg t).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1))hcount:mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1) ≤ width⊢ 0 ≤ ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1)) ∧ ↑(mismatchCount width (digits (configs cfg t) 0) (digits (configs cfg t) 1)) ≤ ↑width All goals completed! 🐙 input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:¬t ≤ f⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:¬t ≤ fafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg f⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:¬t ≤ fafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhq:(configs cfg (Counter.flips n.bits)).state = some stReturnhp0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hp1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)right✝:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPos ∧ (digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD false) ∧ digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) ∧ machine.outputString cfg (Counter.flips n.bits) = []⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:¬t ≤ fafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhq:(configs cfg (Counter.flips n.bits)).state = some stReturnhp0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hp1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)right✝:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPos ∧ (digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD false) ∧ digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) ∧ machine.outputString cfg (Counter.flips n.bits) = []horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)left✝:(configs cfg f).workTapes 2 = cfg.workTapes 2hm':(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:¬t ≤ fafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhq:(configs cfg (Counter.flips n.bits)).state = some stReturnhp0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hp1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)right✝:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPos ∧ (digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD false) ∧ digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) ∧ machine.outputString cfg (Counter.flips n.bits) = []horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)left✝:(configs cfg f).workTapes 2 = cfg.workTapes 2hm':(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))ho:∀ (z : ℤ), origin (after.workTapes 0 z) = decide (z = 0)⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:¬t ≤ fafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhq:(configs cfg (Counter.flips n.bits)).state = some stReturnhp0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hp1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)right✝:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPos ∧ (digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD false) ∧ digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) ∧ machine.outputString cfg (Counter.flips n.bits) = []horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)left✝:(configs cfg f).workTapes 2 = cfg.workTapes 2hm':(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))ho:∀ (z : ℤ), origin (after.workTapes 0 z) = decide (z = 0)he:returnCfg after f = after⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:¬t ≤ fafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhq:(configs cfg (Counter.flips n.bits)).state = some stReturnhp0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hp1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)right✝:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPos ∧ (digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD false) ∧ digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) ∧ machine.outputString cfg (Counter.flips n.bits) = []horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)left✝:(configs cfg f).workTapes 2 = cfg.workTapes 2hm':(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))ho:∀ (z : ℤ), origin (after.workTapes 0 z) = decide (z = 0)he:returnCfg after f = afterhcount:mismatchCount width (digits after 0) (digits after 1) ≤ width⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:¬t ≤ fafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhq:(configs cfg (Counter.flips n.bits)).state = some stReturnhp0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hp1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)right✝:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPos ∧ (digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD false) ∧ digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) ∧ machine.outputString cfg (Counter.flips n.bits) = []horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)left✝:(configs cfg f).workTapes 2 = cfg.workTapes 2hm':(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))ho:∀ (z : ℤ), origin (after.workTapes 0 z) = decide (z = 0)he:returnCfg after f = afterhcount:mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1) ≤ width⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:¬t ≤ fafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhq:(configs cfg (Counter.flips n.bits)).state = some stReturnhp0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hp1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)right✝:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPos ∧ (digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD false) ∧ digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) ∧ machine.outputString cfg (Counter.flips n.bits) = []horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)left✝:(configs cfg f).workTapes 2 = cfg.workTapes 2hm':(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))ho:∀ (z : ℤ), origin (after.workTapes 0 z) = decide (z = 0)he:returnCfg after f = afterhcount:mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1) ≤ widthhb:0 ≤ (configs (returnCfg after f) (t - f)).workTapePos i ∧ (configs (returnCfg after f) (t - f)).workTapePos i ≤ ↑width⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:¬t ≤ fafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhq:(configs cfg (Counter.flips n.bits)).state = some stReturnhp0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hp1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)right✝:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPos ∧ (digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD false) ∧ digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) ∧ machine.outputString cfg (Counter.flips n.bits) = []horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)left✝:(configs cfg f).workTapes 2 = cfg.workTapes 2hm':(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))ho:∀ (z : ℤ), origin (after.workTapes 0 z) = decide (z = 0)he:returnCfg after f = afterhcount:mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1) ≤ widthhb:0 ≤ (configs after (t - f)).workTapePos i ∧ (configs after (t - f)).workTapePos i ≤ ↑width⊢ 0 ≤ (configs cfg t).workTapePos i ∧ (configs cfg t).workTapePos i ≤ ↑width input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕa:ℕb:ℕh:Represents width cfg (if leaf = true then stCarryLeaf else stCarryFork) a bhnext:((if leaf = true then b else a) + 1).size ≤ widtht:ℕht:t ≤ 2 * Counter.flips (if leaf = true then b else a).bits + 1i:Fin 3n:ℕ := if leaf = true then b else af:ℕ := Counter.flips n.bitshw:f ≤ widthhbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = n.bits[j]?.getD falsehm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))htf:¬t ≤ fafter:Cfg 3 (Fin 4) (Fin 10) input := configs cfg fhq:(configs cfg (Counter.flips n.bits)).state = some stReturnhp0:(configs cfg (Counter.flips n.bits)).workTapePos 0 = ↑(Counter.flips n.bits)hp1:(configs cfg (Counter.flips n.bits)).workTapePos 1 = ↑(Counter.flips n.bits)right✝:(configs cfg (Counter.flips n.bits)).inputPos = cfg.inputPos ∧ (digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment n.bits)[j]?.getD false) ∧ digits (configs cfg (Counter.flips n.bits)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) ∧ machine.outputString cfg (Counter.flips n.bits) = []horigin:∀ (z : ℤ), origin ((configs cfg f).workTapes 0 z) = origin (cfg.workTapes 0 z)left✝:(configs cfg f).workTapes 2 = cfg.workTapes 2hm':(configs cfg f).workTapePos 2 = ↑(mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1))ho:∀ (z : ℤ), origin (after.workTapes 0 z) = decide (z = 0)he:returnCfg after f = afterhcount:mismatchCount width (digits (configs cfg f) 0) (digits (configs cfg f) 1) ≤ widthhb:0 ≤ (configs after (t - f)).workTapePos i ∧ (configs after (t - f)).workTapePos i ≤ ↑width⊢ 0 ≤ (configs (configs cfg f) (t - f)).workTapePos i ∧ (configs (configs cfg f) (t - f)).workTapePos i ≤ ↑width All goals completed! 🐙
end Geb.BitTree.BinaryMachine