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.Elias.Machine
public import Mathlib.Logic.Function.Basic

set_option doc.verso true

Configurations at delta-decoder phase boundaries

The binary fields are finite words with fixed marked origins. During cleanup a field is truncated at the head position; this gives an explicit description of every intermediate configuration, including when the shorter field has already been erased.

Main definitions

prefixTape restricts a binary field to a most-significant prefix.
clearingCfg describes the simultaneous erasure of two binary fields.
clearedCfg describes the state after both fields are erased.

Tags

Elias delta code, Turing machine, configuration

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

Reading a split binary word selects its displayed middle digit.

theorem wordTape_split (lower higher : List Bool) (b : Bool) :
    wordTape (lower ++ b :: higher) (higher.length + 1 : ℕ) = some (boolEmb b) := bylower:List Boolhigher:List Boolb:Bool⊢ wordTape (lower ++ b :: higher) ↑(higher.length + 1) = some (boolEmb b)
  rw [wordTape_succ,lower:List Boolhigher:List Boolb:Bool⊢ Option.map (⇑boolEmb) (lower ++ b :: higher).reverse[higher.length]? = some (boolEmb b) List.reverse_append,lower:List Boolhigher:List Boolb:Bool⊢ Option.map (⇑boolEmb) ((b :: higher).reverse ++ lower.reverse)[higher.length]? = some (boolEmb b) List.reverse_cons,lower:List Boolhigher:List Boolb:Bool⊢ Option.map (⇑boolEmb) (higher.reverse ++ [b] ++ lower.reverse)[higher.length]? = some (boolEmb b) List.append_assoclower:List Boolhigher:List Boolb:Bool⊢ Option.map (⇑boolEmb) (higher.reverse ++ ([b] ++ lower.reverse))[higher.length]? = some (boolEmb b)]lower:List Boolhigher:List Boolb:Bool⊢ Option.map (⇑boolEmb) (higher.reverse ++ ([b] ++ lower.reverse))[higher.length]? = some (boolEmb b)
  rw [List.getElem?_append_right (bylower:List Boolhigher:List Boolb:Bool⊢ higher.reverse.length ≤ higher.length rw [List.length_reverselower:List Boolhigher:List Boolb:Bool⊢ higher.length ≤ higher.length]All goals completed! 🐙)]lower:List Boolhigher:List Boolb:Bool⊢ Option.map (⇑boolEmb) ([b] ++ lower.reverse)[higher.length - higher.reverse.length]? = some (boolEmb b)
  rw [List.length_reverse,lower:List Boolhigher:List Boolb:Bool⊢ Option.map (⇑boolEmb) ([b] ++ lower.reverse)[higher.length - higher.length]? = some (boolEmb b) Nat.sub_selflower:List Boolhigher:List Boolb:Bool⊢ Option.map (⇑boolEmb) ([b] ++ lower.reverse)[0]? = some (boolEmb b)]lower:List Boolhigher:List Boolb:Bool⊢ Option.map (⇑boolEmb) ([b] ++ lower.reverse)[0]? = some (boolEmb b)
  rflAll goals completed! 🐙

Updating an existing most-significant-first digit updates precisely its tape cell.

