1. Geb
  2. Prototypes
  3. Computability
  4. BitTree
  5. Elias
  6. Machine
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
set_option doc.verso true

A machine for trees with Elias delta leaf lengths

Four work tapes hold the pending-tree count, the leading-zero count, the binary length of a length, and the binary payload length. The first two counts use head positions. The binary counters have a marked origin and most-significant-first digits, followed by a blank. Appending a digit takes one transition. Decrementing a positive counter sweeps left and returns right, retaining a zero-test result in finite control. Thus a declared length never causes a unary allocation.

Main definitions

  • machine is the four-work-tape transition table.

  • borrow, sweepLeft and sweepRight implement a decrement.

  • clear erases both binary fields when a leaf finishes.

Tags

Elias delta code, Turing machine, binary tree, countdown

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

Binary input and output use zero and one; two marks a work-tape origin.

def boolEmb : Bool ↪ Fin 3 where toFun b := if b then 1 else 0 inj' a b := a:Boolb:Bool⊢ (fun b ↦ if b = true then 1 else 0) a = (fun b ↦ if b = true then 1 else 0) b → a = b b:Bool⊢ (fun b ↦ if b = true then 1 else 0) false = (fun b ↦ if b = true then 1 else 0) b → false = bb:Bool⊢ (fun b ↦ if b = true then 1 else 0) true = (fun b ↦ if b = true then 1 else 0) b → true = b b:Bool⊢ (fun b ↦ if b = true then 1 else 0) false = (fun b ↦ if b = true then 1 else 0) b → false = bb:Bool⊢ (fun b ↦ if b = true then 1 else 0) true = (fun b ↦ if b = true then 1 else 0) b → true = b ⊢ (fun b ↦ if b = true then 1 else 0) true = (fun b ↦ if b = true then 1 else 0) false → true = false⊢ (fun b ↦ if b = true then 1 else 0) true = (fun b ↦ if b = true then 1 else 0) true → true = true ⊢ (fun b ↦ if b = true then 1 else 0) false = (fun b ↦ if b = true then 1 else 0) false → false = false⊢ (fun b ↦ if b = true then 1 else 0) false = (fun b ↦ if b = true then 1 else 0) true → false = true⊢ (fun b ↦ if b = true then 1 else 0) true = (fun b ↦ if b = true then 1 else 0) false → true = false⊢ (fun b ↦ if b = true then 1 else 0) true = (fun b ↦ if b = true then 1 else 0) true → true = true All goals completed! 🐙

The embedding reads as the corresponding finite alphabet digit.

theorem boolEmb_apply (b : Bool) : boolEmb b = if b then 1 else 0 := rfl

The finite control has room for both counter subroutines and their boolean flags.

abbrev Control := Fin 25

Initialize all four origin markers.

def stInit : Control := 0

Read a tree constructor.

def stTree : Control := 1

Count the zero prefix of a delta code.

def stZeros : Control := 2

Test whether the binary width field is complete.

def stSizeCheck : Control := 3

Append one bit to the binary width field.

def stSizeBit : Control := 4

Append one bit to the binary payload-length field.

def stLengthBit : Control := 5

Consume one raw payload bit.

def stPayloadBit : Control := 6

Erase the completed leaf's binary counters.

def stClear : Control := 7

Test whether decrementing the pending count completed the tree.

def stLeaf : Control := 8

Accept precisely if no input remains.

def stDone : Control := 9

Reject at the end of the input.

def stDead : Control := 10

Enter the selected countdown from its right-hand blank.

def stDecrement (value : Bool) : Control := if value then 12 else 11

Borrow leftward, remembering whether a lower digit has become one.

def stBorrow (value seen : Bool) : Control := if value then (if seen then 16 else 15) else (if seen then 14 else 13)

Inspect the remaining higher digits while continuing to the origin.

def stLeft (value seen : Bool) : Control := if value then (if seen then 20 else 19) else (if seen then 18 else 17)

Return to the right-hand blank carrying the zero-test result.

def stRight (value seen : Bool) : Control := if value then (if seen then 24 else 23) else (if seen then 22 else 21)

Select either the width countdown or the payload countdown.

def counterTape (value : Bool) : Fin 4 := if value then 3 else 2

A stationary state change with no output or tape writes.

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

Consume one input bit and enter the given state.

def consume (q : Control) : TransitionOut 4 (Fin 3) Control := { jump q with inputMove := 1 }

