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.Machine
public import Geb.Prototypes.Computability.BitTree.BinaryMachine.Difference
public import Geb.Prototypes.Computability.BitTree.Counter
public import Mathlib.Data.Nat.Bitwise

set_option doc.verso true

Representation invariants for binary counters

The representation relation records digit values, origin markers and the mismatch count. It permits either blank cells or explicit zero digits beyond the represented number. The fixed width bounds both binary counters throughout a complete execution.

Main definitions

bitsAt extends a natural number's digits by zero.
Represents describes configurations at scan boundaries.

Tags

Turing machine, binary representation, simulation

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

A natural number's little-endian bit sequence, extended by zero.

def bitsAt (n j : ℕ) : Bool := (n.bits[j]?).getD false

The zero-extended list representation agrees with bit testing.

theorem bitsAt_eq_testBit (n j : ℕ) : bitsAt n j = n.testBit j := byn:ℕj:ℕ⊢ bitsAt n j = n.testBit j
  rw [Nat.testBit_eq_inth,n:ℕj:ℕ⊢ bitsAt n j = n.bits.getI j List.getI_eq_getElem?_getDn:ℕj:ℕ⊢ bitsAt n j = n.bits[j]?.getD default]n:ℕj:ℕ⊢ bitsAt n j = n.bits[j]?.getD default
  rflAll goals completed! 🐙

Zero-extended binary representations determine their natural numbers.

theorem bitsAt_injective {a b : ℕ} (h : bitsAt a = bitsAt b) : a = b := bya:ℕb:ℕh:bitsAt a = bitsAt b⊢ a = b
  apply Nat.eq_of_testBit_eqa:ℕb:ℕh:bitsAt a = bitsAt b⊢ ∀ (i : ℕ), a.testBit i = b.testBit i
  intro ia:ℕb:ℕh:bitsAt a = bitsAt bi:ℕ⊢ a.testBit i = b.testBit i
  simpa only [bitsAt_eq_testBit] using congrFun h iAll goals completed! 🐙

All digits beyond the binary size are zero.

theorem bitsAt_of_size_le (n j : ℕ) (h : n.size ≤ j) : bitsAt n j = false := byn:ℕj:ℕh:n.size ≤ j⊢ bitsAt n j = false
  have hl : n.bits.length ≤ j := by rw [Counter.length_bitsn:ℕj:ℕh:n.size ≤ j⊢ n.size ≤ j]n:ℕj:ℕh:n.size ≤ j⊢ n.size ≤ j; exact hn:ℕj:ℕh:n.size ≤ jhl:n.bits.length ≤ j⊢ bitsAt n j = false
  simp only [bitsAt, List.getElem?_eq_none hl, Option.getD_none]All goals completed! 🐙

Scan-boundary configurations represent two bounded binary counters.

Finite control at the scan boundary.

The fork counter is read at its least significant digit.

The leaf counter is read at its least significant digit.

Digit representation of the fork counter.

Digit representation of the leaf counter.

Only the origin is tagged on the first binary tape.

The mismatch tape contains only its origin marker.

The third head counts unequal digit positions.

The fork counter fits within the fixed width.

The leaf counter fits within the fixed width.

              structure Represents {input : List (Fin 4)} (width : ℕ)
    (cfg : Cfg 3 (Fin 4) (Fin 10) input) (q : Fin 10) (a b : ℕ) : Prop where  state : cfg.state = some q  forkPos : cfg.workTapePos 0 = 0  leafPos : cfg.workTapePos 1 = 0  forkDigits : digits cfg 0 = bitsAt a  leafDigits : digits cfg 1 = bitsAt b  originTag : ∀ z, origin (cfg.workTapes 0 z) = decide (z = 0)  marker : ∀ z, cfg.workTapes 2 z = if z = 0 then some 0 else none  mismatchPos : cfg.workTapePos 2 = (mismatchCount width (bitsAt a) (bitsAt b) : ℤ)  forkSize : a.size ≤ width  leafSize : b.size ≤ width

The mismatch head is at the origin exactly when the two counters are equal.