theorem wordTape_update (xs : List Bool) (p : ℕ) (b : Bool) (hp : p < xs.length) :
    Function.update (wordTape xs.reverse) (p + 1 : ℕ) (some (boolEmb b)) =
      wordTape (xs.set p b).reverse := byxs:List Boolp:ℕb:Boolhp:p < xs.length⊢ Function.update (wordTape xs.reverse) (↑(p + 1)) (some (boolEmb b)) = wordTape (xs.set p b).reverse
  funext zxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤ⊢ Function.update (wordTape xs.reverse) (↑(p + 1)) (some (boolEmb b)) z = wordTape (xs.set p b).reverse z
  by_cases he : z = (p + 1 : ℕ)posxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:z = ↑(p + 1)⊢ Function.update (wordTape xs.reverse) (↑(p + 1)) (some (boolEmb b)) z = wordTape (xs.set p b).reverse znegxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)⊢ Function.update (wordTape xs.reverse) (↑(p + 1)) (some (boolEmb b)) z = wordTape (xs.set p b).reverse z
  ·posxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:z = ↑(p + 1)⊢ Function.update (wordTape xs.reverse) (↑(p + 1)) (some (boolEmb b)) z = wordTape (xs.set p b).reverse z subst zposxs:List Boolp:ℕb:Boolhp:p < xs.length⊢ Function.update (wordTape xs.reverse) (↑(p + 1)) (some (boolEmb b)) ↑(p + 1) = wordTape (xs.set p b).reverse ↑(p + 1)
    rw [Function.update_self,posxs:List Boolp:ℕb:Boolhp:p < xs.length⊢ some (boolEmb b) = wordTape (xs.set p b).reverse ↑(p + 1) wordTape_succ,posxs:List Boolp:ℕb:Boolhp:p < xs.length⊢ some (boolEmb b) = Option.map (⇑boolEmb) (xs.set p b).reverse.reverse[p]? List.reverse_reverse,posxs:List Boolp:ℕb:Boolhp:p < xs.length⊢ some (boolEmb b) = Option.map (⇑boolEmb) (xs.set p b)[p]?
      List.getElem?_set_self hpposxs:List Boolp:ℕb:Boolhp:p < xs.length⊢ some (boolEmb b) = Option.map (⇑boolEmb) (some b)]posxs:List Boolp:ℕb:Boolhp:p < xs.length⊢ some (boolEmb b) = Option.map (⇑boolEmb) (some b)
    rflAll goals completed! 🐙
  ·negxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)⊢ Function.update (wordTape xs.reverse) (↑(p + 1)) (some (boolEmb b)) z = wordTape (xs.set p b).reverse z rw [Function.update_of_ne henegxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)⊢ wordTape xs.reverse z = wordTape (xs.set p b).reverse z]negxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)⊢ wordTape xs.reverse z = wordTape (xs.set p b).reverse z
    unfold wordTapenegxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)⊢ (if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) xs.reverse.reverse[z.toNat - 1]? else none) =
  if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) (xs.set p b).reverse.reverse[z.toNat - 1]? else none
    by_cases hz : z = 0posxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)hz:z = 0⊢ (if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) xs.reverse.reverse[z.toNat - 1]? else none) =
  if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) (xs.set p b).reverse.reverse[z.toNat - 1]? else nonenegxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0⊢ (if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) xs.reverse.reverse[z.toNat - 1]? else none) =
  if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) (xs.set p b).reverse.reverse[z.toNat - 1]? else none
    ·posxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)hz:z = 0⊢ (if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) xs.reverse.reverse[z.toNat - 1]? else none) =
  if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) (xs.set p b).reverse.reverse[z.toNat - 1]? else none rw [ite_eq_left hz,posxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)hz:z = 0⊢ some 2 =
  if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) (xs.set p b).reverse.reverse[z.toNat - 1]? else none ite_eq_left hzposxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)hz:z = 0⊢ some 2 = some 2]All goals completed! 🐙
    ·negxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0⊢ (if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) xs.reverse.reverse[z.toNat - 1]? else none) =
  if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) (xs.set p b).reverse.reverse[z.toNat - 1]? else none rw [ite_eq_right hz,negxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0⊢ (if 0 < z then Option.map (⇑boolEmb) xs.reverse.reverse[z.toNat - 1]? else none) =
  if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) (xs.set p b).reverse.reverse[z.toNat - 1]? else none ite_eq_right hznegxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0⊢ (if 0 < z then Option.map (⇑boolEmb) xs.reverse.reverse[z.toNat - 1]? else none) =
  if 0 < z then Option.map (⇑boolEmb) (xs.set p b).reverse.reverse[z.toNat - 1]? else none]negxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0⊢ (if 0 < z then Option.map (⇑boolEmb) xs.reverse.reverse[z.toNat - 1]? else none) =
  if 0 < z then Option.map (⇑boolEmb) (xs.set p b).reverse.reverse[z.toNat - 1]? else none
      by_cases hzpos : 0 < zposxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hzpos:0 < z⊢ (if 0 < z then Option.map (⇑boolEmb) xs.reverse.reverse[z.toNat - 1]? else none) =
  if 0 < z then Option.map (⇑boolEmb) (xs.set p b).reverse.reverse[z.toNat - 1]? else nonenegxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hzpos:¬0 < z⊢ (if 0 < z then Option.map (⇑boolEmb) xs.reverse.reverse[z.toNat - 1]? else none) =
  if 0 < z then Option.map (⇑boolEmb) (xs.set p b).reverse.reverse[z.toNat - 1]? else none
      ·posxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hzpos:0 < z⊢ (if 0 < z then Option.map (⇑boolEmb) xs.reverse.reverse[z.toNat - 1]? else none) =
  if 0 < z then Option.map (⇑boolEmb) (xs.set p b).reverse.reverse[z.toNat - 1]? else none rw [ite_eq_left hzpos,posxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hzpos:0 < z⊢ Option.map (⇑boolEmb) xs.reverse.reverse[z.toNat - 1]? =
  if 0 < z then Option.map (⇑boolEmb) (xs.set p b).reverse.reverse[z.toNat - 1]? else none ite_eq_left hzpos,posxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hzpos:0 < z⊢ Option.map (⇑boolEmb) xs.reverse.reverse[z.toNat - 1]? =
  Option.map (⇑boolEmb) (xs.set p b).reverse.reverse[z.toNat - 1]? List.reverse_reverse,posxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hzpos:0 < z⊢ Option.map (⇑boolEmb) xs[z.toNat - 1]? = Option.map (⇑boolEmb) (xs.set p b).reverse.reverse[z.toNat - 1]?
          List.reverse_reverse,posxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hzpos:0 < z⊢ Option.map (⇑boolEmb) xs[z.toNat - 1]? = Option.map (⇑boolEmb) (xs.set p b)[z.toNat - 1]? List.getElem?_set_ne (byxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hzpos:0 < z⊢ p ≠ z.toNat - 1 omegaAll goals completed! 🐙)]All goals completed! 🐙
      ·negxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hzpos:¬0 < z⊢ (if 0 < z then Option.map (⇑boolEmb) xs.reverse.reverse[z.toNat - 1]? else none) =
  if 0 < z then Option.map (⇑boolEmb) (xs.set p b).reverse.reverse[z.toNat - 1]? else none rw [ite_eq_right hzpos,negxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hzpos:¬0 < z⊢ none = if 0 < z then Option.map (⇑boolEmb) (xs.set p b).reverse.reverse[z.toNat - 1]? else none ite_eq_right hzposnegxs:List Boolp:ℕb:Boolhp:p < xs.lengthz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hzpos:¬0 < z⊢ none = none]All goals completed! 🐙

Changing the middle digit of a split word writes its one corresponding tape cell.