Emit one boolean and halt.

def finish (b : Bool) : TransitionOut 4 (Fin 3) Control := { jump stDead with outS := some (boolEmb b), q' := none }

Move or write only the selected binary counter.

-- ponytail: full-width countdown sweeps give quadratic time; -- amortized local updates can improve it.def counterAction (value : Bool) (write : Option (Option (Fin 3))) (move : SignType) (q : Control) : TransitionOut 4 (Fin 3) Control := { jump q with workActions := fun i ↦ if i = counterTape value then (write, move) else (none, 0) }

Subtract one, changing trailing zeros to ones until the first one is reached.

def borrow (value seen : Bool) (work : Fin 4 → Option (Fin 3)) : TransitionOut 4 (Fin 3) Control := if work (counterTape value) == some 2 then finish false else if work (counterTape value) == some 1 then counterAction value (some (some 0)) (-1) (stLeft value seen) else counterAction value (some (some 1)) (-1) (stBorrow value true)

Inspect higher digits, remembering whether any result digit is one.

def sweepLeft (value seen : Bool) (work : Fin 4 → Option (Fin 3)) : TransitionOut 4 (Fin 3) Control := if work (counterTape value) == some 2 then counterAction value none 1 (stRight value seen) else counterAction value none (-1) (stLeft value (seen || work (counterTape value) == some 1))

Resume decoding after the selected countdown has been tested for zero.

def afterDecrement (value seen : Bool) : Control := if value then (if seen then stPayloadBit else stClear) else (if seen then stLengthBit else stDecrement true)

Return to the blank immediately after the selected counter's last digit.

def sweepRight (value seen : Bool) (work : Fin 4 → Option (Fin 3)) : TransitionOut 4 (Fin 3) Control := if work (counterTape value) == none then jump (afterDecrement value seen) else counterAction value none 1 (stRight value seen)

Clear both binary fields in parallel, leaving their origin markers in place.

def clear (work : Fin 4 → Option (Fin 3)) : TransitionOut 4 (Fin 3) Control := if work 2 == some 2 && work 3 == some 2 then { jump stLeaf with workActions := fun i ↦ if i = 0 then (none, -1) else if i = 1 then (none, 0) else (none, 1) } else { jump stClear with workActions := fun i ↦ if i = 0 ∨ i = 1 ∨ work i = some 2 then (none, 0) else (some none, -1) }

Read the next external bit once every internal subroutine has finished.

def read (q : Control) (b : Fin 3) : TransitionOut 4 (Fin 3) Control := if q = stTree then if b == 1 then { consume stTree with workActions := fun i ↦ (none, if i = 0 then 1 else 0) } else { consume stZeros with workActions := fun i ↦ if i = 3 then (some (some 1), 1) else (none, 0) } else if q = stZeros then if b == 0 then { consume stZeros with workActions := fun i ↦ (none, if i = 1 then 1 else 0) } else { consume stSizeCheck with workActions := fun i ↦ if i = 2 then (some (some 1), 1) else (none, 0) } else if q = stSizeBit then { consume stSizeCheck with workActions := fun i ↦ if i = 1 then (none, -1) else if i = 2 then (some (some b), 1) else (none, 0) } else if q = stLengthBit then { consume (stDecrement false) with workActions := fun i ↦ if i = 3 then (some (some b), 1) else (none, 0) } else if q = stPayloadBit then consume (stDecrement true) else consume stDead

The four-work-tape recognizer for delta-length-prefixed bitstring leaves.

def machine : MultiTapeTM 4 (Fin 3) Control where q₀ := stInit tr q input work := if q = stInit then { jump stTree with workActions := fun i ↦ (some (some 2), if i = 1 then 0 else 1) } else if q = stSizeCheck then jump (if work 1 == some 2 then stDecrement false else stSizeBit) else if q = stDecrement false then counterAction false none (-1) (stBorrow false false) else if q = stDecrement true then counterAction true none (-1) (stBorrow true false) else if q = stBorrow false false then borrow false false work else if q = stBorrow false true then borrow false true work else if q = stBorrow true false then borrow true false work else if q = stBorrow true true then borrow true true work else if q = stLeft false false then sweepLeft false false work else if q = stLeft false true then sweepLeft false true work else if q = stLeft true false then sweepLeft true false work else if q = stLeft true true then sweepLeft true true work else if q = stRight false false then sweepRight false false work else if q = stRight false true then sweepRight false true work else if q = stRight true false then sweepRight true false work else if q = stRight true true then sweepRight true true work else if q = stClear then clear work else if q = stLeaf then jump (if work 0 == some 2 then stDone else stTree) else match input with | none => finish (q == stDone) | some b => read q b

Both counter-entry states resolve without inspecting input.

theorem tr_decrement (value : Bool) (input : Option (Fin 3)) (work : Fin 4 → Option (Fin 3)) : machine.tr (stDecrement value) input work = counterAction value none (-1) (stBorrow value false) := value:Boolinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stDecrement value) input work = counterAction value none (-1) (stBorrow value false) input:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stDecrement false) input work = counterAction false none (-1) (stBorrow false false)input:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stDecrement true) input work = counterAction true none (-1) (stBorrow true false) input:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stDecrement false) input work = counterAction false none (-1) (stBorrow false false)input:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stDecrement true) input work = counterAction true none (-1) (stBorrow true false) All goals completed! 🐙

