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 Cslib.Computability.Machines.Turing.MultiTape.Deterministic
public import Geb.Prototypes.Computability.BitTree.Scanner

set_option doc.verso true

A binary-counter machine for trees with bitstring leaves

The machine reads the input from left to right. Its first two work tapes hold the number of forks plus one and the number of completed leaves in binary. Their heads remain aligned. The third head records the number of unequal bit positions, so equality is detected at its marked origin without scanning the binary representations. Each carry changes this number by one at each bit flip.

Main definitions

machine is the three-work-tape machine.
digit reads a binary digit, including the tagged origin digits.
flipped flips a digit while preserving the origin tag.
modeState embeds scanner modes into finite machine control.
startCfg, consumeCfg and returnCfg describe phase boundaries.
HeadBound bounds all work-head positions.

Implementation notes

The alphabet has four symbols. Symbols zero and one are ordinary digits; symbols two and three tag the least significant position. A blank is read as zero. The third tape has one marker, at its origin. Input movement occurs only when consuming a bit; carry and return transitions leave the input head fixed.

Tags

Turing machine, binary counter, bitstring, tree

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

Embed input and output booleans into the machine alphabet.

def boolEmb : Bool ↪ Fin 4 where
  toFun b := if b then 1 else 0
  inj' a b := bya:Boolb:Bool⊢ (fun b ↦ if b = true then 1 else 0) a = (fun b ↦ if b = true then 1 else 0) b → a = b cases afalseb:Bool⊢ (fun b ↦ if b = true then 1 else 0) false = (fun b ↦ if b = true then 1 else 0) b → false = btrueb:Bool⊢ (fun b ↦ if b = true then 1 else 0) true = (fun b ↦ if b = true then 1 else 0) b → true = b <;>falseb:Bool⊢ (fun b ↦ if b = true then 1 else 0) false = (fun b ↦ if b = true then 1 else 0) b → false = btrueb:Bool⊢ (fun b ↦ if b = true then 1 else 0) true = (fun b ↦ if b = true then 1 else 0) b → true = b cases btrue.false⊢ (fun b ↦ if b = true then 1 else 0) true = (fun b ↦ if b = true then 1 else 0) false → true = falsetrue.true⊢ (fun b ↦ if b = true then 1 else 0) true = (fun b ↦ if b = true then 1 else 0) true → true = true <;>false.false⊢ (fun b ↦ if b = true then 1 else 0) false = (fun b ↦ if b = true then 1 else 0) false → false = falsefalse.true⊢ (fun b ↦ if b = true then 1 else 0) false = (fun b ↦ if b = true then 1 else 0) true → false = truetrue.false⊢ (fun b ↦ if b = true then 1 else 0) true = (fun b ↦ if b = true then 1 else 0) false → true = falsetrue.true⊢ (fun b ↦ if b = true then 1 else 0) true = (fun b ↦ if b = true then 1 else 0) true → true = true simpAll goals completed! 🐙

Read a digit, with a blank representing zero.

def digit (s : Option (Fin 4)) : Bool := s == some 1 || s == some 3

Detect a tagged least significant digit.

def origin (s : Option (Fin 4)) : Bool := s == some 2 || s == some 3

Flip one digit, preserving its origin tag.

def flipped (s : Option (Fin 4)) : Fin 4 :=
  if origin s then (if digit s then 2 else 3) else (if digit s then 0 else 1)

Reading a flipped digit gives the boolean complement.

theorem digit_flipped (s : Option (Fin 4)) : digit (some (flipped s)) = !digit s := bys:Option (Fin 4)⊢ digit (some (flipped s)) = !digit s
  unfold flippeds:Option (Fin 4)⊢ digit (some (if origin s = true then if digit s = true then 2 else 3 else if digit s = true then 0 else 1)) = !digit s
  cases origin sfalses:Option (Fin 4)⊢ digit (some (if false = true then if digit s = true then 2 else 3 else if digit s = true then 0 else 1)) = !digit strues:Option (Fin 4)⊢ digit (some (if true = true then if digit s = true then 2 else 3 else if digit s = true then 0 else 1)) = !digit s <;>falses:Option (Fin 4)⊢ digit (some (if false = true then if digit s = true then 2 else 3 else if digit s = true then 0 else 1)) = !digit strues:Option (Fin 4)⊢ digit (some (if true = true then if digit s = true then 2 else 3 else if digit s = true then 0 else 1)) = !digit s cases digit strue.falses:Option (Fin 4)⊢ digit (some (if true = true then if false = true then 2 else 3 else if false = true then 0 else 1)) = !falsetrue.trues:Option (Fin 4)⊢ digit (some (if true = true then if true = true then 2 else 3 else if true = true then 0 else 1)) = !true <;>false.falses:Option (Fin 4)⊢ digit (some (if false = true then if false = true then 2 else 3 else if false = true then 0 else 1)) = !falsefalse.trues:Option (Fin 4)⊢ digit (some (if false = true then if true = true then 2 else 3 else if true = true then 0 else 1)) = !truetrue.falses:Option (Fin 4)⊢ digit (some (if true = true then if false = true then 2 else 3 else if false = true then 0 else 1)) = !falsetrue.trues:Option (Fin 4)⊢ digit (some (if true = true then if true = true then 2 else 3 else if true = true then 0 else 1)) = !true rflAll goals completed! 🐙

Flipping a digit preserves its origin tag.

theorem origin_flipped (s : Option (Fin 4)) : origin (some (flipped s)) = origin s := bys:Option (Fin 4)⊢ origin (some (flipped s)) = origin s
  unfold flippeds:Option (Fin 4)⊢ origin (some (if origin s = true then if digit s = true then 2 else 3 else if digit s = true then 0 else 1)) = origin s
  cases origin sfalses:Option (Fin 4)⊢ origin (some (if false = true then if digit s = true then 2 else 3 else if digit s = true then 0 else 1)) = falsetrues:Option (Fin 4)⊢ origin (some (if true = true then if digit s = true then 2 else 3 else if digit s = true then 0 else 1)) = true <;>falses:Option (Fin 4)⊢ origin (some (if false = true then if digit s = true then 2 else 3 else if digit s = true then 0 else 1)) = falsetrues:Option (Fin 4)⊢ origin (some (if true = true then if digit s = true then 2 else 3 else if digit s = true then 0 else 1)) = true cases digit strue.falses:Option (Fin 4)⊢ origin (some (if true = true then if false = true then 2 else 3 else if false = true then 0 else 1)) = truetrue.trues:Option (Fin 4)⊢ origin (some (if true = true then if true = true then 2 else 3 else if true = true then 0 else 1)) = true <;>false.falses:Option (Fin 4)⊢ origin (some (if false = true then if false = true then 2 else 3 else if false = true then 0 else 1)) = falsefalse.trues:Option (Fin 4)⊢ origin (some (if false = true then if true = true then 2 else 3 else if true = true then 0 else 1)) = falsetrue.falses:Option (Fin 4)⊢ origin (some (if true = true then if false = true then 2 else 3 else if false = true then 0 else 1)) = truetrue.trues:Option (Fin 4)⊢ origin (some (if true = true then if true = true then 2 else 3 else if true = true then 0 else 1)) = true rflAll goals completed! 🐙

The mismatch count rises when two equal digits become different.

def mismatchMove (a b : Option (Fin 4)) : SignType :=
  if digit a == digit b then 1 else -1

Write both origin digits and the mismatch tape's origin marker.

def stInit : Fin 10 := 0

Enter scanning after initialization.

def stStart : Fin 10 := 1

Expect a tree constructor.

def stTree : Fin 10 := 2

Expect a string continuation or terminator.

def stString : Fin 10 := 3

Consume one payload bit.

def stBit : Fin 10 := 4

The complete tree has ended; only end of input is accepted.

def stDone : Fin 10 := 5

A malformed prefix has been found.

def stDead : Fin 10 := 6