theorem wordTape_update_split (lower higher : List Bool) (b b' : Bool) :
    Function.update (wordTape (lower ++ b :: higher)) (higher.length + 1 : ℕ)
      (some (boolEmb b')) = wordTape (lower ++ b' :: higher) := bylower:List Boolhigher:List Boolb:Boolb':Bool⊢ Function.update (wordTape (lower ++ b :: higher)) (↑(higher.length + 1)) (some (boolEmb b')) =
  wordTape (lower ++ b' :: higher)
  have h := wordTape_update (higher.reverse ++ b :: lower.reverse) higher.length b'
    (bylower:List Boolhigher:List Boolb:Boolb':Bool⊢ higher.length < (higher.reverse ++ b :: lower.reverse).length rw [List.length_append,lower:List Boolhigher:List Boolb:Boolb':Bool⊢ higher.length < higher.reverse.length + (b :: lower.reverse).length List.length_reverse,lower:List Boolhigher:List Boolb:Boolb':Bool⊢ higher.length < higher.length + (b :: lower.reverse).length List.length_conslower:List Boolhigher:List Boolb:Boolb':Bool⊢ higher.length < higher.length + (lower.reverse.length + 1)]lower:List Boolhigher:List Boolb:Boolb':Bool⊢ higher.length < higher.length + (lower.reverse.length + 1); omegaAll goals completed! 🐙)lower:List Boolhigher:List Boolb:Boolb':Boolh:Function.update (wordTape (higher.reverse ++ b :: lower.reverse).reverse) (↑(higher.length + 1)) (some (boolEmb b')) =
  wordTape ((higher.reverse ++ b :: lower.reverse).set higher.length b').reverse⊢ Function.update (wordTape (lower ++ b :: higher)) (↑(higher.length + 1)) (some (boolEmb b')) =
  wordTape (lower ++ b' :: higher)
  rw [List.set_append_right _ _ (bylower:List Boolhigher:List Boolb:Boolb':Boolh:Function.update (wordTape (higher.reverse ++ b :: lower.reverse).reverse) (↑(higher.length + 1)) (some (boolEmb b')) =
  wordTape ((higher.reverse ++ b :: lower.reverse).set higher.length b').reverse⊢ higher.reverse.length ≤ higher.length rw [List.length_reverselower:List Boolhigher:List Boolb:Boolb':Boolh:Function.update (wordTape (higher.reverse ++ b :: lower.reverse).reverse) (↑(higher.length + 1)) (some (boolEmb b')) =
  wordTape ((higher.reverse ++ b :: lower.reverse).set higher.length b').reverse⊢ higher.length ≤ higher.length]All goals completed! 🐙), List.length_reverse,lower:List Boolhigher:List Boolb:Boolb':Boolh:Function.update (wordTape (higher.reverse ++ b :: lower.reverse).reverse) (↑(higher.length + 1)) (some (boolEmb b')) =
  wordTape (higher.reverse ++ (b :: lower.reverse).set (higher.length - higher.length) b').reverse⊢ Function.update (wordTape (lower ++ b :: higher)) (↑(higher.length + 1)) (some (boolEmb b')) =
  wordTape (lower ++ b' :: higher)
    Nat.sub_self,lower:List Boolhigher:List Boolb:Boolb':Boolh:Function.update (wordTape (higher.reverse ++ b :: lower.reverse).reverse) (↑(higher.length + 1)) (some (boolEmb b')) =
  wordTape (higher.reverse ++ (b :: lower.reverse).set 0 b').reverse⊢ Function.update (wordTape (lower ++ b :: higher)) (↑(higher.length + 1)) (some (boolEmb b')) =
  wordTape (lower ++ b' :: higher) List.set_cons_zerolower:List Boolhigher:List Boolb:Boolb':Boolh:Function.update (wordTape (higher.reverse ++ b :: lower.reverse).reverse) (↑(higher.length + 1)) (some (boolEmb b')) =
  wordTape (higher.reverse ++ b' :: lower.reverse).reverse⊢ Function.update (wordTape (lower ++ b :: higher)) (↑(higher.length + 1)) (some (boolEmb b')) =
  wordTape (lower ++ b' :: higher)] at hlower:List Boolhigher:List Boolb:Boolb':Boolh:Function.update (wordTape (higher.reverse ++ b :: lower.reverse).reverse) (↑(higher.length + 1)) (some (boolEmb b')) =
  wordTape (higher.reverse ++ b' :: lower.reverse).reverse⊢ Function.update (wordTape (lower ++ b :: higher)) (↑(higher.length + 1)) (some (boolEmb b')) =
  wordTape (lower ++ b' :: higher)
  simpa only [List.reverse_append, List.reverse_cons, List.reverse_reverse,
    List.append_assoc, List.singleton_append] using hAll goals completed! 🐙

Appending an input digit writes the blank immediately after the stored field.

theorem wordTape_cons (bs : List Bool) (b : Bool) :
    Function.update (wordTape bs) (bs.length + 1 : ℕ) (some (boolEmb b)) =
      wordTape (b :: bs) := bybs:List Boolb:Bool⊢ Function.update (wordTape bs) (↑(bs.length + 1)) (some (boolEmb b)) = wordTape (b :: bs)
  funext zbs:List Boolb:Boolz:ℤ⊢ Function.update (wordTape bs) (↑(bs.length + 1)) (some (boolEmb b)) z = wordTape (b :: bs) z
  by_cases he : z = (bs.length + 1 : ℕ)posbs:List Boolb:Boolz:ℤhe:z = ↑(bs.length + 1)⊢ Function.update (wordTape bs) (↑(bs.length + 1)) (some (boolEmb b)) z = wordTape (b :: bs) znegbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)⊢ Function.update (wordTape bs) (↑(bs.length + 1)) (some (boolEmb b)) z = wordTape (b :: bs) z
  ·posbs:List Boolb:Boolz:ℤhe:z = ↑(bs.length + 1)⊢ Function.update (wordTape bs) (↑(bs.length + 1)) (some (boolEmb b)) z = wordTape (b :: bs) z subst zposbs:List Boolb:Bool⊢ Function.update (wordTape bs) (↑(bs.length + 1)) (some (boolEmb b)) ↑(bs.length + 1) =
  wordTape (b :: bs) ↑(bs.length + 1)
    rw [Function.update_self,posbs:List Boolb:Bool⊢ some (boolEmb b) = wordTape (b :: bs) ↑(bs.length + 1) wordTape_succ,posbs:List Boolb:Bool⊢ some (boolEmb b) = Option.map (⇑boolEmb) (b :: bs).reverse[bs.length]? List.reverse_cons,posbs:List Boolb:Bool⊢ some (boolEmb b) = Option.map (⇑boolEmb) (bs.reverse ++ [b])[bs.length]?
      List.getElem?_append_right (bybs:List Boolb:Bool⊢ bs.reverse.length ≤ bs.length rw [List.length_reversebs:List Boolb:Bool⊢ bs.length ≤ bs.length]All goals completed! 🐙), List.length_reverse,posbs:List Boolb:Bool⊢ some (boolEmb b) = Option.map ⇑boolEmb [b][bs.length - bs.length]?
      Nat.sub_selfposbs:List Boolb:Bool⊢ some (boolEmb b) = Option.map ⇑boolEmb [b][0]?]posbs:List Boolb:Bool⊢ some (boolEmb b) = Option.map ⇑boolEmb [b][0]?
    rflAll goals completed! 🐙
  ·negbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)⊢ Function.update (wordTape bs) (↑(bs.length + 1)) (some (boolEmb b)) z = wordTape (b :: bs) z rw [Function.update_of_ne henegbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)⊢ wordTape bs z = wordTape (b :: bs) z]negbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)⊢ wordTape bs z = wordTape (b :: bs) z
    unfold wordTapenegbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)⊢ (if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? else none) =
  if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) (b :: bs).reverse[z.toNat - 1]? else none
    by_cases hz : z = 0posbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:z = 0⊢ (if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? else none) =
  if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) (b :: bs).reverse[z.toNat - 1]? else nonenegbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0⊢ (if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? else none) =
  if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) (b :: bs).reverse[z.toNat - 1]? else none
    ·posbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:z = 0⊢ (if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? else none) =
  if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) (b :: bs).reverse[z.toNat - 1]? else none rw [ite_eq_left hz,posbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:z = 0⊢ some 2 = if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) (b :: bs).reverse[z.toNat - 1]? else none ite_eq_left hzposbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:z = 0⊢ some 2 = some 2]All goals completed! 🐙
    ·negbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0⊢ (if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? else none) =
  if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) (b :: bs).reverse[z.toNat - 1]? else none rw [ite_eq_right hz,negbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0⊢ (if 0 < z then Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? else none) =
  if z = 0 then some 2 else if 0 < z then Option.map (⇑boolEmb) (b :: bs).reverse[z.toNat - 1]? else none ite_eq_right hznegbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0⊢ (if 0 < z then Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? else none) =
  if 0 < z then Option.map (⇑boolEmb) (b :: bs).reverse[z.toNat - 1]? else none]negbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0⊢ (if 0 < z then Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? else none) =
  if 0 < z then Option.map (⇑boolEmb) (b :: bs).reverse[z.toNat - 1]? else none
      by_cases hzpos : 0 < zposbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < z⊢ (if 0 < z then Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? else none) =
  if 0 < z then Option.map (⇑boolEmb) (b :: bs).reverse[z.toNat - 1]? else nonenegbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:¬0 < z⊢ (if 0 < z then Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? else none) =
  if 0 < z then Option.map (⇑boolEmb) (b :: bs).reverse[z.toNat - 1]? else none
      ·posbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < z⊢ (if 0 < z then Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? else none) =
  if 0 < z then Option.map (⇑boolEmb) (b :: bs).reverse[z.toNat - 1]? else none rw [ite_eq_left hzpos,posbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < z⊢ Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? =
  if 0 < z then Option.map (⇑boolEmb) (b :: bs).reverse[z.toNat - 1]? else none ite_eq_left hzpos,posbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < z⊢ Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? = Option.map (⇑boolEmb) (b :: bs).reverse[z.toNat - 1]? List.reverse_consposbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < z⊢ Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? = Option.map (⇑boolEmb) (bs.reverse ++ [b])[z.toNat - 1]?]posbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < z⊢ Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? = Option.map (⇑boolEmb) (bs.reverse ++ [b])[z.toNat - 1]?
        by_cases hj : z.toNat - 1 < bs.lengthposbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < zhj:z.toNat - 1 < bs.length⊢ Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? = Option.map (⇑boolEmb) (bs.reverse ++ [b])[z.toNat - 1]?negbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < zhj:¬z.toNat - 1 < bs.length⊢ Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? = Option.map (⇑boolEmb) (bs.reverse ++ [b])[z.toNat - 1]?
        ·posbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < zhj:z.toNat - 1 < bs.length⊢ Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? = Option.map (⇑boolEmb) (bs.reverse ++ [b])[z.toNat - 1]? rw [List.getElem?_append_left (bybs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < zhj:z.toNat - 1 < bs.length⊢ z.toNat - 1 < bs.reverse.length rwa [List.length_reversebs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < zhj:z.toNat - 1 < bs.length⊢ z.toNat - 1 < bs.length]bs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < zhj:z.toNat - 1 < bs.length⊢ z.toNat - 1 < bs.length)]All goals completed! 🐙
        ·negbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < zhj:¬z.toNat - 1 < bs.length⊢ Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? = Option.map (⇑boolEmb) (bs.reverse ++ [b])[z.toNat - 1]? have hne : z.toNat - 1 ≠ bs.length := bybs:List Boolb:Bool⊢ Function.update (wordTape bs) (↑(bs.length + 1)) (some (boolEmb b)) = wordTape (b :: bs) omeganegbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < zhj:¬z.toNat - 1 < bs.lengthhne:z.toNat - 1 ≠ bs.length⊢ Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? = Option.map (⇑boolEmb) (bs.reverse ++ [b])[z.toNat - 1]?
          rw [List.getElem?_eq_none (bybs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < zhj:¬z.toNat - 1 < bs.lengthhne:z.toNat - 1 ≠ bs.length⊢ bs.reverse.length ≤ z.toNat - 1 rw [List.length_reversebs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < zhj:¬z.toNat - 1 < bs.lengthhne:z.toNat - 1 ≠ bs.length⊢ bs.length ≤ z.toNat - 1]bs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < zhj:¬z.toNat - 1 < bs.lengthhne:z.toNat - 1 ≠ bs.length⊢ bs.length ≤ z.toNat - 1; omegaAll goals completed! 🐙),
            List.getElem?_eq_none (bybs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < zhj:¬z.toNat - 1 < bs.lengthhne:z.toNat - 1 ≠ bs.length⊢ (bs.reverse ++ [b]).length ≤ z.toNat - 1
              rw [List.length_append,bs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < zhj:¬z.toNat - 1 < bs.lengthhne:z.toNat - 1 ≠ bs.length⊢ bs.reverse.length + [b].length ≤ z.toNat - 1 List.length_reverse,bs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < zhj:¬z.toNat - 1 < bs.lengthhne:z.toNat - 1 ≠ bs.length⊢ bs.length + [b].length ≤ z.toNat - 1 List.length_singletonbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < zhj:¬z.toNat - 1 < bs.lengthhne:z.toNat - 1 ≠ bs.length⊢ bs.length + 1 ≤ z.toNat - 1]bs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:0 < zhj:¬z.toNat - 1 < bs.lengthhne:z.toNat - 1 ≠ bs.length⊢ bs.length + 1 ≤ z.toNat - 1
              omegaAll goals completed! 🐙)]All goals completed! 🐙
      ·negbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:¬0 < z⊢ (if 0 < z then Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? else none) =
  if 0 < z then Option.map (⇑boolEmb) (b :: bs).reverse[z.toNat - 1]? else none rw [ite_eq_right hzpos,negbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:¬0 < z⊢ none = if 0 < z then Option.map (⇑boolEmb) (b :: bs).reverse[z.toNat - 1]? else none ite_eq_right hzposnegbs:List Boolb:Boolz:ℤhe:¬z = ↑(bs.length + 1)hz:¬z = 0hzpos:¬0 < z⊢ none = none]All goals completed! 🐙