Borrow-state resolution exposes only the selected counter's current digit.

theorem tr_borrow (value seen : Bool) (input : Option (Fin 3)) (work : Fin 4 → Option (Fin 3)) : machine.tr (stBorrow value seen) input work = borrow value seen work := value:Boolseen:Boolinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stBorrow value seen) input work = borrow value seen work seen:Boolinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stBorrow false seen) input work = borrow false seen workseen:Boolinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stBorrow true seen) input work = borrow true seen work seen:Boolinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stBorrow false seen) input work = borrow false seen workseen:Boolinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stBorrow true seen) input work = borrow true seen work input:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stBorrow true false) input work = borrow true false workinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stBorrow true true) input work = borrow true true work input:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stBorrow false false) input work = borrow false false workinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stBorrow false true) input work = borrow false true workinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stBorrow true false) input work = borrow true false workinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stBorrow true true) input work = borrow true true work All goals completed! 🐙

Left-sweep states preserve their two finite-control parameters.

theorem tr_left (value seen : Bool) (input : Option (Fin 3)) (work : Fin 4 → Option (Fin 3)) : machine.tr (stLeft value seen) input work = sweepLeft value seen work := value:Boolseen:Boolinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stLeft value seen) input work = sweepLeft value seen work seen:Boolinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stLeft false seen) input work = sweepLeft false seen workseen:Boolinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stLeft true seen) input work = sweepLeft true seen work seen:Boolinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stLeft false seen) input work = sweepLeft false seen workseen:Boolinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stLeft true seen) input work = sweepLeft true seen work input:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stLeft true false) input work = sweepLeft true false workinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stLeft true true) input work = sweepLeft true true work input:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stLeft false false) input work = sweepLeft false false workinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stLeft false true) input work = sweepLeft false true workinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stLeft true false) input work = sweepLeft true false workinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stLeft true true) input work = sweepLeft true true work All goals completed! 🐙

Right-sweep states preserve their two finite-control parameters.

theorem tr_right (value seen : Bool) (input : Option (Fin 3)) (work : Fin 4 → Option (Fin 3)) : machine.tr (stRight value seen) input work = sweepRight value seen work := value:Boolseen:Boolinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stRight value seen) input work = sweepRight value seen work seen:Boolinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stRight false seen) input work = sweepRight false seen workseen:Boolinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stRight true seen) input work = sweepRight true seen work seen:Boolinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stRight false seen) input work = sweepRight false seen workseen:Boolinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stRight true seen) input work = sweepRight true seen work input:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stRight true false) input work = sweepRight true false workinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stRight true true) input work = sweepRight true true work input:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stRight false false) input work = sweepRight false false workinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stRight false true) input work = sweepRight false true workinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stRight true false) input work = sweepRight true false workinput:Option (Fin 3)work:Fin 4 → Option (Fin 3)⊢ machine.tr (stRight true true) input work = sweepRight true true work All goals completed! 🐙

Reading states resolve directly to the external-bit transition table.