theorem Represents.mismatchPos_eq_zero_iff {input : List (Fin 4)} {width a b : ℕ}
    {cfg : Cfg 3 (Fin 4) (Fin 10) input} {q : Fin 10}
    (h : Represents width cfg q a b) : cfg.workTapePos 2 = 0 ↔ a = b := byinput:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a b⊢ cfg.workTapePos 2 = 0 ↔ a = b
  have he := mismatchCount_eq_zero_iff_eq width (bitsAt a) (bitsAt b) (byinput:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a b⊢ ∀ (i : ℕ), width ≤ i → bitsAt a i = bitsAt b i
    intro j hjinput:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bj:ℕhj:width ≤ j⊢ bitsAt a j = bitsAt b j
    rw [bitsAt_of_size_le a j (Nat.le_trans h.forkSize hj),input:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bj:ℕhj:width ≤ j⊢ false = bitsAt b j
      bitsAt_of_size_le b j (Nat.le_trans h.leafSize hj)input:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bj:ℕhj:width ≤ j⊢ false = false]All goals completed! 🐙)input:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bhe:mismatchCount width (bitsAt a) (bitsAt b) = 0 ↔ bitsAt a = bitsAt b⊢ cfg.workTapePos 2 = 0 ↔ a = b
  constructormpinput:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bhe:mismatchCount width (bitsAt a) (bitsAt b) = 0 ↔ bitsAt a = bitsAt b⊢ cfg.workTapePos 2 = 0 → a = bmprinput:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bhe:mismatchCount width (bitsAt a) (bitsAt b) = 0 ↔ bitsAt a = bitsAt b⊢ a = b → cfg.workTapePos 2 = 0
  ·mpinput:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bhe:mismatchCount width (bitsAt a) (bitsAt b) = 0 ↔ bitsAt a = bitsAt b⊢ cfg.workTapePos 2 = 0 → a = b intro hzmpinput:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bhe:mismatchCount width (bitsAt a) (bitsAt b) = 0 ↔ bitsAt a = bitsAt bhz:cfg.workTapePos 2 = 0⊢ a = b
    have hc : mismatchCount width (bitsAt a) (bitsAt b) = 0 := byinput:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a b⊢ cfg.workTapePos 2 = 0 ↔ a = b
      have hp := h.mismatchPosinput:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bhe:mismatchCount width (bitsAt a) (bitsAt b) = 0 ↔ bitsAt a = bitsAt bhz:cfg.workTapePos 2 = 0hp:cfg.workTapePos 2 = ↑(mismatchCount width (bitsAt a) (bitsAt b))⊢ mismatchCount width (bitsAt a) (bitsAt b) = 0
      omegampinput:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bhe:mismatchCount width (bitsAt a) (bitsAt b) = 0 ↔ bitsAt a = bitsAt bhz:cfg.workTapePos 2 = 0hc:mismatchCount width (bitsAt a) (bitsAt b) = 0⊢ a = b
    exact bitsAt_injective (he.mp hc)All goals completed! 🐙
  ·mprinput:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bhe:mismatchCount width (bitsAt a) (bitsAt b) = 0 ↔ bitsAt a = bitsAt b⊢ a = b → cfg.workTapePos 2 = 0 intro habmprinput:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bhe:mismatchCount width (bitsAt a) (bitsAt b) = 0 ↔ bitsAt a = bitsAt bhab:a = b⊢ cfg.workTapePos 2 = 0
    have hc := he.mpr (congrArg bitsAt hab)mprinput:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bhe:mismatchCount width (bitsAt a) (bitsAt b) = 0 ↔ bitsAt a = bitsAt bhab:a = bhc:mismatchCount width (bitsAt a) (bitsAt b) = 0⊢ cfg.workTapePos 2 = 0
    rw [h.mismatchPos,mprinput:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bhe:mismatchCount width (bitsAt a) (bitsAt b) = 0 ↔ bitsAt a = bitsAt bhab:a = bhc:mismatchCount width (bitsAt a) (bitsAt b) = 0⊢ ↑(mismatchCount width (bitsAt a) (bitsAt b)) = 0 hcmprinput:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bhe:mismatchCount width (bitsAt a) (bitsAt b) = 0 ↔ bitsAt a = bitsAt bhab:a = bhc:mismatchCount width (bitsAt a) (bitsAt b) = 0⊢ ↑0 = 0]mprinput:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bhe:mismatchCount width (bitsAt a) (bitsAt b) = 0 ↔ bitsAt a = bitsAt bhab:a = bhc:mismatchCount width (bitsAt a) (bitsAt b) = 0⊢ ↑0 = 0
    rflAll goals completed! 🐙

The initial counters differ only at their least significant digit.