A marked tape containing at most the first p most-significant digits.

def prefixTape (bs : List Bool) (p : ℕ) : ℤ → Option (Fin 3) :=
  wordTape ((bs.reverse.take p).reverse)

A prefix tape always retains its origin marker.

theorem prefixTape_zero (bs : List Bool) (p : ℕ) : prefixTape bs p 0 = some 2 := rfl

Removing all digits leaves only the origin marker.

theorem prefixTape_empty (bs : List Bool) : prefixTape bs 0 = wordTape [] := rfl

Keeping at least the full width retains every digit.

theorem prefixTape_full (bs : List Bool) {p : ℕ} (h : bs.length ≤ p) :
    prefixTape bs p = wordTape bs := bybs:List Boolp:ℕh:bs.length ≤ p⊢ prefixTape bs p = wordTape bs
  unfold prefixTapebs:List Boolp:ℕh:bs.length ≤ p⊢ wordTape (List.take p bs.reverse).reverse = wordTape bs
  rw [List.take_of_length_le (bybs:List Boolp:ℕh:bs.length ≤ p⊢ bs.reverse.length ≤ p rwa [List.length_reversebs:List Boolp:ℕh:bs.length ≤ p⊢ bs.length ≤ p]bs:List Boolp:ℕh:bs.length ≤ p⊢ bs.length ≤ p), List.reverse_reversebs:List Boolp:ℕh:bs.length ≤ p⊢ wordTape bs = wordTape bs]All goals completed! 🐙