theorem tr_read (q : Control) (b : Fin 3) (work : Fin 4 → Option (Fin 3)) (hq : q = stTree ∨ q = stZeros ∨ q = stSizeBit ∨ q = stLengthBit ∨ q = stPayloadBit ∨ q = stDone ∨ q = stDead) : machine.tr q (some b) work = read q b := q:Controlb:Fin 3work:Fin 4 → Option (Fin 3)hq:q = stTree ∨ q = stZeros ∨ q = stSizeBit ∨ q = stLengthBit ∨ q = stPayloadBit ∨ q = stDone ∨ q = stDead⊢ machine.tr q (some b) work = read q b b:Fin 3work:Fin 4 → Option (Fin 3)⊢ machine.tr stTree (some b) work = read stTree bb:Fin 3work:Fin 4 → Option (Fin 3)⊢ machine.tr stZeros (some b) work = read stZeros bb:Fin 3work:Fin 4 → Option (Fin 3)⊢ machine.tr stSizeBit (some b) work = read stSizeBit bb:Fin 3work:Fin 4 → Option (Fin 3)⊢ machine.tr stLengthBit (some b) work = read stLengthBit bb:Fin 3work:Fin 4 → Option (Fin 3)⊢ machine.tr stPayloadBit (some b) work = read stPayloadBit bb:Fin 3work:Fin 4 → Option (Fin 3)⊢ machine.tr stDone (some b) work = read stDone bb:Fin 3work:Fin 4 → Option (Fin 3)⊢ machine.tr stDead (some b) work = read stDead b b:Fin 3work:Fin 4 → Option (Fin 3)⊢ machine.tr stTree (some b) work = read stTree bb:Fin 3work:Fin 4 → Option (Fin 3)⊢ machine.tr stZeros (some b) work = read stZeros bb:Fin 3work:Fin 4 → Option (Fin 3)⊢ machine.tr stSizeBit (some b) work = read stSizeBit bb:Fin 3work:Fin 4 → Option (Fin 3)⊢ machine.tr stLengthBit (some b) work = read stLengthBit bb:Fin 3work:Fin 4 → Option (Fin 3)⊢ machine.tr stPayloadBit (some b) work = read stPayloadBit bb:Fin 3work:Fin 4 → Option (Fin 3)⊢ machine.tr stDone (some b) work = read stDone bb:Fin 3work:Fin 4 → Option (Fin 3)⊢ machine.tr stDead (some b) work = read stDead b All goals completed! 🐙

An external reading state emits the end-of-input verdict and halts.

theorem tr_end (q : Control) (work : Fin 4 → Option (Fin 3)) (hq : q = stTree ∨ q = stZeros ∨ q = stSizeBit ∨ q = stLengthBit ∨ q = stPayloadBit ∨ q = stDone ∨ q = stDead) : machine.tr q none work = finish (q == stDone) := q:Controlwork:Fin 4 → Option (Fin 3)hq:q = stTree ∨ q = stZeros ∨ q = stSizeBit ∨ q = stLengthBit ∨ q = stPayloadBit ∨ q = stDone ∨ q = stDead⊢ machine.tr q none work = finish (q == stDone) work:Fin 4 → Option (Fin 3)⊢ machine.tr stTree none work = finish (stTree == stDone)work:Fin 4 → Option (Fin 3)⊢ machine.tr stZeros none work = finish (stZeros == stDone)work:Fin 4 → Option (Fin 3)⊢ machine.tr stSizeBit none work = finish (stSizeBit == stDone)work:Fin 4 → Option (Fin 3)⊢ machine.tr stLengthBit none work = finish (stLengthBit == stDone)work:Fin 4 → Option (Fin 3)⊢ machine.tr stPayloadBit none work = finish (stPayloadBit == stDone)work:Fin 4 → Option (Fin 3)⊢ machine.tr stDone none work = finish (stDone == stDone)work:Fin 4 → Option (Fin 3)⊢ machine.tr stDead none work = finish (stDead == stDone) work:Fin 4 → Option (Fin 3)⊢ machine.tr stTree none work = finish (stTree == stDone)work:Fin 4 → Option (Fin 3)⊢ machine.tr stZeros none work = finish (stZeros == stDone)work:Fin 4 → Option (Fin 3)⊢ machine.tr stSizeBit none work = finish (stSizeBit == stDone)work:Fin 4 → Option (Fin 3)⊢ machine.tr stLengthBit none work = finish (stLengthBit == stDone)work:Fin 4 → Option (Fin 3)⊢ machine.tr stPayloadBit none work = finish (stPayloadBit == stDone)work:Fin 4 → Option (Fin 3)⊢ machine.tr stDone none work = finish (stDone == stDone)work:Fin 4 → Option (Fin 3)⊢ machine.tr stDead none work = finish (stDead == stDone) All goals completed! 🐙

Every external-bit transition advances the input head exactly once.