Increment the number of forks plus one.

def stCarryFork : Fin 10 := 7

Increment the number of completed leaves.

def stCarryLeaf : Fin 10 := 8

Return both binary heads to their origins.

def stReturn : Fin 10 := 9

A transition consuming one input symbol without changing work tapes.

def consume (q : Fin 10) : TransitionOut 3 (Fin 4) (Fin 10) where
  inputMove := 1
  workActions _ := (none, 0)
  outS := none
  q' := some q

Emit one boolean and halt.

def finish (b : Bool) : TransitionOut 3 (Fin 4) (Fin 10) where
  inputMove := 0
  workActions _ := (none, 0)
  outS := some (boolEmb b)
  q' := none

Flip the selected counter's current bit and maintain the mismatch count. Carry transitions move both binary heads right; the first zero ends the carry.

def carry (leaf : Bool) (work : Fin 3 → Option (Fin 4)) :
    TransitionOut 3 (Fin 4) (Fin 10) :=
  let selected : Fin 3 := if leaf then 1 else 0
  { inputMove := 0
    workActions := fun i ↦
      if i = 2 then (none, mismatchMove (work 0) (work 1))
      else (if i = selected then some (some (flipped (work i))) else none, 1)
    outS := none
    q' := some (if digit (work selected) then
      (if leaf then stCarryLeaf else stCarryFork) else stReturn) }

A three-work-tape recognizer whose counters are incremented monotonically.