The cell erased at a positive position is never an origin marker.

theorem prefixTape_succ_ne_marker (bs : List Bool) (p : ℕ) :
    prefixTape bs (p + 1) (p + 1 : ℕ) ≠ some 2 := bybs:List Boolp:ℕ⊢ prefixTape bs (p + 1) ↑(p + 1) ≠ some 2
  unfold prefixTapebs:List Boolp:ℕ⊢ wordTape (List.take (p + 1) bs.reverse).reverse ↑(p + 1) ≠ some 2
  rw [wordTape_succ,bs:List Boolp:ℕ⊢ Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse).reverse.reverse[p]? ≠ some 2 List.reverse_reversebs:List Boolp:ℕ⊢ Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse)[p]? ≠ some 2]bs:List Boolp:ℕ⊢ Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse)[p]? ≠ some 2
  cases (bs.reverse.take (p + 1))[p]? with
  | none =>nonebs:List Boolp:ℕ⊢ Option.map (⇑boolEmb) none ≠ some 2 exact (bybs:List Boolp:ℕ⊢ Option.map (⇑boolEmb) none ≠ some 2 decideAll goals completed! 🐙)
  | some b =>somebs:List Boolp:ℕb:Bool⊢ Option.map (⇑boolEmb) (some b) ≠ some 2 cases bsome.falsebs:List Boolp:ℕ⊢ Option.map (⇑boolEmb) (some false) ≠ some 2some.truebs:List Boolp:ℕ⊢ Option.map (⇑boolEmb) (some true) ≠ some 2 <;>some.falsebs:List Boolp:ℕ⊢ Option.map (⇑boolEmb) (some false) ≠ some 2some.truebs:List Boolp:ℕ⊢ Option.map (⇑boolEmb) (some true) ≠ some 2 exact (bybs:List Boolp:ℕ⊢ Option.map (⇑boolEmb) (some true) ≠ some 2 decideAll goals completed! 🐙)

The current cell is an origin marker exactly when the head position is zero.