theorem read_inputMove (q : Control) (b : Fin 3) : (read q b).inputMove = 1 := q:Controlb:Fin 3⊢ (read q b).inputMove = 1 q:Controlb:Fin 3⊢ (if q = stTree then if (b == 1) = true then { inputMove := (consume stTree).inputMove, workActions := fun i ↦ (none, if i = 0 then 1 else 0), outS := (consume stTree).outS, q' := (consume stTree).q' } else { inputMove := (consume stZeros).inputMove, workActions := fun i ↦ if i = 3 then (some (some 1), 1) else (none, 0), outS := (consume stZeros).outS, q' := (consume stZeros).q' } else if q = stZeros then if (b == 0) = true then { inputMove := (consume stZeros).inputMove, workActions := fun i ↦ (none, if i = 1 then 1 else 0), outS := (consume stZeros).outS, q' := (consume stZeros).q' } else { inputMove := (consume stSizeCheck).inputMove, workActions := fun i ↦ if i = 2 then (some (some 1), 1) else (none, 0), outS := (consume stSizeCheck).outS, q' := (consume stSizeCheck).q' } else if q = stSizeBit then { inputMove := (consume stSizeCheck).inputMove, workActions := fun i ↦ if i = 1 then (none, -1) else if i = 2 then (some (some b), 1) else (none, 0), outS := (consume stSizeCheck).outS, q' := (consume stSizeCheck).q' } else if q = stLengthBit then { inputMove := (consume (stDecrement false)).inputMove, workActions := fun i ↦ if i = 3 then (some (some b), 1) else (none, 0), outS := (consume (stDecrement false)).outS, q' := (consume (stDecrement false)).q' } else if q = stPayloadBit then consume (stDecrement true) else consume stDead).inputMove = 1 q:Controlb:Fin 3h✝¹:q = stTreeh✝:(b == 1) = true⊢ { inputMove := (consume stTree).inputMove, workActions := fun i ↦ (none, if i = 0 then 1 else 0), outS := (consume stTree).outS, q' := (consume stTree).q' }.inputMove = 1q:Controlb:Fin 3h✝¹:q = stTreeh✝:¬(b == 1) = true⊢ { inputMove := (consume stZeros).inputMove, workActions := fun i ↦ if i = 3 then (some (some 1), 1) else (none, 0), outS := (consume stZeros).outS, q' := (consume stZeros).q' }.inputMove = 1q:Controlb:Fin 3h✝²:¬q = stTreeh✝¹:q = stZerosh✝:(b == 0) = true⊢ { inputMove := (consume stZeros).inputMove, workActions := fun i ↦ (none, if i = 1 then 1 else 0), outS := (consume stZeros).outS, q' := (consume stZeros).q' }.inputMove = 1q:Controlb:Fin 3h✝²:¬q = stTreeh✝¹:q = stZerosh✝:¬(b == 0) = true⊢ { inputMove := (consume stSizeCheck).inputMove, workActions := fun i ↦ if i = 2 then (some (some 1), 1) else (none, 0), outS := (consume stSizeCheck).outS, q' := (consume stSizeCheck).q' }.inputMove = 1q:Controlb:Fin 3h✝²:¬q = stTreeh✝¹:¬q = stZerosh✝:q = stSizeBit⊢ { inputMove := (consume stSizeCheck).inputMove, workActions := fun i ↦ if i = 1 then (none, -1) else if i = 2 then (some (some b), 1) else (none, 0), outS := (consume stSizeCheck).outS, q' := (consume stSizeCheck).q' }.inputMove = 1q:Controlb:Fin 3h✝³:¬q = stTreeh✝²:¬q = stZerosh✝¹:¬q = stSizeBith✝:q = stLengthBit⊢ { inputMove := (consume (stDecrement false)).inputMove, workActions := fun i ↦ if i = 3 then (some (some b), 1) else (none, 0), outS := (consume (stDecrement false)).outS, q' := (consume (stDecrement false)).q' }.inputMove = 1q:Controlb:Fin 3h✝⁴:¬q = stTreeh✝³:¬q = stZerosh✝²:¬q = stSizeBith✝¹:¬q = stLengthBith✝:q = stPayloadBit⊢ (consume (stDecrement true)).inputMove = 1q:Controlb:Fin 3h✝⁴:¬q = stTreeh✝³:¬q = stZerosh✝²:¬q = stSizeBith✝¹:¬q = stLengthBith✝:¬q = stPayloadBit⊢ (consume stDead).inputMove = 1 q:Controlb:Fin 3h✝¹:q = stTreeh✝:(b == 1) = true⊢ { inputMove := (consume stTree).inputMove, workActions := fun i ↦ (none, if i = 0 then 1 else 0), outS := (consume stTree).outS, q' := (consume stTree).q' }.inputMove = 1q:Controlb:Fin 3h✝¹:q = stTreeh✝:¬(b == 1) = true⊢ { inputMove := (consume stZeros).inputMove, workActions := fun i ↦ if i = 3 then (some (some 1), 1) else (none, 0), outS := (consume stZeros).outS, q' := (consume stZeros).q' }.inputMove = 1q:Controlb:Fin 3h✝²:¬q = stTreeh✝¹:q = stZerosh✝:(b == 0) = true⊢ { inputMove := (consume stZeros).inputMove, workActions := fun i ↦ (none, if i = 1 then 1 else 0), outS := (consume stZeros).outS, q' := (consume stZeros).q' }.inputMove = 1q:Controlb:Fin 3h✝²:¬q = stTreeh✝¹:q = stZerosh✝:¬(b == 0) = true⊢ { inputMove := (consume stSizeCheck).inputMove, workActions := fun i ↦ if i = 2 then (some (some 1), 1) else (none, 0), outS := (consume stSizeCheck).outS, q' := (consume stSizeCheck).q' }.inputMove = 1q:Controlb:Fin 3h✝²:¬q = stTreeh✝¹:¬q = stZerosh✝:q = stSizeBit⊢ { inputMove := (consume stSizeCheck).inputMove, workActions := fun i ↦ if i = 1 then (none, -1) else if i = 2 then (some (some b), 1) else (none, 0), outS := (consume stSizeCheck).outS, q' := (consume stSizeCheck).q' }.inputMove = 1q:Controlb:Fin 3h✝³:¬q = stTreeh✝²:¬q = stZerosh✝¹:¬q = stSizeBith✝:q = stLengthBit⊢ { inputMove := (consume (stDecrement false)).inputMove, workActions := fun i ↦ if i = 3 then (some (some b), 1) else (none, 0), outS := (consume (stDecrement false)).outS, q' := (consume (stDecrement false)).q' }.inputMove = 1q:Controlb:Fin 3h✝⁴:¬q = stTreeh✝³:¬q = stZerosh✝²:¬q = stSizeBith✝¹:¬q = stLengthBith✝:q = stPayloadBit⊢ (consume (stDecrement true)).inputMove = 1q:Controlb:Fin 3h✝⁴:¬q = stTreeh✝³:¬q = stZerosh✝²:¬q = stSizeBith✝¹:¬q = stLengthBith✝:¬q = stPayloadBit⊢ (consume stDead).inputMove = 1 All goals completed! 🐙