theorem mismatchCount_one_zero (width : ℕ) (hw : 1 ≤ width) :
    mismatchCount width (bitsAt 1) (bitsAt 0) = 1 := bywidth:ℕhw:1 ≤ width⊢ mismatchCount width (bitsAt 1) (bitsAt 0) = 1
  cases width with
  | zero =>zerohw:1 ≤ 0⊢ mismatchCount 0 (bitsAt 1) (bitsAt 0) = 1 omegaAll goals completed! 🐙
  | succ width =>succwidth:ℕhw:1 ≤ width + 1⊢ mismatchCount (width + 1) (bitsAt 1) (bitsAt 0) = 1
    apply Nat.rec (motive := fun k ↦ mismatchCount (k + 1) (bitsAt 1) (bitsAt 0) = 1)
      ?_ ?_ widthwidth:ℕhw:1 ≤ width + 1⊢ mismatchCount (Nat.zero + 1) (bitsAt 1) (bitsAt 0) = 1width:ℕhw:1 ≤ width + 1⊢ ∀ (n : ℕ), mismatchCount (n + 1) (bitsAt 1) (bitsAt 0) = 1 → mismatchCount (n.succ + 1) (bitsAt 1) (bitsAt 0) = 1
    ·width:ℕhw:1 ≤ width + 1⊢ mismatchCount (Nat.zero + 1) (bitsAt 1) (bitsAt 0) = 1 rflAll goals completed! 🐙
    ·width:ℕhw:1 ≤ width + 1⊢ ∀ (n : ℕ), mismatchCount (n + 1) (bitsAt 1) (bitsAt 0) = 1 → mismatchCount (n.succ + 1) (bitsAt 1) (bitsAt 0) = 1 intro k ihwidth:ℕhw:1 ≤ width + 1k:ℕih:mismatchCount (k + 1) (bitsAt 1) (bitsAt 0) = 1⊢ mismatchCount (k.succ + 1) (bitsAt 1) (bitsAt 0) = 1
      rw [mismatchCount_succ,width:ℕhw:1 ≤ width + 1k:ℕih:mismatchCount (k + 1) (bitsAt 1) (bitsAt 0) = 1⊢ (mismatchCount (k + 1) (bitsAt 1) (bitsAt 0) + if bitsAt 1 (k + 1) = bitsAt 0 (k + 1) then 0 else 1) = 1 ihwidth:ℕhw:1 ≤ width + 1k:ℕih:mismatchCount (k + 1) (bitsAt 1) (bitsAt 0) = 1⊢ (1 + if bitsAt 1 (k + 1) = bitsAt 0 (k + 1) then 0 else 1) = 1]width:ℕhw:1 ≤ width + 1k:ℕih:mismatchCount (k + 1) (bitsAt 1) (bitsAt 0) = 1⊢ (1 + if bitsAt 1 (k + 1) = bitsAt 0 (k + 1) then 0 else 1) = 1
      have h1 : bitsAt 1 (k + 1) = false := bitsAt_of_size_le 1 (k + 1) (bywidth:ℕhw:1 ≤ width + 1k:ℕih:mismatchCount (k + 1) (bitsAt 1) (bitsAt 0) = 1⊢ Nat.size 1 ≤ k + 1 change 1 ≤ k + 1width:ℕhw:1 ≤ width + 1k:ℕih:mismatchCount (k + 1) (bitsAt 1) (bitsAt 0) = 1⊢ 1 ≤ k + 1; omegaAll goals completed! 🐙)width:ℕhw:1 ≤ width + 1k:ℕih:mismatchCount (k + 1) (bitsAt 1) (bitsAt 0) = 1h1:bitsAt 1 (k + 1) = false⊢ (1 + if bitsAt 1 (k + 1) = bitsAt 0 (k + 1) then 0 else 1) = 1
      have h0 : bitsAt 0 (k + 1) = false := bitsAt_of_size_le 0 (k + 1) (Nat.zero_le _)width:ℕhw:1 ≤ width + 1k:ℕih:mismatchCount (k + 1) (bitsAt 1) (bitsAt 0) = 1h1:bitsAt 1 (k + 1) = falseh0:bitsAt 0 (k + 1) = false⊢ (1 + if bitsAt 1 (k + 1) = bitsAt 0 (k + 1) then 0 else 1) = 1
      rw [h1,width:ℕhw:1 ≤ width + 1k:ℕih:mismatchCount (k + 1) (bitsAt 1) (bitsAt 0) = 1h1:bitsAt 1 (k + 1) = falseh0:bitsAt 0 (k + 1) = false⊢ (1 + if false = bitsAt 0 (k + 1) then 0 else 1) = 1 h0width:ℕhw:1 ≤ width + 1k:ℕih:mismatchCount (k + 1) (bitsAt 1) (bitsAt 0) = 1h1:bitsAt 1 (k + 1) = falseh0:bitsAt 0 (k + 1) = false⊢ (1 + if false = false then 0 else 1) = 1]width:ℕhw:1 ≤ width + 1k:ℕih:mismatchCount (k + 1) (bitsAt 1) (bitsAt 0) = 1h1:bitsAt 1 (k + 1) = falseh0:bitsAt 0 (k + 1) = false⊢ (1 + if false = false then 0 else 1) = 1
      rflAll goals completed! 🐙

Initialization establishes the boundary representation with one pending root.