theorem prefixTape_marker (bs : List Bool) (p : ℕ) :
    (prefixTape bs p (p : ℤ) == some 2) = decide (p = 0) := bybs:List Boolp:ℕ⊢ (prefixTape bs p ↑p == some 2) = decide (p = 0)
  cases p with
  | zero =>zerobs:List Bool⊢ (prefixTape bs 0 ↑0 == some 2) = decide (0 = 0) rflAll goals completed! 🐙
  | succ p =>succbs:List Boolp:ℕ⊢ (prefixTape bs (p + 1) ↑(p + 1) == some 2) = decide (p + 1 = 0)
    change (prefixTape bs (p + 1) (p + 1 : ℕ) == some 2) = falsesuccbs:List Boolp:ℕ⊢ (prefixTape bs (p + 1) ↑(p + 1) == some 2) = false
    unfold prefixTapesuccbs:List Boolp:ℕ⊢ (wordTape (List.take (p + 1) bs.reverse).reverse ↑(p + 1) == some 2) = false
    rw [wordTape_succ,succbs:List Boolp:ℕ⊢ (Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse).reverse.reverse[p]? == some 2) = false List.reverse_reversesuccbs:List Boolp:ℕ⊢ (Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse)[p]? == some 2) = false]succbs:List Boolp:ℕ⊢ (Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse)[p]? == some 2) = false
    cases (bs.reverse.take (p + 1))[p]? with
    | none =>succ.nonebs:List Boolp:ℕ⊢ (Option.map (⇑boolEmb) none == some 2) = false rflAll goals completed! 🐙
    | some b =>succ.somebs:List Boolp:ℕb:Bool⊢ (Option.map (⇑boolEmb) (some b) == some 2) = false cases bsucc.some.falsebs:List Boolp:ℕ⊢ (Option.map (⇑boolEmb) (some false) == some 2) = falsesucc.some.truebs:List Boolp:ℕ⊢ (Option.map (⇑boolEmb) (some true) == some 2) = false <;>succ.some.falsebs:List Boolp:ℕ⊢ (Option.map (⇑boolEmb) (some false) == some 2) = falsesucc.some.truebs:List Boolp:ℕ⊢ (Option.map (⇑boolEmb) (some true) == some 2) = false rflAll goals completed! 🐙

Erasing the current positive cell shortens a prefix tape by one position.