No external-bit transition emits output.

theorem read_outS (q : Control) (b : Fin 3) : (read q b).outS = none := q:Controlb:Fin 3⊢ (read q b).outS = none q:Controlb:Fin 3⊢ (if q = stTree then if (b == 1) = true then { inputMove := (consume stTree).inputMove, workActions := fun i ↦ (none, if i = 0 then 1 else 0), outS := (consume stTree).outS, q' := (consume stTree).q' } else { inputMove := (consume stZeros).inputMove, workActions := fun i ↦ if i = 3 then (some (some 1), 1) else (none, 0), outS := (consume stZeros).outS, q' := (consume stZeros).q' } else if q = stZeros then if (b == 0) = true then { inputMove := (consume stZeros).inputMove, workActions := fun i ↦ (none, if i = 1 then 1 else 0), outS := (consume stZeros).outS, q' := (consume stZeros).q' } else { inputMove := (consume stSizeCheck).inputMove, workActions := fun i ↦ if i = 2 then (some (some 1), 1) else (none, 0), outS := (consume stSizeCheck).outS, q' := (consume stSizeCheck).q' } else if q = stSizeBit then { inputMove := (consume stSizeCheck).inputMove, workActions := fun i ↦ if i = 1 then (none, -1) else if i = 2 then (some (some b), 1) else (none, 0), outS := (consume stSizeCheck).outS, q' := (consume stSizeCheck).q' } else if q = stLengthBit then { inputMove := (consume (stDecrement false)).inputMove, workActions := fun i ↦ if i = 3 then (some (some b), 1) else (none, 0), outS := (consume (stDecrement false)).outS, q' := (consume (stDecrement false)).q' } else if q = stPayloadBit then consume (stDecrement true) else consume stDead).outS = none q:Controlb:Fin 3h✝¹:q = stTreeh✝:(b == 1) = true⊢ { inputMove := (consume stTree).inputMove, workActions := fun i ↦ (none, if i = 0 then 1 else 0), outS := (consume stTree).outS, q' := (consume stTree).q' }.outS = noneq:Controlb:Fin 3h✝¹:q = stTreeh✝:¬(b == 1) = true⊢ { inputMove := (consume stZeros).inputMove, workActions := fun i ↦ if i = 3 then (some (some 1), 1) else (none, 0), outS := (consume stZeros).outS, q' := (consume stZeros).q' }.outS = noneq:Controlb:Fin 3h✝²:¬q = stTreeh✝¹:q = stZerosh✝:(b == 0) = true⊢ { inputMove := (consume stZeros).inputMove, workActions := fun i ↦ (none, if i = 1 then 1 else 0), outS := (consume stZeros).outS, q' := (consume stZeros).q' }.outS = noneq:Controlb:Fin 3h✝²:¬q = stTreeh✝¹:q = stZerosh✝:¬(b == 0) = true⊢ { inputMove := (consume stSizeCheck).inputMove, workActions := fun i ↦ if i = 2 then (some (some 1), 1) else (none, 0), outS := (consume stSizeCheck).outS, q' := (consume stSizeCheck).q' }.outS = noneq:Controlb:Fin 3h✝²:¬q = stTreeh✝¹:¬q = stZerosh✝:q = stSizeBit⊢ { inputMove := (consume stSizeCheck).inputMove, workActions := fun i ↦ if i = 1 then (none, -1) else if i = 2 then (some (some b), 1) else (none, 0), outS := (consume stSizeCheck).outS, q' := (consume stSizeCheck).q' }.outS = noneq:Controlb:Fin 3h✝³:¬q = stTreeh✝²:¬q = stZerosh✝¹:¬q = stSizeBith✝:q = stLengthBit⊢ { inputMove := (consume (stDecrement false)).inputMove, workActions := fun i ↦ if i = 3 then (some (some b), 1) else (none, 0), outS := (consume (stDecrement false)).outS, q' := (consume (stDecrement false)).q' }.outS = noneq:Controlb:Fin 3h✝⁴:¬q = stTreeh✝³:¬q = stZerosh✝²:¬q = stSizeBith✝¹:¬q = stLengthBith✝:q = stPayloadBit⊢ (consume (stDecrement true)).outS = noneq:Controlb:Fin 3h✝⁴:¬q = stTreeh✝³:¬q = stZerosh✝²:¬q = stSizeBith✝¹:¬q = stLengthBith✝:¬q = stPayloadBit⊢ (consume stDead).outS = none q:Controlb:Fin 3h✝¹:q = stTreeh✝:(b == 1) = true⊢ { inputMove := (consume stTree).inputMove, workActions := fun i ↦ (none, if i = 0 then 1 else 0), outS := (consume stTree).outS, q' := (consume stTree).q' }.outS = noneq:Controlb:Fin 3h✝¹:q = stTreeh✝:¬(b == 1) = true⊢ { inputMove := (consume stZeros).inputMove, workActions := fun i ↦ if i = 3 then (some (some 1), 1) else (none, 0), outS := (consume stZeros).outS, q' := (consume stZeros).q' }.outS = noneq:Controlb:Fin 3h✝²:¬q = stTreeh✝¹:q = stZerosh✝:(b == 0) = true⊢ { inputMove := (consume stZeros).inputMove, workActions := fun i ↦ (none, if i = 1 then 1 else 0), outS := (consume stZeros).outS, q' := (consume stZeros).q' }.outS = noneq:Controlb:Fin 3h✝²:¬q = stTreeh✝¹:q = stZerosh✝:¬(b == 0) = true⊢ { inputMove := (consume stSizeCheck).inputMove, workActions := fun i ↦ if i = 2 then (some (some 1), 1) else (none, 0), outS := (consume stSizeCheck).outS, q' := (consume stSizeCheck).q' }.outS = noneq:Controlb:Fin 3h✝²:¬q = stTreeh✝¹:¬q = stZerosh✝:q = stSizeBit⊢ { inputMove := (consume stSizeCheck).inputMove, workActions := fun i ↦ if i = 1 then (none, -1) else if i = 2 then (some (some b), 1) else (none, 0), outS := (consume stSizeCheck).outS, q' := (consume stSizeCheck).q' }.outS = noneq:Controlb:Fin 3h✝³:¬q = stTreeh✝²:¬q = stZerosh✝¹:¬q = stSizeBith✝:q = stLengthBit⊢ { inputMove := (consume (stDecrement false)).inputMove, workActions := fun i ↦ if i = 3 then (some (some b), 1) else (none, 0), outS := (consume (stDecrement false)).outS, q' := (consume (stDecrement false)).q' }.outS = noneq:Controlb:Fin 3h✝⁴:¬q = stTreeh✝³:¬q = stZerosh✝²:¬q = stSizeBith✝¹:¬q = stLengthBith✝:q = stPayloadBit⊢ (consume (stDecrement true)).outS = noneq:Controlb:Fin 3h✝⁴:¬q = stTreeh✝³:¬q = stZerosh✝²:¬q = stSizeBith✝¹:¬q = stLengthBith✝:¬q = stPayloadBit⊢ (consume stDead).outS = none All goals completed! 🐙