theorem represents_startCfg (input : List (Fin 4)) (width : ℕ) (hw : 1 ≤ width) :
    Represents width (startCfg input) stTree 1 0 := byinput:List (Fin 4)width:ℕhw:1 ≤ width⊢ Represents width (startCfg input) stTree 1 0
  refine ⟨rfl, rfl, rfl, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩refine_1input:List (Fin 4)width:ℕhw:1 ≤ width⊢ digits (startCfg input) 0 = bitsAt 1refine_2input:List (Fin 4)width:ℕhw:1 ≤ width⊢ digits (startCfg input) 1 = bitsAt 0refine_3input:List (Fin 4)width:ℕhw:1 ≤ width⊢ ∀ (z : ℤ), origin ((startCfg input).workTapes 0 z) = decide (z = 0)refine_4input:List (Fin 4)width:ℕhw:1 ≤ width⊢ ∀ (z : ℤ), (startCfg input).workTapes 2 z = if z = 0 then some 0 else nonerefine_5input:List (Fin 4)width:ℕhw:1 ≤ width⊢ (startCfg input).workTapePos 2 = ↑(mismatchCount width (bitsAt 1) (bitsAt 0))refine_6input:List (Fin 4)width:ℕhw:1 ≤ width⊢ Nat.size 1 ≤ widthrefine_7input:List (Fin 4)width:ℕhw:1 ≤ width⊢ Nat.size 0 ≤ width
  ·refine_1input:List (Fin 4)width:ℕhw:1 ≤ width⊢ digits (startCfg input) 0 = bitsAt 1 funext jrefine_1input:List (Fin 4)width:ℕhw:1 ≤ widthj:ℕ⊢ digits (startCfg input) 0 j = bitsAt 1 j
    change digit (if (j : ℤ) = 0 then some 3 else none) = ([true][j]?).getD falserefine_1input:List (Fin 4)width:ℕhw:1 ≤ widthj:ℕ⊢ digit (if ↑j = 0 then some 3 else none) = [true][j]?.getD false
    cases j with
    | zero =>refine_1.zeroinput:List (Fin 4)width:ℕhw:1 ≤ width⊢ digit (if ↑0 = 0 then some 3 else none) = [true][0]?.getD false rflAll goals completed! 🐙
    | succ j =>refine_1.succinput:List (Fin 4)width:ℕhw:1 ≤ widthj:ℕ⊢ digit (if ↑(j + 1) = 0 then some 3 else none) = [true][j + 1]?.getD false
      rw [ite_eq_right (byinput:List (Fin 4)width:ℕhw:1 ≤ widthj:ℕ⊢ ¬↑(j + 1) = 0 omegaAll goals completed! 🐙)]refine_1.succinput:List (Fin 4)width:ℕhw:1 ≤ widthj:ℕ⊢ digit none = [true][j + 1]?.getD false
      rflAll goals completed! 🐙
  ·refine_2input:List (Fin 4)width:ℕhw:1 ≤ width⊢ digits (startCfg input) 1 = bitsAt 0 funext jrefine_2input:List (Fin 4)width:ℕhw:1 ≤ widthj:ℕ⊢ digits (startCfg input) 1 j = bitsAt 0 j
    change digit (if (j : ℤ) = 0 then some 2 else none) = falserefine_2input:List (Fin 4)width:ℕhw:1 ≤ widthj:ℕ⊢ digit (if ↑j = 0 then some 2 else none) = false
    split_ifsposinput:List (Fin 4)width:ℕhw:1 ≤ widthj:ℕh✝:↑j = 0⊢ digit (some 2) = falseneginput:List (Fin 4)width:ℕhw:1 ≤ widthj:ℕh✝:¬↑j = 0⊢ digit none = false <;>posinput:List (Fin 4)width:ℕhw:1 ≤ widthj:ℕh✝:↑j = 0⊢ digit (some 2) = falseneginput:List (Fin 4)width:ℕhw:1 ≤ widthj:ℕh✝:¬↑j = 0⊢ digit none = false rflAll goals completed! 🐙
  ·refine_3input:List (Fin 4)width:ℕhw:1 ≤ width⊢ ∀ (z : ℤ), origin ((startCfg input).workTapes 0 z) = decide (z = 0) intro zrefine_3input:List (Fin 4)width:ℕhw:1 ≤ widthz:ℤ⊢ origin ((startCfg input).workTapes 0 z) = decide (z = 0)
    change origin (if z = 0 then some 3 else none) = decide (z = 0)refine_3input:List (Fin 4)width:ℕhw:1 ≤ widthz:ℤ⊢ origin (if z = 0 then some 3 else none) = decide (z = 0)
    split_ifs with hzposinput:List (Fin 4)width:ℕhw:1 ≤ widthz:ℤhz:z = 0⊢ origin (some 3) = decide (z = 0)neginput:List (Fin 4)width:ℕhw:1 ≤ widthz:ℤhz:¬z = 0⊢ origin none = decide (z = 0)
    ·posinput:List (Fin 4)width:ℕhw:1 ≤ widthz:ℤhz:z = 0⊢ origin (some 3) = decide (z = 0) rw [decide_eq_true hzposinput:List (Fin 4)width:ℕhw:1 ≤ widthz:ℤhz:z = 0⊢ origin (some 3) = true]posinput:List (Fin 4)width:ℕhw:1 ≤ widthz:ℤhz:z = 0⊢ origin (some 3) = true
      rflAll goals completed! 🐙
    ·neginput:List (Fin 4)width:ℕhw:1 ≤ widthz:ℤhz:¬z = 0⊢ origin none = decide (z = 0) rw [decide_eq_false hzneginput:List (Fin 4)width:ℕhw:1 ≤ widthz:ℤhz:¬z = 0⊢ origin none = false]neginput:List (Fin 4)width:ℕhw:1 ≤ widthz:ℤhz:¬z = 0⊢ origin none = false
      rflAll goals completed! 🐙
  ·refine_4input:List (Fin 4)width:ℕhw:1 ≤ width⊢ ∀ (z : ℤ), (startCfg input).workTapes 2 z = if z = 0 then some 0 else none intro zrefine_4input:List (Fin 4)width:ℕhw:1 ≤ widthz:ℤ⊢ (startCfg input).workTapes 2 z = if z = 0 then some 0 else none
    rflAll goals completed! 🐙
  ·refine_5input:List (Fin 4)width:ℕhw:1 ≤ width⊢ (startCfg input).workTapePos 2 = ↑(mismatchCount width (bitsAt 1) (bitsAt 0)) change (1 : ℤ) = (mismatchCount width (bitsAt 1) (bitsAt 0) : ℤ)refine_5input:List (Fin 4)width:ℕhw:1 ≤ width⊢ 1 = ↑(mismatchCount width (bitsAt 1) (bitsAt 0))
    rw [mismatchCount_one_zero width hwrefine_5input:List (Fin 4)width:ℕhw:1 ≤ width⊢ 1 = ↑1]refine_5input:List (Fin 4)width:ℕhw:1 ≤ width⊢ 1 = ↑1
    rflAll goals completed! 🐙
  ·refine_6input:List (Fin 4)width:ℕhw:1 ≤ width⊢ Nat.size 1 ≤ width exact hwAll goals completed! 🐙
  ·refine_7input:List (Fin 4)width:ℕhw:1 ≤ width⊢ Nat.size 0 ≤ width exact Nat.zero_le _All goals completed! 🐙