theorem prefixTape_erase (bs : List Bool) (p : ℕ) :
    Function.update (prefixTape bs (p + 1)) (p + 1 : ℕ) none = prefixTape bs p := bybs:List Boolp:ℕ⊢ Function.update (prefixTape bs (p + 1)) (↑(p + 1)) none = prefixTape bs p
  funext zbs:List Boolp:ℕz:ℤ⊢ Function.update (prefixTape bs (p + 1)) (↑(p + 1)) none z = prefixTape bs p z
  by_cases he : z = (p + 1 : ℕ)posbs:List Boolp:ℕz:ℤhe:z = ↑(p + 1)⊢ Function.update (prefixTape bs (p + 1)) (↑(p + 1)) none z = prefixTape bs p znegbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)⊢ Function.update (prefixTape bs (p + 1)) (↑(p + 1)) none z = prefixTape bs p z
  ·posbs:List Boolp:ℕz:ℤhe:z = ↑(p + 1)⊢ Function.update (prefixTape bs (p + 1)) (↑(p + 1)) none z = prefixTape bs p z subst zposbs:List Boolp:ℕ⊢ Function.update (prefixTape bs (p + 1)) (↑(p + 1)) none ↑(p + 1) = prefixTape bs p ↑(p + 1)
    rw [Function.update_selfposbs:List Boolp:ℕ⊢ none = prefixTape bs p ↑(p + 1)]posbs:List Boolp:ℕ⊢ none = prefixTape bs p ↑(p + 1)
    unfold prefixTapeposbs:List Boolp:ℕ⊢ none = wordTape (List.take p bs.reverse).reverse ↑(p + 1)
    rw [wordTape_succ,posbs:List Boolp:ℕ⊢ none = Option.map (⇑boolEmb) (List.take p bs.reverse).reverse.reverse[p]? List.reverse_reverse,posbs:List Boolp:ℕ⊢ none = Option.map (⇑boolEmb) (List.take p bs.reverse)[p]?
      List.getElem?_take_eq_none (Nat.le_refl p)posbs:List Boolp:ℕ⊢ none = Option.map (⇑boolEmb) none]posbs:List Boolp:ℕ⊢ none = Option.map (⇑boolEmb) none
    rflAll goals completed! 🐙
  ·negbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)⊢ Function.update (prefixTape bs (p + 1)) (↑(p + 1)) none z = prefixTape bs p z rw [Function.update_of_ne henegbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)⊢ prefixTape bs (p + 1) z = prefixTape bs p z]negbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)⊢ prefixTape bs (p + 1) z = prefixTape bs p z
    unfold prefixTape wordTapenegbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)⊢ (if z = 0 then some 2
  else if 0 < z then Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse).reverse.reverse[z.toNat - 1]? else none) =
  if z = 0 then some 2
  else if 0 < z then Option.map (⇑boolEmb) (List.take p bs.reverse).reverse.reverse[z.toNat - 1]? else none
    by_cases hz : z = 0posbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:z = 0⊢ (if z = 0 then some 2
  else if 0 < z then Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse).reverse.reverse[z.toNat - 1]? else none) =
  if z = 0 then some 2
  else if 0 < z then Option.map (⇑boolEmb) (List.take p bs.reverse).reverse.reverse[z.toNat - 1]? else nonenegbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0⊢ (if z = 0 then some 2
  else if 0 < z then Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse).reverse.reverse[z.toNat - 1]? else none) =
  if z = 0 then some 2
  else if 0 < z then Option.map (⇑boolEmb) (List.take p bs.reverse).reverse.reverse[z.toNat - 1]? else none
    ·posbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:z = 0⊢ (if z = 0 then some 2
  else if 0 < z then Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse).reverse.reverse[z.toNat - 1]? else none) =
  if z = 0 then some 2
  else if 0 < z then Option.map (⇑boolEmb) (List.take p bs.reverse).reverse.reverse[z.toNat - 1]? else none rw [ite_eq_left hz,posbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:z = 0⊢ some 2 =
  if z = 0 then some 2
  else if 0 < z then Option.map (⇑boolEmb) (List.take p bs.reverse).reverse.reverse[z.toNat - 1]? else none ite_eq_left hzposbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:z = 0⊢ some 2 = some 2]All goals completed! 🐙
    ·negbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0⊢ (if z = 0 then some 2
  else if 0 < z then Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse).reverse.reverse[z.toNat - 1]? else none) =
  if z = 0 then some 2
  else if 0 < z then Option.map (⇑boolEmb) (List.take p bs.reverse).reverse.reverse[z.toNat - 1]? else none rw [ite_eq_right hz,negbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0⊢ (if 0 < z then Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse).reverse.reverse[z.toNat - 1]? else none) =
  if z = 0 then some 2
  else if 0 < z then Option.map (⇑boolEmb) (List.take p bs.reverse).reverse.reverse[z.toNat - 1]? else none ite_eq_right hznegbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0⊢ (if 0 < z then Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse).reverse.reverse[z.toNat - 1]? else none) =
  if 0 < z then Option.map (⇑boolEmb) (List.take p bs.reverse).reverse.reverse[z.toNat - 1]? else none]negbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0⊢ (if 0 < z then Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse).reverse.reverse[z.toNat - 1]? else none) =
  if 0 < z then Option.map (⇑boolEmb) (List.take p bs.reverse).reverse.reverse[z.toNat - 1]? else none
      by_cases hp : 0 < zposbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:0 < z⊢ (if 0 < z then Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse).reverse.reverse[z.toNat - 1]? else none) =
  if 0 < z then Option.map (⇑boolEmb) (List.take p bs.reverse).reverse.reverse[z.toNat - 1]? else nonenegbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:¬0 < z⊢ (if 0 < z then Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse).reverse.reverse[z.toNat - 1]? else none) =
  if 0 < z then Option.map (⇑boolEmb) (List.take p bs.reverse).reverse.reverse[z.toNat - 1]? else none
      ·posbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:0 < z⊢ (if 0 < z then Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse).reverse.reverse[z.toNat - 1]? else none) =
  if 0 < z then Option.map (⇑boolEmb) (List.take p bs.reverse).reverse.reverse[z.toNat - 1]? else none rw [ite_eq_left hp,posbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:0 < z⊢ Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse).reverse.reverse[z.toNat - 1]? =
  if 0 < z then Option.map (⇑boolEmb) (List.take p bs.reverse).reverse.reverse[z.toNat - 1]? else none ite_eq_left hp,posbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:0 < z⊢ Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse).reverse.reverse[z.toNat - 1]? =
  Option.map (⇑boolEmb) (List.take p bs.reverse).reverse.reverse[z.toNat - 1]? List.reverse_reverse,posbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:0 < z⊢ Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse)[z.toNat - 1]? =
  Option.map (⇑boolEmb) (List.take p bs.reverse).reverse.reverse[z.toNat - 1]? List.reverse_reverse,posbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:0 < z⊢ Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse)[z.toNat - 1]? =
  Option.map (⇑boolEmb) (List.take p bs.reverse)[z.toNat - 1]?
          List.getElem?_take,posbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:0 < z⊢ Option.map (⇑boolEmb) (if z.toNat - 1 < p + 1 then bs.reverse[z.toNat - 1]? else none) =
  Option.map (⇑boolEmb) (List.take p bs.reverse)[z.toNat - 1]? List.getElem?_takeposbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:0 < z⊢ Option.map (⇑boolEmb) (if z.toNat - 1 < p + 1 then bs.reverse[z.toNat - 1]? else none) =
  Option.map (⇑boolEmb) (if z.toNat - 1 < p then bs.reverse[z.toNat - 1]? else none)]posbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:0 < z⊢ Option.map (⇑boolEmb) (if z.toNat - 1 < p + 1 then bs.reverse[z.toNat - 1]? else none) =
  Option.map (⇑boolEmb) (if z.toNat - 1 < p then bs.reverse[z.toNat - 1]? else none)
        have hn : z.toNat - 1 ≠ p := bybs:List Boolp:ℕ⊢ Function.update (prefixTape bs (p + 1)) (↑(p + 1)) none = prefixTape bs p omegaposbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:0 < zhn:z.toNat - 1 ≠ p⊢ Option.map (⇑boolEmb) (if z.toNat - 1 < p + 1 then bs.reverse[z.toNat - 1]? else none) =
  Option.map (⇑boolEmb) (if z.toNat - 1 < p then bs.reverse[z.toNat - 1]? else none)
        by_cases hj : z.toNat - 1 < pposbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:0 < zhn:z.toNat - 1 ≠ phj:z.toNat - 1 < p⊢ Option.map (⇑boolEmb) (if z.toNat - 1 < p + 1 then bs.reverse[z.toNat - 1]? else none) =
  Option.map (⇑boolEmb) (if z.toNat - 1 < p then bs.reverse[z.toNat - 1]? else none)negbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:0 < zhn:z.toNat - 1 ≠ phj:¬z.toNat - 1 < p⊢ Option.map (⇑boolEmb) (if z.toNat - 1 < p + 1 then bs.reverse[z.toNat - 1]? else none) =
  Option.map (⇑boolEmb) (if z.toNat - 1 < p then bs.reverse[z.toNat - 1]? else none)
        ·posbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:0 < zhn:z.toNat - 1 ≠ phj:z.toNat - 1 < p⊢ Option.map (⇑boolEmb) (if z.toNat - 1 < p + 1 then bs.reverse[z.toNat - 1]? else none) =
  Option.map (⇑boolEmb) (if z.toNat - 1 < p then bs.reverse[z.toNat - 1]? else none) rw [ite_eq_left (bybs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:0 < zhn:z.toNat - 1 ≠ phj:z.toNat - 1 < p⊢ z.toNat - 1 < p + 1 omegaAll goals completed! 🐙), ite_eq_left hjposbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:0 < zhn:z.toNat - 1 ≠ phj:z.toNat - 1 < p⊢ Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]? = Option.map (⇑boolEmb) bs.reverse[z.toNat - 1]?]All goals completed! 🐙
        ·negbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:0 < zhn:z.toNat - 1 ≠ phj:¬z.toNat - 1 < p⊢ Option.map (⇑boolEmb) (if z.toNat - 1 < p + 1 then bs.reverse[z.toNat - 1]? else none) =
  Option.map (⇑boolEmb) (if z.toNat - 1 < p then bs.reverse[z.toNat - 1]? else none) rw [ite_eq_right (bybs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:0 < zhn:z.toNat - 1 ≠ phj:¬z.toNat - 1 < p⊢ ¬z.toNat - 1 < p + 1 omegaAll goals completed! 🐙), ite_eq_right hjnegbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:0 < zhn:z.toNat - 1 ≠ phj:¬z.toNat - 1 < p⊢ Option.map (⇑boolEmb) none = Option.map (⇑boolEmb) none]All goals completed! 🐙
      ·negbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:¬0 < z⊢ (if 0 < z then Option.map (⇑boolEmb) (List.take (p + 1) bs.reverse).reverse.reverse[z.toNat - 1]? else none) =
  if 0 < z then Option.map (⇑boolEmb) (List.take p bs.reverse).reverse.reverse[z.toNat - 1]? else none rw [ite_eq_right hp,negbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:¬0 < z⊢ none = if 0 < z then Option.map (⇑boolEmb) (List.take p bs.reverse).reverse.reverse[z.toNat - 1]? else none ite_eq_right hpnegbs:List Boolp:ℕz:ℤhe:¬z = ↑(p + 1)hz:¬z = 0hp:¬0 < z⊢ none = none]All goals completed! 🐙