def machine : MultiTapeTM 3 (Fin 4) (Fin 10) where
  q₀ := stInit
  tr q input work :=
    if q = stInit then
      { inputMove := 0
        workActions := fun i ↦
          if i = 0 then (some (some 3), 0)
          else if i = 1 then (some (some 2), 0)
          else (some (some 0), 1)
        outS := none
        q' := some stStart }
    else if q = stStart then
      { inputMove := 0, workActions := fun _ ↦ (none, 0),
        outS := none, q' := some stTree }
    else if q = stCarryFork then carry false work
    else if q = stCarryLeaf then carry true work
    else if q = stReturn then
      if origin (work 0) then
        { inputMove := 0, workActions := fun _ ↦ (none, 0), outS := none,
          q' := some (if work 2 == some 0 then stDone else stTree) }
      else
        { inputMove := 0,
          workActions := fun i ↦ (none, if i = 2 then 0 else -1),
          outS := none, q' := some stReturn }
    else
      match input with
      | none => finish (q == stDone)
      | some b =>
        if q = stTree then consume (if b == 0 then stString else stCarryFork)
        else if q = stString then consume (if b == 0 then stCarryLeaf else stBit)
        else if q = stBit then consume stString
        else consume stDead

Every input transition is stationary or moves right.

theorem inputMove_ne_neg (q : Fin 10) (input : Option (Fin 4))
    (work : Fin 3 → Option (Fin 4)) : (machine.tr q input work).inputMove ≠ -1 := byq:Fin 10input:Option (Fin 4)work:Fin 3 → Option (Fin 4)⊢ (machine.tr q input work).inputMove ≠ -1
  cases inputnoneq:Fin 10work:Fin 3 → Option (Fin 4)⊢ (machine.tr q none work).inputMove ≠ -1someq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4⊢ (machine.tr q (some val✝) work).inputMove ≠ -1 <;>noneq:Fin 10work:Fin 3 → Option (Fin 4)⊢ (machine.tr q none work).inputMove ≠ -1someq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4⊢ (machine.tr q (some val✝) work).inputMove ≠ -1 simp only [machine]someq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4⊢ (if q = stInit then
      { inputMove := 0,
        workActions := fun i ↦
          if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1),
        outS := none, q' := some stStart }
    else
      if q = stStart then { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }
      else
        if q = stCarryFork then carry false work
        else
          if q = stCarryLeaf then carry true work
          else
            if q = stReturn then
              if origin (work 0) = true then
                { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none,
                  q' := some (if (work 2 == some 0) = true then stDone else stTree) }
              else
                { inputMove := 0, workActions := fun i ↦ (none, if i = 2 then 0 else -1), outS := none,
                  q' := some stReturn }
            else
              if q = stTree then consume (if (val✝ == 0) = true then stString else stCarryFork)
              else
                if q = stString then consume (if (val✝ == 0) = true then stCarryLeaf else stBit)
                else if q = stBit then consume stString else consume stDead).inputMove ≠
  -1 <;>noneq:Fin 10work:Fin 3 → Option (Fin 4)⊢ (if q = stInit then
      { inputMove := 0,
        workActions := fun i ↦
          if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1),
        outS := none, q' := some stStart }
    else
      if q = stStart then { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }
      else
        if q = stCarryFork then carry false work
        else
          if q = stCarryLeaf then carry true work
          else
            if q = stReturn then
              if origin (work 0) = true then
                { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none,
                  q' := some (if (work 2 == some 0) = true then stDone else stTree) }
              else
                { inputMove := 0, workActions := fun i ↦ (none, if i = 2 then 0 else -1), outS := none,
                  q' := some stReturn }
            else finish (q == stDone)).inputMove ≠
  -1someq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4⊢ (if q = stInit then
      { inputMove := 0,
        workActions := fun i ↦
          if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1),
        outS := none, q' := some stStart }
    else
      if q = stStart then { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }
      else
        if q = stCarryFork then carry false work
        else
          if q = stCarryLeaf then carry true work
          else
            if q = stReturn then
              if origin (work 0) = true then
                { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none,
                  q' := some (if (work 2 == some 0) = true then stDone else stTree) }
              else
                { inputMove := 0, workActions := fun i ↦ (none, if i = 2 then 0 else -1), outS := none,
                  q' := some stReturn }
            else
              if q = stTree then consume (if (val✝ == 0) = true then stString else stCarryFork)
              else
                if q = stString then consume (if (val✝ == 0) = true then stCarryLeaf else stBit)
                else if q = stBit then consume stString else consume stDead).inputMove ≠
  -1 split_ifsposq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝:q = stInit⊢ { inputMove := 0,
      workActions := fun i ↦
        if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1),
      outS := none, q' := some stStart }.inputMove ≠
  -1posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝¹:¬q = stInith✝:q = stStart⊢ { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }.inputMove ≠ -1posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝²:¬q = stInith✝¹:¬q = stStarth✝:q = stCarryFork⊢ (carry false work).inputMove ≠ -1posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝³:¬q = stInith✝²:¬q = stStarth✝¹:¬q = stCarryForkh✝:q = stCarryLeaf⊢ (carry true work).inputMove ≠ -1posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁶:¬q = stInith✝⁵:¬q = stStarth✝⁴:¬q = stCarryForkh✝³:¬q = stCarryLeafh✝²:q = stReturnh✝¹:origin (work 0) = trueh✝:(work 2 == some 0) = true⊢ { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stDone }.inputMove ≠ -1negq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁶:¬q = stInith✝⁵:¬q = stStarth✝⁴:¬q = stCarryForkh✝³:¬q = stCarryLeafh✝²:q = stReturnh✝¹:origin (work 0) = trueh✝:¬(work 2 == some 0) = true⊢ { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }.inputMove ≠ -1negq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁵:¬q = stInith✝⁴:¬q = stStarth✝³:¬q = stCarryForkh✝²:¬q = stCarryLeafh✝¹:q = stReturnh✝:¬origin (work 0) = true⊢ { inputMove := 0, workActions := fun i ↦ (none, if i = 2 then 0 else -1), outS := none,
      q' := some stReturn }.inputMove ≠
  -1posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁶:¬q = stInith✝⁵:¬q = stStarth✝⁴:¬q = stCarryForkh✝³:¬q = stCarryLeafh✝²:¬q = stReturnh✝¹:q = stTreeh✝:(val✝ == 0) = true⊢ (consume stString).inputMove ≠ -1negq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁶:¬q = stInith✝⁵:¬q = stStarth✝⁴:¬q = stCarryForkh✝³:¬q = stCarryLeafh✝²:¬q = stReturnh✝¹:q = stTreeh✝:¬(val✝ == 0) = true⊢ (consume stCarryFork).inputMove ≠ -1posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁷:¬q = stInith✝⁶:¬q = stStarth✝⁵:¬q = stCarryForkh✝⁴:¬q = stCarryLeafh✝³:¬q = stReturnh✝²:¬q = stTreeh✝¹:q = stStringh✝:(val✝ == 0) = true⊢ (consume stCarryLeaf).inputMove ≠ -1negq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁷:¬q = stInith✝⁶:¬q = stStarth✝⁵:¬q = stCarryForkh✝⁴:¬q = stCarryLeafh✝³:¬q = stReturnh✝²:¬q = stTreeh✝¹:q = stStringh✝:¬(val✝ == 0) = true⊢ (consume stBit).inputMove ≠ -1posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁷:¬q = stInith✝⁶:¬q = stStarth✝⁵:¬q = stCarryForkh✝⁴:¬q = stCarryLeafh✝³:¬q = stReturnh✝²:¬q = stTreeh✝¹:¬q = stStringh✝:q = stBit⊢ (consume stString).inputMove ≠ -1negq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁷:¬q = stInith✝⁶:¬q = stStarth✝⁵:¬q = stCarryForkh✝⁴:¬q = stCarryLeafh✝³:¬q = stReturnh✝²:¬q = stTreeh✝¹:¬q = stStringh✝:¬q = stBit⊢ (consume stDead).inputMove ≠ -1 <;>posq:Fin 10work:Fin 3 → Option (Fin 4)h✝:q = stInit⊢ { inputMove := 0,
      workActions := fun i ↦
        if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1),
      outS := none, q' := some stStart }.inputMove ≠
  -1posq:Fin 10work:Fin 3 → Option (Fin 4)h✝¹:¬q = stInith✝:q = stStart⊢ { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }.inputMove ≠ -1posq:Fin 10work:Fin 3 → Option (Fin 4)h✝²:¬q = stInith✝¹:¬q = stStarth✝:q = stCarryFork⊢ (carry false work).inputMove ≠ -1posq:Fin 10work:Fin 3 → Option (Fin 4)h✝³:¬q = stInith✝²:¬q = stStarth✝¹:¬q = stCarryForkh✝:q = stCarryLeaf⊢ (carry true work).inputMove ≠ -1posq:Fin 10work:Fin 3 → Option (Fin 4)h✝⁶:¬q = stInith✝⁵:¬q = stStarth✝⁴:¬q = stCarryForkh✝³:¬q = stCarryLeafh✝²:q = stReturnh✝¹:origin (work 0) = trueh✝:(work 2 == some 0) = true⊢ { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stDone }.inputMove ≠ -1negq:Fin 10work:Fin 3 → Option (Fin 4)h✝⁶:¬q = stInith✝⁵:¬q = stStarth✝⁴:¬q = stCarryForkh✝³:¬q = stCarryLeafh✝²:q = stReturnh✝¹:origin (work 0) = trueh✝:¬(work 2 == some 0) = true⊢ { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }.inputMove ≠ -1negq:Fin 10work:Fin 3 → Option (Fin 4)h✝⁵:¬q = stInith✝⁴:¬q = stStarth✝³:¬q = stCarryForkh✝²:¬q = stCarryLeafh✝¹:q = stReturnh✝:¬origin (work 0) = true⊢ { inputMove := 0, workActions := fun i ↦ (none, if i = 2 then 0 else -1), outS := none,
      q' := some stReturn }.inputMove ≠
  -1negq:Fin 10work:Fin 3 → Option (Fin 4)h✝⁴:¬q = stInith✝³:¬q = stStarth✝²:¬q = stCarryForkh✝¹:¬q = stCarryLeafh✝:¬q = stReturn⊢ (finish (q == stDone)).inputMove ≠ -1posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝:q = stInit⊢ { inputMove := 0,
      workActions := fun i ↦
        if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1),
      outS := none, q' := some stStart }.inputMove ≠
  -1posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝¹:¬q = stInith✝:q = stStart⊢ { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }.inputMove ≠ -1posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝²:¬q = stInith✝¹:¬q = stStarth✝:q = stCarryFork⊢ (carry false work).inputMove ≠ -1posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝³:¬q = stInith✝²:¬q = stStarth✝¹:¬q = stCarryForkh✝:q = stCarryLeaf⊢ (carry true work).inputMove ≠ -1posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁶:¬q = stInith✝⁵:¬q = stStarth✝⁴:¬q = stCarryForkh✝³:¬q = stCarryLeafh✝²:q = stReturnh✝¹:origin (work 0) = trueh✝:(work 2 == some 0) = true⊢ { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stDone }.inputMove ≠ -1negq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁶:¬q = stInith✝⁵:¬q = stStarth✝⁴:¬q = stCarryForkh✝³:¬q = stCarryLeafh✝²:q = stReturnh✝¹:origin (work 0) = trueh✝:¬(work 2 == some 0) = true⊢ { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }.inputMove ≠ -1negq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁵:¬q = stInith✝⁴:¬q = stStarth✝³:¬q = stCarryForkh✝²:¬q = stCarryLeafh✝¹:q = stReturnh✝:¬origin (work 0) = true⊢ { inputMove := 0, workActions := fun i ↦ (none, if i = 2 then 0 else -1), outS := none,
      q' := some stReturn }.inputMove ≠
  -1posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁶:¬q = stInith✝⁵:¬q = stStarth✝⁴:¬q = stCarryForkh✝³:¬q = stCarryLeafh✝²:¬q = stReturnh✝¹:q = stTreeh✝:(val✝ == 0) = true⊢ (consume stString).inputMove ≠ -1negq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁶:¬q = stInith✝⁵:¬q = stStarth✝⁴:¬q = stCarryForkh✝³:¬q = stCarryLeafh✝²:¬q = stReturnh✝¹:q = stTreeh✝:¬(val✝ == 0) = true⊢ (consume stCarryFork).inputMove ≠ -1posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁷:¬q = stInith✝⁶:¬q = stStarth✝⁵:¬q = stCarryForkh✝⁴:¬q = stCarryLeafh✝³:¬q = stReturnh✝²:¬q = stTreeh✝¹:q = stStringh✝:(val✝ == 0) = true⊢ (consume stCarryLeaf).inputMove ≠ -1negq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁷:¬q = stInith✝⁶:¬q = stStarth✝⁵:¬q = stCarryForkh✝⁴:¬q = stCarryLeafh✝³:¬q = stReturnh✝²:¬q = stTreeh✝¹:q = stStringh✝:¬(val✝ == 0) = true⊢ (consume stBit).inputMove ≠ -1posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁷:¬q = stInith✝⁶:¬q = stStarth✝⁵:¬q = stCarryForkh✝⁴:¬q = stCarryLeafh✝³:¬q = stReturnh✝²:¬q = stTreeh✝¹:¬q = stStringh✝:q = stBit⊢ (consume stString).inputMove ≠ -1negq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁷:¬q = stInith✝⁶:¬q = stStarth✝⁵:¬q = stCarryForkh✝⁴:¬q = stCarryLeafh✝³:¬q = stReturnh✝²:¬q = stTreeh✝¹:¬q = stStringh✝:¬q = stBit⊢ (consume stDead).inputMove ≠ -1 first
    | exact (byq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁷:¬q = stInith✝⁶:¬q = stStarth✝⁵:¬q = stCarryForkh✝⁴:¬q = stCarryLeafh✝³:¬q = stReturnh✝²:¬q = stTreeh✝¹:¬q = stStringh✝:¬q = stBit⊢ 0 ≠ -1 decideAll goals completed! 🐙 : (0 : SignType) ≠ -1)
    | exact (byq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁷:¬q = stInith✝⁶:¬q = stStarth✝⁵:¬q = stCarryForkh✝⁴:¬q = stCarryLeafh✝³:¬q = stReturnh✝²:¬q = stTreeh✝¹:¬q = stStringh✝:¬q = stBit⊢ 1 ≠ -1 decideAll goals completed! 🐙 : (1 : SignType) ≠ -1)

All transitions move the two binary heads by the same displacement.

theorem binaryHeads_move_eq (q : Fin 10) (input : Option (Fin 4))
    (work : Fin 3 → Option (Fin 4)) :
    ((machine.tr q input work).workActions 0).2 =
      ((machine.tr q input work).workActions 1).2 := byq:Fin 10input:Option (Fin 4)work:Fin 3 → Option (Fin 4)⊢ ((machine.tr q input work).workActions 0).2 = ((machine.tr q input work).workActions 1).2
  cases inputnoneq:Fin 10work:Fin 3 → Option (Fin 4)⊢ ((machine.tr q none work).workActions 0).2 = ((machine.tr q none work).workActions 1).2someq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4⊢ ((machine.tr q (some val✝) work).workActions 0).2 = ((machine.tr q (some val✝) work).workActions 1).2 <;>noneq:Fin 10work:Fin 3 → Option (Fin 4)⊢ ((machine.tr q none work).workActions 0).2 = ((machine.tr q none work).workActions 1).2someq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4⊢ ((machine.tr q (some val✝) work).workActions 0).2 = ((machine.tr q (some val✝) work).workActions 1).2 simp only [machine]someq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4⊢ ((if q = stInit then
          { inputMove := 0,
            workActions := fun i ↦
              if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1),
            outS := none, q' := some stStart }
        else
          if q = stStart then { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }
          else
            if q = stCarryFork then carry false work
            else
              if q = stCarryLeaf then carry true work
              else
                if q = stReturn then
                  if origin (work 0) = true then
                    { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none,
                      q' := some (if (work 2 == some 0) = true then stDone else stTree) }
                  else
                    { inputMove := 0, workActions := fun i ↦ (none, if i = 2 then 0 else -1), outS := none,
                      q' := some stReturn }
                else
                  if q = stTree then consume (if (val✝ == 0) = true then stString else stCarryFork)
                  else
                    if q = stString then consume (if (val✝ == 0) = true then stCarryLeaf else stBit)
                    else if q = stBit then consume stString else consume stDead).workActions
      0).2 =
  ((if q = stInit then
          { inputMove := 0,
            workActions := fun i ↦
              if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1),
            outS := none, q' := some stStart }
        else
          if q = stStart then { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }
          else
            if q = stCarryFork then carry false work
            else
              if q = stCarryLeaf then carry true work
              else
                if q = stReturn then
                  if origin (work 0) = true then
                    { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none,
                      q' := some (if (work 2 == some 0) = true then stDone else stTree) }
                  else
                    { inputMove := 0, workActions := fun i ↦ (none, if i = 2 then 0 else -1), outS := none,
                      q' := some stReturn }
                else
                  if q = stTree then consume (if (val✝ == 0) = true then stString else stCarryFork)
                  else
                    if q = stString then consume (if (val✝ == 0) = true then stCarryLeaf else stBit)
                    else if q = stBit then consume stString else consume stDead).workActions
      1).2 <;>noneq:Fin 10work:Fin 3 → Option (Fin 4)⊢ ((if q = stInit then
          { inputMove := 0,
            workActions := fun i ↦
              if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1),
            outS := none, q' := some stStart }
        else
          if q = stStart then { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }
          else
            if q = stCarryFork then carry false work
            else
              if q = stCarryLeaf then carry true work
              else
                if q = stReturn then
                  if origin (work 0) = true then
                    { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none,
                      q' := some (if (work 2 == some 0) = true then stDone else stTree) }
                  else
                    { inputMove := 0, workActions := fun i ↦ (none, if i = 2 then 0 else -1), outS := none,
                      q' := some stReturn }
                else finish (q == stDone)).workActions
      0).2 =
  ((if q = stInit then
          { inputMove := 0,
            workActions := fun i ↦
              if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1),
            outS := none, q' := some stStart }
        else
          if q = stStart then { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }
          else
            if q = stCarryFork then carry false work
            else
              if q = stCarryLeaf then carry true work
              else
                if q = stReturn then
                  if origin (work 0) = true then
                    { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none,
                      q' := some (if (work 2 == some 0) = true then stDone else stTree) }
                  else
                    { inputMove := 0, workActions := fun i ↦ (none, if i = 2 then 0 else -1), outS := none,
                      q' := some stReturn }
                else finish (q == stDone)).workActions
      1).2someq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4⊢ ((if q = stInit then
          { inputMove := 0,
            workActions := fun i ↦
              if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1),
            outS := none, q' := some stStart }
        else
          if q = stStart then { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }
          else
            if q = stCarryFork then carry false work
            else
              if q = stCarryLeaf then carry true work
              else
                if q = stReturn then
                  if origin (work 0) = true then
                    { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none,
                      q' := some (if (work 2 == some 0) = true then stDone else stTree) }
                  else
                    { inputMove := 0, workActions := fun i ↦ (none, if i = 2 then 0 else -1), outS := none,
                      q' := some stReturn }
                else
                  if q = stTree then consume (if (val✝ == 0) = true then stString else stCarryFork)
                  else
                    if q = stString then consume (if (val✝ == 0) = true then stCarryLeaf else stBit)
                    else if q = stBit then consume stString else consume stDead).workActions
      0).2 =
  ((if q = stInit then
          { inputMove := 0,
            workActions := fun i ↦
              if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1),
            outS := none, q' := some stStart }
        else
          if q = stStart then { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }
          else
            if q = stCarryFork then carry false work
            else
              if q = stCarryLeaf then carry true work
              else
                if q = stReturn then
                  if origin (work 0) = true then
                    { inputMove := 0, workActions := fun x ↦ (none, 0), outS := none,
                      q' := some (if (work 2 == some 0) = true then stDone else stTree) }
                  else
                    { inputMove := 0, workActions := fun i ↦ (none, if i = 2 then 0 else -1), outS := none,
                      q' := some stReturn }
                else
                  if q = stTree then consume (if (val✝ == 0) = true then stString else stCarryFork)
                  else
                    if q = stString then consume (if (val✝ == 0) = true then stCarryLeaf else stBit)
                    else if q = stBit then consume stString else consume stDead).workActions
      1).2 split_ifsposq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝:q = stInit⊢ ({ inputMove := 0,
          workActions := fun i ↦
            if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1),
          outS := none, q' := some stStart }.workActions
      0).2 =
  ({ inputMove := 0,
          workActions := fun i ↦
            if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1),
          outS := none, q' := some stStart }.workActions
      1).2posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝¹:¬q = stInith✝:q = stStart⊢ ({ inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }.workActions 0).2 =
  ({ inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }.workActions 1).2posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝²:¬q = stInith✝¹:¬q = stStarth✝:q = stCarryFork⊢ ((carry false work).workActions 0).2 = ((carry false work).workActions 1).2posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝³:¬q = stInith✝²:¬q = stStarth✝¹:¬q = stCarryForkh✝:q = stCarryLeaf⊢ ((carry true work).workActions 0).2 = ((carry true work).workActions 1).2posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁶:¬q = stInith✝⁵:¬q = stStarth✝⁴:¬q = stCarryForkh✝³:¬q = stCarryLeafh✝²:q = stReturnh✝¹:origin (work 0) = trueh✝:(work 2 == some 0) = true⊢ ({ inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stDone }.workActions 0).2 =
  ({ inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stDone }.workActions 1).2negq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁶:¬q = stInith✝⁵:¬q = stStarth✝⁴:¬q = stCarryForkh✝³:¬q = stCarryLeafh✝²:q = stReturnh✝¹:origin (work 0) = trueh✝:¬(work 2 == some 0) = true⊢ ({ inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }.workActions 0).2 =
  ({ inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }.workActions 1).2negq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁵:¬q = stInith✝⁴:¬q = stStarth✝³:¬q = stCarryForkh✝²:¬q = stCarryLeafh✝¹:q = stReturnh✝:¬origin (work 0) = true⊢ ({ inputMove := 0, workActions := fun i ↦ (none, if i = 2 then 0 else -1), outS := none,
          q' := some stReturn }.workActions
      0).2 =
  ({ inputMove := 0, workActions := fun i ↦ (none, if i = 2 then 0 else -1), outS := none,
          q' := some stReturn }.workActions
      1).2posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁶:¬q = stInith✝⁵:¬q = stStarth✝⁴:¬q = stCarryForkh✝³:¬q = stCarryLeafh✝²:¬q = stReturnh✝¹:q = stTreeh✝:(val✝ == 0) = true⊢ ((consume stString).workActions 0).2 = ((consume stString).workActions 1).2negq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁶:¬q = stInith✝⁵:¬q = stStarth✝⁴:¬q = stCarryForkh✝³:¬q = stCarryLeafh✝²:¬q = stReturnh✝¹:q = stTreeh✝:¬(val✝ == 0) = true⊢ ((consume stCarryFork).workActions 0).2 = ((consume stCarryFork).workActions 1).2posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁷:¬q = stInith✝⁶:¬q = stStarth✝⁵:¬q = stCarryForkh✝⁴:¬q = stCarryLeafh✝³:¬q = stReturnh✝²:¬q = stTreeh✝¹:q = stStringh✝:(val✝ == 0) = true⊢ ((consume stCarryLeaf).workActions 0).2 = ((consume stCarryLeaf).workActions 1).2negq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁷:¬q = stInith✝⁶:¬q = stStarth✝⁵:¬q = stCarryForkh✝⁴:¬q = stCarryLeafh✝³:¬q = stReturnh✝²:¬q = stTreeh✝¹:q = stStringh✝:¬(val✝ == 0) = true⊢ ((consume stBit).workActions 0).2 = ((consume stBit).workActions 1).2posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁷:¬q = stInith✝⁶:¬q = stStarth✝⁵:¬q = stCarryForkh✝⁴:¬q = stCarryLeafh✝³:¬q = stReturnh✝²:¬q = stTreeh✝¹:¬q = stStringh✝:q = stBit⊢ ((consume stString).workActions 0).2 = ((consume stString).workActions 1).2negq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁷:¬q = stInith✝⁶:¬q = stStarth✝⁵:¬q = stCarryForkh✝⁴:¬q = stCarryLeafh✝³:¬q = stReturnh✝²:¬q = stTreeh✝¹:¬q = stStringh✝:¬q = stBit⊢ ((consume stDead).workActions 0).2 = ((consume stDead).workActions 1).2 <;>posq:Fin 10work:Fin 3 → Option (Fin 4)h✝:q = stInit⊢ ({ inputMove := 0,
          workActions := fun i ↦
            if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1),
          outS := none, q' := some stStart }.workActions
      0).2 =
  ({ inputMove := 0,
          workActions := fun i ↦
            if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1),
          outS := none, q' := some stStart }.workActions
      1).2posq:Fin 10work:Fin 3 → Option (Fin 4)h✝¹:¬q = stInith✝:q = stStart⊢ ({ inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }.workActions 0).2 =
  ({ inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }.workActions 1).2posq:Fin 10work:Fin 3 → Option (Fin 4)h✝²:¬q = stInith✝¹:¬q = stStarth✝:q = stCarryFork⊢ ((carry false work).workActions 0).2 = ((carry false work).workActions 1).2posq:Fin 10work:Fin 3 → Option (Fin 4)h✝³:¬q = stInith✝²:¬q = stStarth✝¹:¬q = stCarryForkh✝:q = stCarryLeaf⊢ ((carry true work).workActions 0).2 = ((carry true work).workActions 1).2posq:Fin 10work:Fin 3 → Option (Fin 4)h✝⁶:¬q = stInith✝⁵:¬q = stStarth✝⁴:¬q = stCarryForkh✝³:¬q = stCarryLeafh✝²:q = stReturnh✝¹:origin (work 0) = trueh✝:(work 2 == some 0) = true⊢ ({ inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stDone }.workActions 0).2 =
  ({ inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stDone }.workActions 1).2negq:Fin 10work:Fin 3 → Option (Fin 4)h✝⁶:¬q = stInith✝⁵:¬q = stStarth✝⁴:¬q = stCarryForkh✝³:¬q = stCarryLeafh✝²:q = stReturnh✝¹:origin (work 0) = trueh✝:¬(work 2 == some 0) = true⊢ ({ inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }.workActions 0).2 =
  ({ inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }.workActions 1).2negq:Fin 10work:Fin 3 → Option (Fin 4)h✝⁵:¬q = stInith✝⁴:¬q = stStarth✝³:¬q = stCarryForkh✝²:¬q = stCarryLeafh✝¹:q = stReturnh✝:¬origin (work 0) = true⊢ ({ inputMove := 0, workActions := fun i ↦ (none, if i = 2 then 0 else -1), outS := none,
          q' := some stReturn }.workActions
      0).2 =
  ({ inputMove := 0, workActions := fun i ↦ (none, if i = 2 then 0 else -1), outS := none,
          q' := some stReturn }.workActions
      1).2negq:Fin 10work:Fin 3 → Option (Fin 4)h✝⁴:¬q = stInith✝³:¬q = stStarth✝²:¬q = stCarryForkh✝¹:¬q = stCarryLeafh✝:¬q = stReturn⊢ ((finish (q == stDone)).workActions 0).2 = ((finish (q == stDone)).workActions 1).2posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝:q = stInit⊢ ({ inputMove := 0,
          workActions := fun i ↦
            if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1),
          outS := none, q' := some stStart }.workActions
      0).2 =
  ({ inputMove := 0,
          workActions := fun i ↦
            if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1),
          outS := none, q' := some stStart }.workActions
      1).2posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝¹:¬q = stInith✝:q = stStart⊢ ({ inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }.workActions 0).2 =
  ({ inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }.workActions 1).2posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝²:¬q = stInith✝¹:¬q = stStarth✝:q = stCarryFork⊢ ((carry false work).workActions 0).2 = ((carry false work).workActions 1).2posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝³:¬q = stInith✝²:¬q = stStarth✝¹:¬q = stCarryForkh✝:q = stCarryLeaf⊢ ((carry true work).workActions 0).2 = ((carry true work).workActions 1).2posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁶:¬q = stInith✝⁵:¬q = stStarth✝⁴:¬q = stCarryForkh✝³:¬q = stCarryLeafh✝²:q = stReturnh✝¹:origin (work 0) = trueh✝:(work 2 == some 0) = true⊢ ({ inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stDone }.workActions 0).2 =
  ({ inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stDone }.workActions 1).2negq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁶:¬q = stInith✝⁵:¬q = stStarth✝⁴:¬q = stCarryForkh✝³:¬q = stCarryLeafh✝²:q = stReturnh✝¹:origin (work 0) = trueh✝:¬(work 2 == some 0) = true⊢ ({ inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }.workActions 0).2 =
  ({ inputMove := 0, workActions := fun x ↦ (none, 0), outS := none, q' := some stTree }.workActions 1).2negq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁵:¬q = stInith✝⁴:¬q = stStarth✝³:¬q = stCarryForkh✝²:¬q = stCarryLeafh✝¹:q = stReturnh✝:¬origin (work 0) = true⊢ ({ inputMove := 0, workActions := fun i ↦ (none, if i = 2 then 0 else -1), outS := none,
          q' := some stReturn }.workActions
      0).2 =
  ({ inputMove := 0, workActions := fun i ↦ (none, if i = 2 then 0 else -1), outS := none,
          q' := some stReturn }.workActions
      1).2posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁶:¬q = stInith✝⁵:¬q = stStarth✝⁴:¬q = stCarryForkh✝³:¬q = stCarryLeafh✝²:¬q = stReturnh✝¹:q = stTreeh✝:(val✝ == 0) = true⊢ ((consume stString).workActions 0).2 = ((consume stString).workActions 1).2negq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁶:¬q = stInith✝⁵:¬q = stStarth✝⁴:¬q = stCarryForkh✝³:¬q = stCarryLeafh✝²:¬q = stReturnh✝¹:q = stTreeh✝:¬(val✝ == 0) = true⊢ ((consume stCarryFork).workActions 0).2 = ((consume stCarryFork).workActions 1).2posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁷:¬q = stInith✝⁶:¬q = stStarth✝⁵:¬q = stCarryForkh✝⁴:¬q = stCarryLeafh✝³:¬q = stReturnh✝²:¬q = stTreeh✝¹:q = stStringh✝:(val✝ == 0) = true⊢ ((consume stCarryLeaf).workActions 0).2 = ((consume stCarryLeaf).workActions 1).2negq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁷:¬q = stInith✝⁶:¬q = stStarth✝⁵:¬q = stCarryForkh✝⁴:¬q = stCarryLeafh✝³:¬q = stReturnh✝²:¬q = stTreeh✝¹:q = stStringh✝:¬(val✝ == 0) = true⊢ ((consume stBit).workActions 0).2 = ((consume stBit).workActions 1).2posq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁷:¬q = stInith✝⁶:¬q = stStarth✝⁵:¬q = stCarryForkh✝⁴:¬q = stCarryLeafh✝³:¬q = stReturnh✝²:¬q = stTreeh✝¹:¬q = stStringh✝:q = stBit⊢ ((consume stString).workActions 0).2 = ((consume stString).workActions 1).2negq:Fin 10work:Fin 3 → Option (Fin 4)val✝:Fin 4h✝⁷:¬q = stInith✝⁶:¬q = stStarth✝⁵:¬q = stCarryForkh✝⁴:¬q = stCarryLeafh✝³:¬q = stReturnh✝²:¬q = stTreeh✝¹:¬q = stStringh✝:¬q = stBit⊢ ((consume stDead).workActions 0).2 = ((consume stDead).workActions 1).2 simp [carry, consume, finish]All goals completed! 🐙

A stationary or right-moving displacement cannot lower an input position.

theorem le_moveInputPos {n : ℕ} (p : Fin (n + 2)) (d : SignType) (h : d ≠ -1) :
    p.val ≤ (moveInputPos p d).val := byn:ℕp:Fin (n + 2)d:SignTypeh:d ≠ -1⊢ ↑p ≤ ↑(moveInputPos p d)
  cases d with
  | neg =>negn:ℕp:Fin (n + 2)h:SignType.neg ≠ -1⊢ ↑p ≤ ↑(moveInputPos p SignType.neg) exact False.elim (h rfl)All goals completed! 🐙
  | zero =>zeron:ℕp:Fin (n + 2)h:SignType.zero ≠ -1⊢ ↑p ≤ ↑(moveInputPos p SignType.zero)
    unfold moveInputPoszeron:ℕp:Fin (n + 2)h:SignType.zero ≠ -1⊢ ↑p ≤
  ↑(have p_1 := (↑↑p + ↑SignType.zero).toNat;
    if h : p_1 < n + 2 then ⟨p_1, h⟩ else ⟨n + 1, ⋯⟩)
    have hz : ((p.val : ℤ) + (SignType.zero.cast : ℤ)).toNat = p.val := byn:ℕp:Fin (n + 2)d:SignTypeh:d ≠ -1⊢ ↑p ≤ ↑(moveInputPos p d)
      change ((p.val : ℤ) + 0).toNat = p.valn:ℕp:Fin (n + 2)h:SignType.zero ≠ -1⊢ (↑↑p + 0).toNat = ↑p
      omegazeron:ℕp:Fin (n + 2)h:SignType.zero ≠ -1hz:(↑↑p + ↑SignType.zero).toNat = ↑p⊢ ↑p ≤
  ↑(have p_1 := (↑↑p + ↑SignType.zero).toNat;
    if h : p_1 < n + 2 then ⟨p_1, h⟩ else ⟨n + 1, ⋯⟩)
    rw [hzzeron:ℕp:Fin (n + 2)h:SignType.zero ≠ -1hz:(↑↑p + ↑SignType.zero).toNat = ↑p⊢ ↑p ≤
  ↑(have p_1 := ↑p;
    if h : p_1 < n + 2 then ⟨p_1, h⟩ else ⟨n + 1, ⋯⟩)]zeron:ℕp:Fin (n + 2)h:SignType.zero ≠ -1hz:(↑↑p + ↑SignType.zero).toNat = ↑p⊢ ↑p ≤
  ↑(have p_1 := ↑p;
    if h : p_1 < n + 2 then ⟨p_1, h⟩ else ⟨n + 1, ⋯⟩)
    dsimp onlyzeron:ℕp:Fin (n + 2)h:SignType.zero ≠ -1hz:(↑↑p + ↑SignType.zero).toNat = ↑p⊢ ↑p ≤ ↑(if h : ↑p < n + 2 then ⟨↑p, h⟩ else ⟨n + 1, ⋯⟩)
    splitzero.isTruen:ℕp:Fin (n + 2)h:SignType.zero ≠ -1hz:(↑↑p + ↑SignType.zero).toNat = ↑ph✝:↑p < n + 2⊢ ↑p ≤ ↑⟨↑p, h✝⟩zero.isFalsen:ℕp:Fin (n + 2)h:SignType.zero ≠ -1hz:(↑↑p + ↑SignType.zero).toNat = ↑ph✝:¬↑p < n + 2⊢ ↑p ≤ ↑⟨n + 1, ⋯⟩
    ·zero.isTruen:ℕp:Fin (n + 2)h:SignType.zero ≠ -1hz:(↑↑p + ↑SignType.zero).toNat = ↑ph✝:↑p < n + 2⊢ ↑p ≤ ↑⟨↑p, h✝⟩ exact Nat.le_refl _All goals completed! 🐙
    ·zero.isFalsen:ℕp:Fin (n + 2)h:SignType.zero ≠ -1hz:(↑↑p + ↑SignType.zero).toNat = ↑ph✝:¬↑p < n + 2⊢ ↑p ≤ ↑⟨n + 1, ⋯⟩ exact Nat.le_of_lt_succ p.isLtAll goals completed! 🐙
  | pos =>posn:ℕp:Fin (n + 2)h:SignType.pos ≠ -1⊢ ↑p ≤ ↑(moveInputPos p SignType.pos)
    unfold moveInputPosposn:ℕp:Fin (n + 2)h:SignType.pos ≠ -1⊢ ↑p ≤
  ↑(have p_1 := (↑↑p + ↑SignType.pos).toNat;
    if h : p_1 < n + 2 then ⟨p_1, h⟩ else ⟨n + 1, ⋯⟩)
    have hz : ((p.val : ℤ) + (SignType.pos.cast : ℤ)).toNat = p.val + 1 := byn:ℕp:Fin (n + 2)d:SignTypeh:d ≠ -1⊢ ↑p ≤ ↑(moveInputPos p d)
      change ((p.val : ℤ) + 1).toNat = p.val + 1n:ℕp:Fin (n + 2)h:SignType.pos ≠ -1⊢ (↑↑p + 1).toNat = ↑p + 1
      omegaposn:ℕp:Fin (n + 2)h:SignType.pos ≠ -1hz:(↑↑p + ↑SignType.pos).toNat = ↑p + 1⊢ ↑p ≤
  ↑(have p_1 := (↑↑p + ↑SignType.pos).toNat;
    if h : p_1 < n + 2 then ⟨p_1, h⟩ else ⟨n + 1, ⋯⟩)
    rw [hzposn:ℕp:Fin (n + 2)h:SignType.pos ≠ -1hz:(↑↑p + ↑SignType.pos).toNat = ↑p + 1⊢ ↑p ≤
  ↑(have p_1 := ↑p + 1;
    if h : p_1 < n + 2 then ⟨p_1, h⟩ else ⟨n + 1, ⋯⟩)]posn:ℕp:Fin (n + 2)h:SignType.pos ≠ -1hz:(↑↑p + ↑SignType.pos).toNat = ↑p + 1⊢ ↑p ≤
  ↑(have p_1 := ↑p + 1;
    if h : p_1 < n + 2 then ⟨p_1, h⟩ else ⟨n + 1, ⋯⟩)
    dsimp onlyposn:ℕp:Fin (n + 2)h:SignType.pos ≠ -1hz:(↑↑p + ↑SignType.pos).toNat = ↑p + 1⊢ ↑p ≤ ↑(if h : ↑p + 1 < n + 2 then ⟨↑p + 1, h⟩ else ⟨n + 1, ⋯⟩)
    splitpos.isTruen:ℕp:Fin (n + 2)h:SignType.pos ≠ -1hz:(↑↑p + ↑SignType.pos).toNat = ↑p + 1h✝:↑p + 1 < n + 2⊢ ↑p ≤ ↑⟨↑p + 1, h✝⟩pos.isFalsen:ℕp:Fin (n + 2)h:SignType.pos ≠ -1hz:(↑↑p + ↑SignType.pos).toNat = ↑p + 1h✝:¬↑p + 1 < n + 2⊢ ↑p ≤ ↑⟨n + 1, ⋯⟩
    ·pos.isTruen:ℕp:Fin (n + 2)h:SignType.pos ≠ -1hz:(↑↑p + ↑SignType.pos).toNat = ↑p + 1h✝:↑p + 1 < n + 2⊢ ↑p ≤ ↑⟨↑p + 1, h✝⟩ exact Nat.le_succ _All goals completed! 🐙
    ·pos.isFalsen:ℕp:Fin (n + 2)h:SignType.pos ≠ -1hz:(↑↑p + ↑SignType.pos).toNat = ↑p + 1h✝:¬↑p + 1 < n + 2⊢ ↑p ≤ ↑⟨n + 1, ⋯⟩ exact Nat.le_of_lt_succ p.isLtAll goals completed! 🐙

The initialized configuration has counter values one and zero.

def startCfg (input : List (Fin 4)) : Cfg 3 (Fin 4) (Fin 10) input where
  state := some stTree
  inputPos := 1
  workTapes i z := if z = 0 then some (if i = 0 then 3 else if i = 1 then 2 else 0)
    else none
  workTapePos i := if i = 2 then 1 else 0

The digits read at nonnegative positions of a work tape.

def digits {input : List (Fin 4)} (cfg : Cfg 3 (Fin 4) (Fin 10) input)
    (i : Fin 3) (j : ℕ) : Bool := digit (cfg.workTapes i j)

Both carry states resolve to the common carry transition.

theorem tr_carry (leaf : Bool) (input : Option (Fin 4))
    (work : Fin 3 → Option (Fin 4)) :
    machine.tr (if leaf then stCarryLeaf else stCarryFork) input work = carry leaf work := byleaf:Boolinput:Option (Fin 4)work:Fin 3 → Option (Fin 4)⊢ machine.tr (if leaf = true then stCarryLeaf else stCarryFork) input work = carry leaf work
  cases leaffalseinput:Option (Fin 4)work:Fin 3 → Option (Fin 4)⊢ machine.tr (if false = true then stCarryLeaf else stCarryFork) input work = carry false worktrueinput:Option (Fin 4)work:Fin 3 → Option (Fin 4)⊢ machine.tr (if true = true then stCarryLeaf else stCarryFork) input work = carry true work <;>falseinput:Option (Fin 4)work:Fin 3 → Option (Fin 4)⊢ machine.tr (if false = true then stCarryLeaf else stCarryFork) input work = carry false worktrueinput:Option (Fin 4)work:Fin 3 → Option (Fin 4)⊢ machine.tr (if true = true then stCarryLeaf else stCarryFork) input work = carry true work rflAll goals completed! 🐙

A return configuration with the binary heads at a specified nonnegative position.

def returnCfg {input : List (Fin 4)} (cfg : Cfg 3 (Fin 4) (Fin 10) input)
    (p : ℕ) : Cfg 3 (Fin 4) (Fin 10) input where
  state := some stReturn
  inputPos := cfg.inputPos
  workTapes := cfg.workTapes
  workTapePos i := if i = 2 then cfg.workTapePos 2 else p

The configuration reached when the return's final state change has completed.

def returnedCfg {input : List (Fin 4)} (cfg : Cfg 3 (Fin 4) (Fin 10) input) :
    Cfg 3 (Fin 4) (Fin 10) input :=
  { returnCfg cfg 0 with
    state := some (if cfg.workTapes 2 (cfg.workTapePos 2) == some 0 then stDone else stTree) }

A configuration already in the return state equals its return normal form.

theorem returnCfg_self {input : List (Fin 4)}
    (cfg : Cfg 3 (Fin 4) (Fin 10) input) (p : ℕ)
    (hq : cfg.state = some stReturn)
    (hp0 : cfg.workTapePos 0 = p) (hp1 : cfg.workTapePos 1 = p) :
    returnCfg cfg p = cfg := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputp:ℕhq:cfg.state = some stReturnhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑p⊢ returnCfg cfg p = cfg
  refine Cfg.ext hq.symm rfl rfl ?_input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputp:ℕhq:cfg.state = some stReturnhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑p⊢ (returnCfg cfg p).workTapePos = cfg.workTapePos
  funext iinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputp:ℕhq:cfg.state = some stReturnhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑pi:Fin 3⊢ (returnCfg cfg p).workTapePos i = cfg.workTapePos i
  exact Fin.cases hp0.symm (Fin.cases hp1.symm (Fin.cases rfl (fun i ↦ Fin.elim0 i))) iAll goals completed! 🐙

The finite machine state corresponding to a scanner mode.

def modeState : Mode → Fin 10
  | .tree => stTree
  | .string => stString
  | .bit => stBit
  | .done => stDone
  | .dead => stDead

The state entered by consuming one bit, before any counter update.

def postReadState : Mode → Bool → Fin 10
  | .tree, false => stString
  | .tree, true => stCarryFork
  | .string, false => stCarryLeaf
  | .string, true => stBit
  | .bit, _ => stString
  | .done, _ => stDead
  | .dead, _ => stDead

Reading a bit selects the grammar transition without modifying work tapes.

theorem tr_read (m : Mode) (b : Bool) (work : Fin 3 → Option (Fin 4)) :
    machine.tr (modeState m) (some (boolEmb b)) work = consume (postReadState m b) := bym:Modeb:Boolwork:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState m) (some (boolEmb b)) work = consume (postReadState m b)
  cases mtreeb:Boolwork:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.tree) (some (boolEmb b)) work = consume (postReadState Mode.tree b)stringb:Boolwork:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.string) (some (boolEmb b)) work = consume (postReadState Mode.string b)bitb:Boolwork:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.bit) (some (boolEmb b)) work = consume (postReadState Mode.bit b)doneb:Boolwork:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.done) (some (boolEmb b)) work = consume (postReadState Mode.done b)deadb:Boolwork:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.dead) (some (boolEmb b)) work = consume (postReadState Mode.dead b) <;>treeb:Boolwork:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.tree) (some (boolEmb b)) work = consume (postReadState Mode.tree b)stringb:Boolwork:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.string) (some (boolEmb b)) work = consume (postReadState Mode.string b)bitb:Boolwork:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.bit) (some (boolEmb b)) work = consume (postReadState Mode.bit b)doneb:Boolwork:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.done) (some (boolEmb b)) work = consume (postReadState Mode.done b)deadb:Boolwork:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.dead) (some (boolEmb b)) work = consume (postReadState Mode.dead b) cases bdead.falsework:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.dead) (some (boolEmb false)) work = consume (postReadState Mode.dead false)dead.truework:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.dead) (some (boolEmb true)) work = consume (postReadState Mode.dead true) <;>tree.falsework:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.tree) (some (boolEmb false)) work = consume (postReadState Mode.tree false)tree.truework:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.tree) (some (boolEmb true)) work = consume (postReadState Mode.tree true)string.falsework:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.string) (some (boolEmb false)) work = consume (postReadState Mode.string false)string.truework:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.string) (some (boolEmb true)) work = consume (postReadState Mode.string true)bit.falsework:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.bit) (some (boolEmb false)) work = consume (postReadState Mode.bit false)bit.truework:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.bit) (some (boolEmb true)) work = consume (postReadState Mode.bit true)done.falsework:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.done) (some (boolEmb false)) work = consume (postReadState Mode.done false)done.truework:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.done) (some (boolEmb true)) work = consume (postReadState Mode.done true)dead.falsework:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.dead) (some (boolEmb false)) work = consume (postReadState Mode.dead false)dead.truework:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.dead) (some (boolEmb true)) work = consume (postReadState Mode.dead true) rflAll goals completed! 🐙

Reading a bit changes the input position and finite control only.

def consumeCfg {input : List (Fin 4)} (cfg : Cfg 3 (Fin 4) (Fin 10) input) (q : Fin 10) :
    Cfg 3 (Fin 4) (Fin 10) input :=
  { cfg with state := some q, inputPos := moveInputPos cfg.inputPos 1 }

The input position advances by one when it is not the right end marker.

theorem consumeCfg_inputPos {input : List (Fin 4)} (cfg : Cfg 3 (Fin 4) (Fin 10) input)
    (q : Fin 10) (h : cfg.inputPos.val < input.length + 1) :
    (consumeCfg cfg q).inputPos.val = cfg.inputPos.val + 1 := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:↑cfg.inputPos < input.length + 1⊢ ↑(consumeCfg cfg q).inputPos = ↑cfg.inputPos + 1
  change (moveInputPos cfg.inputPos SignType.pos).val = _input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:↑cfg.inputPos < input.length + 1⊢ ↑(moveInputPos cfg.inputPos SignType.pos) = ↑cfg.inputPos + 1
  unfold moveInputPosinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:↑cfg.inputPos < input.length + 1⊢ ↑(have p := (↑↑cfg.inputPos + ↑SignType.pos).toNat;
    if h : p < input.length + 2 then ⟨p, h⟩ else ⟨input.length + 1, ⋯⟩) =
  ↑cfg.inputPos + 1
  have hz : ((cfg.inputPos.val : ℤ) + (SignType.pos.cast : ℤ)).toNat =
      cfg.inputPos.val + 1 := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:↑cfg.inputPos < input.length + 1⊢ ↑(consumeCfg cfg q).inputPos = ↑cfg.inputPos + 1
    change ((cfg.inputPos.val : ℤ) + 1).toNat = cfg.inputPos.val + 1input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:↑cfg.inputPos < input.length + 1⊢ (↑↑cfg.inputPos + 1).toNat = ↑cfg.inputPos + 1
    omegainput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:↑cfg.inputPos < input.length + 1hz:(↑↑cfg.inputPos + ↑SignType.pos).toNat = ↑cfg.inputPos + 1⊢ ↑(have p := (↑↑cfg.inputPos + ↑SignType.pos).toNat;
    if h : p < input.length + 2 then ⟨p, h⟩ else ⟨input.length + 1, ⋯⟩) =
  ↑cfg.inputPos + 1
  rw [hzinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:↑cfg.inputPos < input.length + 1hz:(↑↑cfg.inputPos + ↑SignType.pos).toNat = ↑cfg.inputPos + 1⊢ ↑(have p := ↑cfg.inputPos + 1;
    if h : p < input.length + 2 then ⟨p, h⟩ else ⟨input.length + 1, ⋯⟩) =
  ↑cfg.inputPos + 1]input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:↑cfg.inputPos < input.length + 1hz:(↑↑cfg.inputPos + ↑SignType.pos).toNat = ↑cfg.inputPos + 1⊢ ↑(have p := ↑cfg.inputPos + 1;
    if h : p < input.length + 2 then ⟨p, h⟩ else ⟨input.length + 1, ⋯⟩) =
  ↑cfg.inputPos + 1
  dsimp onlyinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:↑cfg.inputPos < input.length + 1hz:(↑↑cfg.inputPos + ↑SignType.pos).toNat = ↑cfg.inputPos + 1⊢ ↑(if h : ↑cfg.inputPos + 1 < input.length + 2 then ⟨↑cfg.inputPos + 1, h⟩ else ⟨input.length + 1, ⋯⟩) =
  ↑cfg.inputPos + 1
  splitisTrueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:↑cfg.inputPos < input.length + 1hz:(↑↑cfg.inputPos + ↑SignType.pos).toNat = ↑cfg.inputPos + 1h✝:↑cfg.inputPos + 1 < input.length + 2⊢ ↑⟨↑cfg.inputPos + 1, h✝⟩ = ↑cfg.inputPos + 1isFalseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:↑cfg.inputPos < input.length + 1hz:(↑↑cfg.inputPos + ↑SignType.pos).toNat = ↑cfg.inputPos + 1h✝:¬↑cfg.inputPos + 1 < input.length + 2⊢ ↑⟨input.length + 1, ⋯⟩ = ↑cfg.inputPos + 1
  ·isTrueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:↑cfg.inputPos < input.length + 1hz:(↑↑cfg.inputPos + ↑SignType.pos).toNat = ↑cfg.inputPos + 1h✝:↑cfg.inputPos + 1 < input.length + 2⊢ ↑⟨↑cfg.inputPos + 1, h✝⟩ = ↑cfg.inputPos + 1 rflAll goals completed! 🐙
  ·isFalseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10h:↑cfg.inputPos < input.length + 1hz:(↑↑cfg.inputPos + ↑SignType.pos).toNat = ↑cfg.inputPos + 1h✝:¬↑cfg.inputPos + 1 < input.length + 2⊢ ↑⟨input.length + 1, ⋯⟩ = ↑cfg.inputPos + 1 omegaAll goals completed! 🐙

The right end marker emits the accepting-mode test and halts.

theorem tr_end (m : Mode) (work : Fin 3 → Option (Fin 4)) :
    machine.tr (modeState m) none work = finish (decide (m = .done)) := bym:Modework:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState m) none work = finish (decide (m = Mode.done))
  cases mtreework:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.tree) none work = finish (decide (Mode.tree = Mode.done))stringwork:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.string) none work = finish (decide (Mode.string = Mode.done))bitwork:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.bit) none work = finish (decide (Mode.bit = Mode.done))donework:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.done) none work = finish (decide (Mode.done = Mode.done))deadwork:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.dead) none work = finish (decide (Mode.dead = Mode.done)) <;>treework:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.tree) none work = finish (decide (Mode.tree = Mode.done))stringwork:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.string) none work = finish (decide (Mode.string = Mode.done))bitwork:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.bit) none work = finish (decide (Mode.bit = Mode.done))donework:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.done) none work = finish (decide (Mode.done = Mode.done))deadwork:Fin 3 → Option (Fin 4)⊢ machine.tr (modeState Mode.dead) none work = finish (decide (Mode.dead = Mode.done)) rflAll goals completed! 🐙

Every work head lies in the nonnegative interval bounded by the chosen width.

def HeadBound {input : List (Fin 4)} (width : ℕ) (cfg : Cfg 3 (Fin 4) (Fin 10) input) :
    Prop := ∀ i, 0 ≤ cfg.workTapePos i ∧ cfg.workTapePos i ≤ (width : ℤ)

end Geb.BitTree.BinaryMachine