The representation invariant is preserved by a pure input transition.

theorem Represents.consume {input : List (Fin 4)} {width a b : ℕ}
    {cfg : Cfg 3 (Fin 4) (Fin 10) input} {q : Fin 10}
    (h : Represents width cfg q a b) (q' : Fin 10) :
    Represents width (consumeCfg cfg q') q' a b :=
  { h with state := rfl }

A scan-boundary representation bounds all three heads.

theorem Represents.headBound {input : List (Fin 4)} {width a b : ℕ}
    {cfg : Cfg 3 (Fin 4) (Fin 10) input} {q : Fin 10}
    (h : Represents width cfg q a b) : HeadBound width cfg := byinput:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a b⊢ HeadBound width cfg
  intro iinput:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bi:Fin 3⊢ 0 ≤ cfg.workTapePos i ∧ cfg.workTapePos i ≤ ↑width
  refine Fin.cases ?_ (Fin.cases ?_ (Fin.cases ?_ (fun j ↦ Fin.elim0 j))) irefine_1input:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bi:Fin 3⊢ 0 ≤ cfg.workTapePos 0 ∧ cfg.workTapePos 0 ≤ ↑widthrefine_2input:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bi:Fin 3⊢ 0 ≤ cfg.workTapePos (Fin.succ 0) ∧ cfg.workTapePos (Fin.succ 0) ≤ ↑widthrefine_3input:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bi:Fin 3⊢ 0 ≤ cfg.workTapePos (Fin.succ 0).succ ∧ cfg.workTapePos (Fin.succ 0).succ ≤ ↑width
  ·refine_1input:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bi:Fin 3⊢ 0 ≤ cfg.workTapePos 0 ∧ cfg.workTapePos 0 ≤ ↑width change 0 ≤ cfg.workTapePos 0 ∧ cfg.workTapePos 0 ≤ (width : ℤ)refine_1input:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bi:Fin 3⊢ 0 ≤ cfg.workTapePos 0 ∧ cfg.workTapePos 0 ≤ ↑width
    rw [h.forkPosrefine_1input:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bi:Fin 3⊢ 0 ≤ 0 ∧ 0 ≤ ↑width]refine_1input:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bi:Fin 3⊢ 0 ≤ 0 ∧ 0 ≤ ↑width
    exact ⟨Int.le_refl _, Int.natCast_nonneg _⟩All goals completed! 🐙
  ·refine_2input:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bi:Fin 3⊢ 0 ≤ cfg.workTapePos (Fin.succ 0) ∧ cfg.workTapePos (Fin.succ 0) ≤ ↑width change 0 ≤ cfg.workTapePos 1 ∧ cfg.workTapePos 1 ≤ (width : ℤ)refine_2input:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bi:Fin 3⊢ 0 ≤ cfg.workTapePos 1 ∧ cfg.workTapePos 1 ≤ ↑width
    rw [h.leafPosrefine_2input:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bi:Fin 3⊢ 0 ≤ 0 ∧ 0 ≤ ↑width]refine_2input:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bi:Fin 3⊢ 0 ≤ 0 ∧ 0 ≤ ↑width
    exact ⟨Int.le_refl _, Int.natCast_nonneg _⟩All goals completed! 🐙
  ·refine_3input:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bi:Fin 3⊢ 0 ≤ cfg.workTapePos (Fin.succ 0).succ ∧ cfg.workTapePos (Fin.succ 0).succ ≤ ↑width change 0 ≤ cfg.workTapePos 2 ∧ cfg.workTapePos 2 ≤ (width : ℤ)refine_3input:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bi:Fin 3⊢ 0 ≤ cfg.workTapePos 2 ∧ cfg.workTapePos 2 ≤ ↑width
    rw [h.mismatchPosrefine_3input:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bi:Fin 3⊢ 0 ≤ ↑(mismatchCount width (bitsAt a) (bitsAt b)) ∧ ↑(mismatchCount width (bitsAt a) (bitsAt b)) ≤ ↑width]refine_3input:List (Fin 4)width:ℕa:ℕb:ℕcfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:Represents width cfg q a bi:Fin 3⊢ 0 ≤ ↑(mismatchCount width (bitsAt a) (bitsAt b)) ∧ ↑(mismatchCount width (bitsAt a) (bitsAt b)) ≤ ↑width
    exact ⟨Int.natCast_nonneg _, Int.ofNat_le.mpr (mismatchCount_le width (bitsAt a) (bitsAt b))⟩All goals completed! 🐙

Returning reconstructs the boundary representation and tests counter equality.

theorem returnedCfg_represents {input : List (Fin 4)}
    (cfg : Cfg 3 (Fin 4) (Fin 10) input) (width a b : ℕ)
    (hd0 : digits cfg 0 = bitsAt a) (hd1 : digits cfg 1 = bitsAt b)
    (ho : ∀ z, origin (cfg.workTapes 0 z) = decide (z = 0))
    (hmark : ∀ z, cfg.workTapes 2 z = if z = 0 then some 0 else none)
    (hm : cfg.workTapePos 2 = (mismatchCount width (bitsAt a) (bitsAt b) : ℤ))
    (ha : a.size ≤ width) (hb : b.size ≤ width) :
    Represents width (returnedCfg cfg) (if a = b then stDone else stTree) a b := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕhd0:digits cfg 0 = bitsAt ahd1:digits cfg 1 = bitsAt bho:∀ (z : ℤ), origin (cfg.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), cfg.workTapes 2 z = if z = 0 then some 0 else nonehm:cfg.workTapePos 2 = ↑(mismatchCount width (bitsAt a) (bitsAt b))ha:a.size ≤ widthhb:b.size ≤ width⊢ Represents width (returnedCfg cfg) (if a = b then stDone else stTree) a b
  have hr : Represents width (returnedCfg cfg)
      (if cfg.workTapes 2 (cfg.workTapePos 2) == some 0 then stDone else stTree) a b :=
    ⟨rfl, rfl, rfl, hd0, hd1, ho, hmark, hm, ha, hb⟩input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕhd0:digits cfg 0 = bitsAt ahd1:digits cfg 1 = bitsAt bho:∀ (z : ℤ), origin (cfg.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), cfg.workTapes 2 z = if z = 0 then some 0 else nonehm:cfg.workTapePos 2 = ↑(mismatchCount width (bitsAt a) (bitsAt b))ha:a.size ≤ widthhb:b.size ≤ widthhr:Represents width (returnedCfg cfg) (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) a
  b⊢ Represents width (returnedCfg cfg) (if a = b then stDone else stTree) a b
  have he : cfg.workTapePos 2 = 0 ↔ a = b := hr.mismatchPos_eq_zero_iffinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕhd0:digits cfg 0 = bitsAt ahd1:digits cfg 1 = bitsAt bho:∀ (z : ℤ), origin (cfg.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), cfg.workTapes 2 z = if z = 0 then some 0 else nonehm:cfg.workTapePos 2 = ↑(mismatchCount width (bitsAt a) (bitsAt b))ha:a.size ≤ widthhb:b.size ≤ widthhr:Represents width (returnedCfg cfg) (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) a
  bhe:cfg.workTapePos 2 = 0 ↔ a = b⊢ Represents width (returnedCfg cfg) (if a = b then stDone else stTree) a b
  have hs : (if cfg.workTapes 2 (cfg.workTapePos 2) == some 0 then stDone else stTree) =
      (if a = b then stDone else stTree) := by
    by_cases hab : a = bposinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕhd0:digits cfg 0 = bitsAt ahd1:digits cfg 1 = bitsAt bho:∀ (z : ℤ), origin (cfg.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), cfg.workTapes 2 z = if z = 0 then some 0 else nonehm:cfg.workTapePos 2 = ↑(mismatchCount width (bitsAt a) (bitsAt b))ha:a.size ≤ widthhb:b.size ≤ widthhr:Represents width (returnedCfg cfg) (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) a
  bhe:cfg.workTapePos 2 = 0 ↔ a = bhab:a = b⊢ (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) = if a = b then stDone else stTreeneginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕhd0:digits cfg 0 = bitsAt ahd1:digits cfg 1 = bitsAt bho:∀ (z : ℤ), origin (cfg.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), cfg.workTapes 2 z = if z = 0 then some 0 else nonehm:cfg.workTapePos 2 = ↑(mismatchCount width (bitsAt a) (bitsAt b))ha:a.size ≤ widthhb:b.size ≤ widthhr:Represents width (returnedCfg cfg) (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) a
  bhe:cfg.workTapePos 2 = 0 ↔ a = bhab:¬a = b⊢ (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) = if a = b then stDone else stTree
    ·posinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕhd0:digits cfg 0 = bitsAt ahd1:digits cfg 1 = bitsAt bho:∀ (z : ℤ), origin (cfg.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), cfg.workTapes 2 z = if z = 0 then some 0 else nonehm:cfg.workTapePos 2 = ↑(mismatchCount width (bitsAt a) (bitsAt b))ha:a.size ≤ widthhb:b.size ≤ widthhr:Represents width (returnedCfg cfg) (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) a
  bhe:cfg.workTapePos 2 = 0 ↔ a = bhab:a = b⊢ (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) = if a = b then stDone else stTree have hp := he.mpr habposinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕhd0:digits cfg 0 = bitsAt ahd1:digits cfg 1 = bitsAt bho:∀ (z : ℤ), origin (cfg.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), cfg.workTapes 2 z = if z = 0 then some 0 else nonehm:cfg.workTapePos 2 = ↑(mismatchCount width (bitsAt a) (bitsAt b))ha:a.size ≤ widthhb:b.size ≤ widthhr:Represents width (returnedCfg cfg) (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) a
  bhe:cfg.workTapePos 2 = 0 ↔ a = bhab:a = bhp:cfg.workTapePos 2 = 0⊢ (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) = if a = b then stDone else stTree
      rw [hmark,posinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕhd0:digits cfg 0 = bitsAt ahd1:digits cfg 1 = bitsAt bho:∀ (z : ℤ), origin (cfg.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), cfg.workTapes 2 z = if z = 0 then some 0 else nonehm:cfg.workTapePos 2 = ↑(mismatchCount width (bitsAt a) (bitsAt b))ha:a.size ≤ widthhb:b.size ≤ widthhr:Represents width (returnedCfg cfg) (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) a
  bhe:cfg.workTapePos 2 = 0 ↔ a = bhab:a = bhp:cfg.workTapePos 2 = 0⊢ (if ((if cfg.workTapePos 2 = 0 then some 0 else none) == some 0) = true then stDone else stTree) =
  if a = b then stDone else stTree ite_eq_left hp,posinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕhd0:digits cfg 0 = bitsAt ahd1:digits cfg 1 = bitsAt bho:∀ (z : ℤ), origin (cfg.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), cfg.workTapes 2 z = if z = 0 then some 0 else nonehm:cfg.workTapePos 2 = ↑(mismatchCount width (bitsAt a) (bitsAt b))ha:a.size ≤ widthhb:b.size ≤ widthhr:Represents width (returnedCfg cfg) (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) a
  bhe:cfg.workTapePos 2 = 0 ↔ a = bhab:a = bhp:cfg.workTapePos 2 = 0⊢ (if (some 0 == some 0) = true then stDone else stTree) = if a = b then stDone else stTree ite_eq_left habposinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕhd0:digits cfg 0 = bitsAt ahd1:digits cfg 1 = bitsAt bho:∀ (z : ℤ), origin (cfg.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), cfg.workTapes 2 z = if z = 0 then some 0 else nonehm:cfg.workTapePos 2 = ↑(mismatchCount width (bitsAt a) (bitsAt b))ha:a.size ≤ widthhb:b.size ≤ widthhr:Represents width (returnedCfg cfg) (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) a
  bhe:cfg.workTapePos 2 = 0 ↔ a = bhab:a = bhp:cfg.workTapePos 2 = 0⊢ (if (some 0 == some 0) = true then stDone else stTree) = stDone]posinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕhd0:digits cfg 0 = bitsAt ahd1:digits cfg 1 = bitsAt bho:∀ (z : ℤ), origin (cfg.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), cfg.workTapes 2 z = if z = 0 then some 0 else nonehm:cfg.workTapePos 2 = ↑(mismatchCount width (bitsAt a) (bitsAt b))ha:a.size ≤ widthhb:b.size ≤ widthhr:Represents width (returnedCfg cfg) (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) a
  bhe:cfg.workTapePos 2 = 0 ↔ a = bhab:a = bhp:cfg.workTapePos 2 = 0⊢ (if (some 0 == some 0) = true then stDone else stTree) = stDone
      rflAll goals completed! 🐙
    ·neginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕhd0:digits cfg 0 = bitsAt ahd1:digits cfg 1 = bitsAt bho:∀ (z : ℤ), origin (cfg.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), cfg.workTapes 2 z = if z = 0 then some 0 else nonehm:cfg.workTapePos 2 = ↑(mismatchCount width (bitsAt a) (bitsAt b))ha:a.size ≤ widthhb:b.size ≤ widthhr:Represents width (returnedCfg cfg) (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) a
  bhe:cfg.workTapePos 2 = 0 ↔ a = bhab:¬a = b⊢ (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) = if a = b then stDone else stTree have hp : cfg.workTapePos 2 ≠ 0 := fun hh ↦ hab (he.mp hh)neginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕhd0:digits cfg 0 = bitsAt ahd1:digits cfg 1 = bitsAt bho:∀ (z : ℤ), origin (cfg.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), cfg.workTapes 2 z = if z = 0 then some 0 else nonehm:cfg.workTapePos 2 = ↑(mismatchCount width (bitsAt a) (bitsAt b))ha:a.size ≤ widthhb:b.size ≤ widthhr:Represents width (returnedCfg cfg) (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) a
  bhe:cfg.workTapePos 2 = 0 ↔ a = bhab:¬a = bhp:cfg.workTapePos 2 ≠ 0⊢ (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) = if a = b then stDone else stTree
      rw [hmark,neginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕhd0:digits cfg 0 = bitsAt ahd1:digits cfg 1 = bitsAt bho:∀ (z : ℤ), origin (cfg.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), cfg.workTapes 2 z = if z = 0 then some 0 else nonehm:cfg.workTapePos 2 = ↑(mismatchCount width (bitsAt a) (bitsAt b))ha:a.size ≤ widthhb:b.size ≤ widthhr:Represents width (returnedCfg cfg) (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) a
  bhe:cfg.workTapePos 2 = 0 ↔ a = bhab:¬a = bhp:cfg.workTapePos 2 ≠ 0⊢ (if ((if cfg.workTapePos 2 = 0 then some 0 else none) == some 0) = true then stDone else stTree) =
  if a = b then stDone else stTree ite_eq_right hp,neginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕhd0:digits cfg 0 = bitsAt ahd1:digits cfg 1 = bitsAt bho:∀ (z : ℤ), origin (cfg.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), cfg.workTapes 2 z = if z = 0 then some 0 else nonehm:cfg.workTapePos 2 = ↑(mismatchCount width (bitsAt a) (bitsAt b))ha:a.size ≤ widthhb:b.size ≤ widthhr:Represents width (returnedCfg cfg) (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) a
  bhe:cfg.workTapePos 2 = 0 ↔ a = bhab:¬a = bhp:cfg.workTapePos 2 ≠ 0⊢ (if (none == some 0) = true then stDone else stTree) = if a = b then stDone else stTree ite_eq_right habneginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕhd0:digits cfg 0 = bitsAt ahd1:digits cfg 1 = bitsAt bho:∀ (z : ℤ), origin (cfg.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), cfg.workTapes 2 z = if z = 0 then some 0 else nonehm:cfg.workTapePos 2 = ↑(mismatchCount width (bitsAt a) (bitsAt b))ha:a.size ≤ widthhb:b.size ≤ widthhr:Represents width (returnedCfg cfg) (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) a
  bhe:cfg.workTapePos 2 = 0 ↔ a = bhab:¬a = bhp:cfg.workTapePos 2 ≠ 0⊢ (if (none == some 0) = true then stDone else stTree) = stTree]neginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕhd0:digits cfg 0 = bitsAt ahd1:digits cfg 1 = bitsAt bho:∀ (z : ℤ), origin (cfg.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), cfg.workTapes 2 z = if z = 0 then some 0 else nonehm:cfg.workTapePos 2 = ↑(mismatchCount width (bitsAt a) (bitsAt b))ha:a.size ≤ widthhb:b.size ≤ widthhr:Represents width (returnedCfg cfg) (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) a
  bhe:cfg.workTapePos 2 = 0 ↔ a = bhab:¬a = bhp:cfg.workTapePos 2 ≠ 0⊢ (if (none == some 0) = true then stDone else stTree) = stTree
      rflinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕhd0:digits cfg 0 = bitsAt ahd1:digits cfg 1 = bitsAt bho:∀ (z : ℤ), origin (cfg.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), cfg.workTapes 2 z = if z = 0 then some 0 else nonehm:cfg.workTapePos 2 = ↑(mismatchCount width (bitsAt a) (bitsAt b))ha:a.size ≤ widthhb:b.size ≤ widthhr:Represents width (returnedCfg cfg) (if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) a
  bhe:cfg.workTapePos 2 = 0 ↔ a = bhs:(if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) = if a = b then stDone else stTree⊢ Represents width (returnedCfg cfg) (if a = b then stDone else stTree) a b
  rw [hsinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕhd0:digits cfg 0 = bitsAt ahd1:digits cfg 1 = bitsAt bho:∀ (z : ℤ), origin (cfg.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), cfg.workTapes 2 z = if z = 0 then some 0 else nonehm:cfg.workTapePos 2 = ↑(mismatchCount width (bitsAt a) (bitsAt b))ha:a.size ≤ widthhb:b.size ≤ widthhr:Represents width (returnedCfg cfg) (if a = b then stDone else stTree) a bhe:cfg.workTapePos 2 = 0 ↔ a = bhs:(if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) = if a = b then stDone else stTree⊢ Represents width (returnedCfg cfg) (if a = b then stDone else stTree) a b] at hrinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕa:ℕb:ℕhd0:digits cfg 0 = bitsAt ahd1:digits cfg 1 = bitsAt bho:∀ (z : ℤ), origin (cfg.workTapes 0 z) = decide (z = 0)hmark:∀ (z : ℤ), cfg.workTapes 2 z = if z = 0 then some 0 else nonehm:cfg.workTapePos 2 = ↑(mismatchCount width (bitsAt a) (bitsAt b))ha:a.size ≤ widthhb:b.size ≤ widthhr:Represents width (returnedCfg cfg) (if a = b then stDone else stTree) a bhe:cfg.workTapePos 2 = 0 ↔ a = bhs:(if (cfg.workTapes 2 (cfg.workTapePos 2) == some 0) = true then stDone else stTree) = if a = b then stDone else stTree⊢ Represents width (returnedCfg cfg) (if a = b then stDone else stTree) a b
  exact hrAll goals completed! 🐙

end Geb.BitTree.BinaryMachine