The binary fields after each has erased down to its current head position.

def clearingCfg {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input)
    (bs cs : List Bool) (p r : ℕ) : Cfg 4 (Fin 3) Control input where
  state := some stClear
  inputPos := cfg.inputPos
  workTapes i :=
    if i = 2 then prefixTape bs p
    else if i = 3 then prefixTape cs r
    else cfg.workTapes i
  workTapePos i := if i = 2 then p else if i = 3 then r else cfg.workTapePos i

Erasure finishes with both heads ready to append a fresh binary field.

def clearedCfg {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) :
    Cfg 4 (Fin 3) Control input where
  state := some stLeaf
  inputPos := cfg.inputPos
  workTapes i := if i = 2 ∨ i = 3 then wordTape [] else cfg.workTapes i
  workTapePos i :=
    if i = 0 then cfg.workTapePos 0 - 1
    else if i = 1 then cfg.workTapePos 1
    else 1

Completing a leaf selects the next constructor or the end-of-tree state.

def completedCfg {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input) :
    Cfg 4 (Fin 3) Control input :=
  { clearedCfg cfg with
    state := some (if cfg.workTapes 0 (cfg.workTapePos 0 - 1) == some 2 then stDone else stTree) }

Replacing a counter configuration preserves a bound containing its selected head.

theorem headBound_counterCfg {input : List (Fin 3)} (cfg : Cfg 4 (Fin 3) Control input)
    (v : Bool) (bs : List Bool) (q : Control) (p width : ℕ)
    (hcfg : HeadBound width cfg) (hp : p ≤ width) :
    HeadBound width (counterCfg cfg v bs q p) := byinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlp:ℕwidth:ℕhcfg:HeadBound width cfghp:p ≤ width⊢ HeadBound width (counterCfg cfg v bs q p)
  intro iinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlp:ℕwidth:ℕhcfg:HeadBound width cfghp:p ≤ widthi:Fin 4⊢ 0 ≤ (counterCfg cfg v bs q p).workTapePos i ∧ (counterCfg cfg v bs q p).workTapePos i ≤ ↑width
  by_cases hi : i = counterTape vposinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlp:ℕwidth:ℕhcfg:HeadBound width cfghp:p ≤ widthi:Fin 4hi:i = counterTape v⊢ 0 ≤ (counterCfg cfg v bs q p).workTapePos i ∧ (counterCfg cfg v bs q p).workTapePos i ≤ ↑widthneginput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlp:ℕwidth:ℕhcfg:HeadBound width cfghp:p ≤ widthi:Fin 4hi:¬i = counterTape v⊢ 0 ≤ (counterCfg cfg v bs q p).workTapePos i ∧ (counterCfg cfg v bs q p).workTapePos i ≤ ↑width
  ·posinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlp:ℕwidth:ℕhcfg:HeadBound width cfghp:p ≤ widthi:Fin 4hi:i = counterTape v⊢ 0 ≤ (counterCfg cfg v bs q p).workTapePos i ∧ (counterCfg cfg v bs q p).workTapePos i ≤ ↑width simp only [counterCfg, hi, ite_true]posinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlp:ℕwidth:ℕhcfg:HeadBound width cfghp:p ≤ widthi:Fin 4hi:i = counterTape v⊢ 0 ≤ ↑p ∧ ↑p ≤ ↑width
    exact ⟨byinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlp:ℕwidth:ℕhcfg:HeadBound width cfghp:p ≤ widthi:Fin 4hi:i = counterTape v⊢ 0 ≤ ↑p omegaAll goals completed! 🐙, byinput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlp:ℕwidth:ℕhcfg:HeadBound width cfghp:p ≤ widthi:Fin 4hi:i = counterTape v⊢ ↑p ≤ ↑width exact_mod_cast hpAll goals completed! 🐙⟩
  ·neginput:List (Fin 3)cfg:Cfg 4 (Fin 3) Control inputv:Boolbs:List Boolq:Controlp:ℕwidth:ℕhcfg:HeadBound width cfghp:p ≤ widthi:Fin 4hi:¬i = counterTape v⊢ 0 ≤ (counterCfg cfg v bs q p).workTapePos i ∧ (counterCfg cfg v bs q p).workTapePos i ≤ ↑width simpa only [counterCfg, hi, ite_false] using hcfg iAll goals completed! 🐙

end Geb.BitTree.Elias.Machine