Store a least-significant-first list as a marked most-significant-first tape.

def wordTape (bs : List Bool) (z : ℤ) : Option (Fin 3) := if z = 0 then some 2 else if 0 < z then (bs.reverse[z.toNat - 1]?).map boolEmb else none

Change the selected countdown's contents, head, and control while retaining the context.

def counterCfg {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) (value : Bool) (bs : List Bool) (q : Control) (p : ℕ) : Cfg 4 (Fin 3) Control input where state := some q inputPos := cfg.inputPos workTapes i := if i = counterTape value then wordTape bs else cfg.workTapes i workTapePos i := if i = counterTape value then p else cfg.workTapePos i

The origin marker does not depend on the stored binary word.

theorem wordTape_zero (bs : List Bool) : wordTape bs 0 = some 2 := rfl

A positive tape position reads the corresponding most-significant-first digit.

theorem wordTape_succ (bs : List Bool) (j : ℕ) : wordTape bs (j + 1 : ℕ) = (bs.reverse[j]?).map boolEmb := bs:List Boolj:ℕ⊢ wordTape bs ↑(j + 1) = Option.map (⇑boolEmb) bs.reverse[j]? bs:List Boolj:ℕ⊢ (if ↑(j + 1) = 0 then some 2 else if 0 < ↑(j + 1) then Option.map (⇑boolEmb) bs.reverse[(↑(j + 1)).toNat - 1]? else none) = Option.map (⇑boolEmb) bs.reverse[j]? bs:List Boolj:ℕhz:↑(j + 1) ≠ 0⊢ (if ↑(j + 1) = 0 then some 2 else if 0 < ↑(j + 1) then Option.map (⇑boolEmb) bs.reverse[(↑(j + 1)).toNat - 1]? else none) = Option.map (⇑boolEmb) bs.reverse[j]? bs:List Boolj:ℕhz:↑(j + 1) ≠ 0hp:0 < ↑(j + 1)⊢ (if ↑(j + 1) = 0 then some 2 else if 0 < ↑(j + 1) then Option.map (⇑boolEmb) bs.reverse[(↑(j + 1)).toNat - 1]? else none) = Option.map (⇑boolEmb) bs.reverse[j]? bs:List Boolj:ℕhz:↑(j + 1) ≠ 0hp:0 < ↑(j + 1)⊢ Option.map (⇑boolEmb) bs.reverse[(↑(j + 1)).toNat - 1]? = Option.map (⇑boolEmb) bs.reverse[j]? All goals completed! 🐙

Immediately after the stored word the tape is blank.

theorem wordTape_end (bs : List Bool) : wordTape bs (bs.length + 1 : ℕ) = none := bs:List Bool⊢ wordTape bs ↑(bs.length + 1) = none bs:List Bool⊢ Option.map (⇑boolEmb) none = none All goals completed! 🐙

All work heads are confined to a common nonnegative interval.

def HeadBound {input : List (Fin 3)} (width : ℕ) (cfg : Cfg 4 (Fin 3) Control input) : Prop := ∀ i, 0 ≤ cfg.workTapePos i ∧ cfg.workTapePos i ≤ width
end Geb.BitTree.Elias.Machine