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.Scanner
public import Geb.Prototypes.Computability.TreeScanner.Machine

set_option doc.verso true

A single-pass machine for binary trees with bitstring leaves

The input head advances once per bit. The work head stores the number of pending subtrees; a marker at cell one detects completion of the last leaf. Two initial steps position the work head and install the marker.

Main definitions

unaryScanner implements the fused structural and payload scan.
scanCfg describes a configuration after a prefix has been consumed.

Tags

binary tree, bitstring, Turing machine, recognizer

              @[expose] public sectionnamespace Geb.BitTreeopen Turing MultiTapeTMopen Geb.TreeScanner (boolEmb)

The scanner modes occupy the last five machine states.

def modeState : Mode → Fin 7
  | .tree => 2
  | .string => 3
  | .bit => 4
  | .done => 5
  | .dead => 6

Consume one input bit, moving the counter head by the given displacement.

def consume (q : Fin 7) (d : SignType) : TransitionOut 1 (Fin 2) (Fin 7) where
  inputMove := 1
  workActions _ := (none, d)
  outS := none
  q' := some q

A fused recognizer with one work tape and a unary pending-subtree counter.

def unaryScanner : MultiTapeTM 1 (Fin 2) (Fin 7) where
  q₀ := 0
  tr q input work :=
    if q = 0 then
      { inputMove := 0, workActions := fun _ ↦ (none, 1), outS := none, q' := some 1 }
    else if q = 1 then
      { inputMove := 0, workActions := fun _ ↦ (some (some 0), 0),
        outS := none, q' := some 2 }
    else match input with
      | none =>
        { inputMove := 0, workActions := fun _ ↦ (none, 0),
          outS := some (boolEmb (q == 5)), q' := none }
      | some b =>
        if q = 2 then
          if b = 0 then consume 3 0 else consume 2 1
        else if q = 3 then
          if b = 0 then consume (if work 0 = some 0 then 5 else 2) (-1)
          else consume 4 0
        else if q = 4 then consume 3 0
        else consume 6 0

The configuration between the two initialization steps.

def plantCfg (w : List Bool) : Cfg 1 (Fin 2) (Fin 7) (w.map boolEmb) where
  state := some 1
  inputPos := 1
  workTapes _ _ := none
  workTapePos _ := 1

A configuration at a prefix boundary, with its pure scanner state.

def scanCfg (w : List Bool) (t : ℕ) (h : t ≤ w.length) (s : State) :
    Cfg 1 (Fin 2) (Fin 7) (w.map boolEmb) where
  state := some (modeState s.1)
  inputPos := ⟨t + 1, byw:List Boolt:ℕh:t ≤ w.lengths:State⊢ t + 1 < (List.map (⇑boolEmb) w).length + 2 simp only [List.length_map]w:List Boolt:ℕh:t ≤ w.lengths:State⊢ t + 1 < w.length + 2; omegaAll goals completed! 🐙⟩
  workTapes _ z := if z = 1 then some 0 else none
  workTapePos _ := s.2

Fork tags increment the counter; string terminators decrement it.

def counterMove (m : Mode) (b : Bool) : SignType :=
  match m, b with
  | .tree, true => 1
  | .string, false => -1
  | _, _ => 0

The transition table implements the pure scanner's finite control.

theorem tr_scan (m : Mode) (n : ℕ) (b : Bool) :
    unaryScanner.tr (modeState m) (some (boolEmb b))
        (fun _ ↦ if n = 1 then some 0 else none) =
      consume (modeState (step (m, n) b).1) (counterMove m b) := bym:Moden:ℕb:Bool⊢ (unaryScanner.tr (modeState m) (some (boolEmb b)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (m, n) b).1) (counterMove m b)
  have hf : boolEmb false = 0 := rflm:Moden:ℕb:Boolhf:boolEmb false = 0⊢ (unaryScanner.tr (modeState m) (some (boolEmb b)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (m, n) b).1) (counterMove m b)
  have ht : boolEmb true = 1 := rflm:Moden:ℕb:Boolhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState m) (some (boolEmb b)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (m, n) b).1) (counterMove m b)
  cases mtreen:ℕb:Boolhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.tree) (some (boolEmb b)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.tree, n) b).1) (counterMove Mode.tree b)stringn:ℕb:Boolhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.string) (some (boolEmb b)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.string, n) b).1) (counterMove Mode.string b)bitn:ℕb:Boolhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.bit) (some (boolEmb b)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.bit, n) b).1) (counterMove Mode.bit b)donen:ℕb:Boolhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.done) (some (boolEmb b)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.done, n) b).1) (counterMove Mode.done b)deadn:ℕb:Boolhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.dead) (some (boolEmb b)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.dead, n) b).1) (counterMove Mode.dead b) <;>treen:ℕb:Boolhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.tree) (some (boolEmb b)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.tree, n) b).1) (counterMove Mode.tree b)stringn:ℕb:Boolhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.string) (some (boolEmb b)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.string, n) b).1) (counterMove Mode.string b)bitn:ℕb:Boolhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.bit) (some (boolEmb b)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.bit, n) b).1) (counterMove Mode.bit b)donen:ℕb:Boolhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.done) (some (boolEmb b)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.done, n) b).1) (counterMove Mode.done b)deadn:ℕb:Boolhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.dead) (some (boolEmb b)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.dead, n) b).1) (counterMove Mode.dead b) cases bdead.falsen:ℕhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.dead) (some (boolEmb false)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.dead, n) false).1) (counterMove Mode.dead false)dead.truen:ℕhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.dead) (some (boolEmb true)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.dead, n) true).1) (counterMove Mode.dead true) <;>tree.falsen:ℕhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.tree) (some (boolEmb false)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.tree, n) false).1) (counterMove Mode.tree false)tree.truen:ℕhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.tree) (some (boolEmb true)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.tree, n) true).1) (counterMove Mode.tree true)string.falsen:ℕhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.string) (some (boolEmb false)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.string, n) false).1) (counterMove Mode.string false)string.truen:ℕhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.string) (some (boolEmb true)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.string, n) true).1) (counterMove Mode.string true)bit.falsen:ℕhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.bit) (some (boolEmb false)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.bit, n) false).1) (counterMove Mode.bit false)bit.truen:ℕhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.bit) (some (boolEmb true)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.bit, n) true).1) (counterMove Mode.bit true)done.falsen:ℕhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.done) (some (boolEmb false)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.done, n) false).1) (counterMove Mode.done false)done.truen:ℕhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.done) (some (boolEmb true)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.done, n) true).1) (counterMove Mode.done true)dead.falsen:ℕhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.dead) (some (boolEmb false)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.dead, n) false).1) (counterMove Mode.dead false)dead.truen:ℕhf:boolEmb false = 0ht:boolEmb true = 1⊢ (unaryScanner.tr (modeState Mode.dead) (some (boolEmb true)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.dead, n) true).1) (counterMove Mode.dead true) by_cases h : n = 1posn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:n = 1⊢ (unaryScanner.tr (modeState Mode.dead) (some (boolEmb true)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.dead, n) true).1) (counterMove Mode.dead true)negn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:¬n = 1⊢ (unaryScanner.tr (modeState Mode.dead) (some (boolEmb true)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.dead, n) true).1) (counterMove Mode.dead true) <;>posn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:n = 1⊢ (unaryScanner.tr (modeState Mode.tree) (some (boolEmb false)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.tree, n) false).1) (counterMove Mode.tree false)negn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:¬n = 1⊢ (unaryScanner.tr (modeState Mode.tree) (some (boolEmb false)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.tree, n) false).1) (counterMove Mode.tree false)posn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:n = 1⊢ (unaryScanner.tr (modeState Mode.tree) (some (boolEmb true)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.tree, n) true).1) (counterMove Mode.tree true)negn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:¬n = 1⊢ (unaryScanner.tr (modeState Mode.tree) (some (boolEmb true)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.tree, n) true).1) (counterMove Mode.tree true)posn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:n = 1⊢ (unaryScanner.tr (modeState Mode.string) (some (boolEmb false)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.string, n) false).1) (counterMove Mode.string false)negn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:¬n = 1⊢ (unaryScanner.tr (modeState Mode.string) (some (boolEmb false)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.string, n) false).1) (counterMove Mode.string false)posn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:n = 1⊢ (unaryScanner.tr (modeState Mode.string) (some (boolEmb true)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.string, n) true).1) (counterMove Mode.string true)negn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:¬n = 1⊢ (unaryScanner.tr (modeState Mode.string) (some (boolEmb true)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.string, n) true).1) (counterMove Mode.string true)posn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:n = 1⊢ (unaryScanner.tr (modeState Mode.bit) (some (boolEmb false)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.bit, n) false).1) (counterMove Mode.bit false)negn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:¬n = 1⊢ (unaryScanner.tr (modeState Mode.bit) (some (boolEmb false)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.bit, n) false).1) (counterMove Mode.bit false)posn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:n = 1⊢ (unaryScanner.tr (modeState Mode.bit) (some (boolEmb true)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.bit, n) true).1) (counterMove Mode.bit true)negn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:¬n = 1⊢ (unaryScanner.tr (modeState Mode.bit) (some (boolEmb true)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.bit, n) true).1) (counterMove Mode.bit true)posn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:n = 1⊢ (unaryScanner.tr (modeState Mode.done) (some (boolEmb false)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.done, n) false).1) (counterMove Mode.done false)negn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:¬n = 1⊢ (unaryScanner.tr (modeState Mode.done) (some (boolEmb false)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.done, n) false).1) (counterMove Mode.done false)posn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:n = 1⊢ (unaryScanner.tr (modeState Mode.done) (some (boolEmb true)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.done, n) true).1) (counterMove Mode.done true)negn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:¬n = 1⊢ (unaryScanner.tr (modeState Mode.done) (some (boolEmb true)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.done, n) true).1) (counterMove Mode.done true)posn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:n = 1⊢ (unaryScanner.tr (modeState Mode.dead) (some (boolEmb false)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.dead, n) false).1) (counterMove Mode.dead false)negn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:¬n = 1⊢ (unaryScanner.tr (modeState Mode.dead) (some (boolEmb false)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.dead, n) false).1) (counterMove Mode.dead false)posn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:n = 1⊢ (unaryScanner.tr (modeState Mode.dead) (some (boolEmb true)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.dead, n) true).1) (counterMove Mode.dead true)negn:ℕhf:boolEmb false = 0ht:boolEmb true = 1h:¬n = 1⊢ (unaryScanner.tr (modeState Mode.dead) (some (boolEmb true)) fun x ↦ if n = 1 then some 0 else none) =
  consume (modeState (step (Mode.dead, n) true).1) (counterMove Mode.dead true)
    simp [unaryScanner, modeState, step, finish, counterMove, hf, ht, h]All goals completed! 🐙

The head displacement agrees with the natural-number counter on live states.

theorem counterMove_add (m : Mode) (n : ℕ) (b : Bool)
    (h : m = .string → 0 < n) :
    (n : ℤ) + (counterMove m b : ℤ) = ((step (m, n) b).2 : ℤ) := bym:Moden:ℕb:Boolh:m = Mode.string → 0 < n⊢ ↑n + ↑(counterMove m b) = ↑(step (m, n) b).2
  cases mtreen:ℕb:Boolh:Mode.tree = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.tree b) = ↑(step (Mode.tree, n) b).2stringn:ℕb:Boolh:Mode.string = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.string b) = ↑(step (Mode.string, n) b).2bitn:ℕb:Boolh:Mode.bit = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.bit b) = ↑(step (Mode.bit, n) b).2donen:ℕb:Boolh:Mode.done = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.done b) = ↑(step (Mode.done, n) b).2deadn:ℕb:Boolh:Mode.dead = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.dead b) = ↑(step (Mode.dead, n) b).2 <;>treen:ℕb:Boolh:Mode.tree = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.tree b) = ↑(step (Mode.tree, n) b).2stringn:ℕb:Boolh:Mode.string = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.string b) = ↑(step (Mode.string, n) b).2bitn:ℕb:Boolh:Mode.bit = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.bit b) = ↑(step (Mode.bit, n) b).2donen:ℕb:Boolh:Mode.done = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.done b) = ↑(step (Mode.done, n) b).2deadn:ℕb:Boolh:Mode.dead = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.dead b) = ↑(step (Mode.dead, n) b).2 cases bdead.falsen:ℕh:Mode.dead = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.dead false) = ↑(step (Mode.dead, n) false).2dead.truen:ℕh:Mode.dead = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.dead true) = ↑(step (Mode.dead, n) true).2 <;>tree.falsen:ℕh:Mode.tree = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.tree false) = ↑(step (Mode.tree, n) false).2tree.truen:ℕh:Mode.tree = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.tree true) = ↑(step (Mode.tree, n) true).2string.falsen:ℕh:Mode.string = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.string false) = ↑(step (Mode.string, n) false).2string.truen:ℕh:Mode.string = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.string true) = ↑(step (Mode.string, n) true).2bit.falsen:ℕh:Mode.bit = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.bit false) = ↑(step (Mode.bit, n) false).2bit.truen:ℕh:Mode.bit = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.bit true) = ↑(step (Mode.bit, n) true).2done.falsen:ℕh:Mode.done = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.done false) = ↑(step (Mode.done, n) false).2done.truen:ℕh:Mode.done = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.done true) = ↑(step (Mode.done, n) true).2dead.falsen:ℕh:Mode.dead = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.dead false) = ↑(step (Mode.dead, n) false).2dead.truen:ℕh:Mode.dead = Mode.string → 0 < n⊢ ↑n + ↑(counterMove Mode.dead true) = ↑(step (Mode.dead, n) true).2 try rflAll goals completed! 🐙
  change (n : ℤ) - 1 = ((finish n).2 : ℤ)string.falsen:ℕh:Mode.string = Mode.string → 0 < n⊢ ↑n - 1 = ↑(finish n).2
  unfold finishstring.falsen:ℕh:Mode.string = Mode.string → 0 < n⊢ ↑n - 1 = ↑(if n = 1 then (Mode.done, 0) else (Mode.tree, n - 1)).2
  split_ifs with hnposn:ℕh:Mode.string = Mode.string → 0 < nhn:n = 1⊢ ↑n - 1 = ↑(Mode.done, 0).2negn:ℕh:Mode.string = Mode.string → 0 < nhn:¬n = 1⊢ ↑n - 1 = ↑(Mode.tree, n - 1).2
  ·posn:ℕh:Mode.string = Mode.string → 0 < nhn:n = 1⊢ ↑n - 1 = ↑(Mode.done, 0).2 subst nposh:Mode.string = Mode.string → 0 < 1⊢ ↑1 - 1 = ↑(Mode.done, 0).2
    rflAll goals completed! 🐙
  ·negn:ℕh:Mode.string = Mode.string → 0 < nhn:¬n = 1⊢ ↑n - 1 = ↑(Mode.tree, n - 1).2 dsimp onlynegn:ℕh:Mode.string = Mode.string → 0 < nhn:¬n = 1⊢ ↑n - 1 = ↑(n - 1)
    have hp := h rflnegn:ℕh:Mode.string = Mode.string → 0 < nhn:¬n = 1hp:0 < n⊢ ↑n - 1 = ↑(n - 1)
    omegaAll goals completed! 🐙

A transition increases the pending count by at most one.

theorem step_counter_le (s : State) (b : Bool) : (step s b).2 ≤ s.2 + 1 := bys:Stateb:Bool⊢ (step s b).2 ≤ s.2 + 1
  rcases s with ⟨m, n⟩b:Boolm:Moden:ℕ⊢ (step (m, n) b).2 ≤ (m, n).2 + 1
  cases mtreeb:Booln:ℕ⊢ (step (Mode.tree, n) b).2 ≤ (Mode.tree, n).2 + 1stringb:Booln:ℕ⊢ (step (Mode.string, n) b).2 ≤ (Mode.string, n).2 + 1bitb:Booln:ℕ⊢ (step (Mode.bit, n) b).2 ≤ (Mode.bit, n).2 + 1doneb:Booln:ℕ⊢ (step (Mode.done, n) b).2 ≤ (Mode.done, n).2 + 1deadb:Booln:ℕ⊢ (step (Mode.dead, n) b).2 ≤ (Mode.dead, n).2 + 1 <;>treeb:Booln:ℕ⊢ (step (Mode.tree, n) b).2 ≤ (Mode.tree, n).2 + 1stringb:Booln:ℕ⊢ (step (Mode.string, n) b).2 ≤ (Mode.string, n).2 + 1bitb:Booln:ℕ⊢ (step (Mode.bit, n) b).2 ≤ (Mode.bit, n).2 + 1doneb:Booln:ℕ⊢ (step (Mode.done, n) b).2 ≤ (Mode.done, n).2 + 1deadb:Booln:ℕ⊢ (step (Mode.dead, n) b).2 ≤ (Mode.dead, n).2 + 1 cases bdead.falsen:ℕ⊢ (step (Mode.dead, n) false).2 ≤ (Mode.dead, n).2 + 1dead.truen:ℕ⊢ (step (Mode.dead, n) true).2 ≤ (Mode.dead, n).2 + 1 <;>tree.falsen:ℕ⊢ (step (Mode.tree, n) false).2 ≤ (Mode.tree, n).2 + 1tree.truen:ℕ⊢ (step (Mode.tree, n) true).2 ≤ (Mode.tree, n).2 + 1string.falsen:ℕ⊢ (step (Mode.string, n) false).2 ≤ (Mode.string, n).2 + 1string.truen:ℕ⊢ (step (Mode.string, n) true).2 ≤ (Mode.string, n).2 + 1bit.falsen:ℕ⊢ (step (Mode.bit, n) false).2 ≤ (Mode.bit, n).2 + 1bit.truen:ℕ⊢ (step (Mode.bit, n) true).2 ≤ (Mode.bit, n).2 + 1done.falsen:ℕ⊢ (step (Mode.done, n) false).2 ≤ (Mode.done, n).2 + 1done.truen:ℕ⊢ (step (Mode.done, n) true).2 ≤ (Mode.done, n).2 + 1dead.falsen:ℕ⊢ (step (Mode.dead, n) false).2 ≤ (Mode.dead, n).2 + 1dead.truen:ℕ⊢ (step (Mode.dead, n) true).2 ≤ (Mode.dead, n).2 + 1
    first | exact Nat.le_succ _All goals completed! 🐙 | exact Nat.le_refl _string.falsen:ℕ⊢ (step (Mode.string, n) false).2 ≤ (Mode.string, n).2 + 1
          | (change (finish n).2 ≤ n + 1string.falsen:ℕ⊢ (finish n).2 ≤ n + 1; unfold finishstring.falsen:ℕ⊢ (if n = 1 then (Mode.done, 0) else (Mode.tree, n - 1)).2 ≤ n + 1; splitstring.false.isTruen:ℕh✝:n = 1⊢ (Mode.done, 0).2 ≤ n + 1string.false.isFalsen:ℕh✝:¬n = 1⊢ (Mode.tree, n - 1).2 ≤ n + 1 <;>string.false.isTruen:ℕh✝:n = 1⊢ (Mode.done, 0).2 ≤ n + 1string.false.isFalsen:ℕh✝:¬n = 1⊢ (Mode.tree, n - 1).2 ≤ n + 1 dsimp onlystring.false.isFalsen:ℕh✝:¬n = 1⊢ n - 1 ≤ n + 1 <;>string.false.isTruen:ℕh✝:n = 1⊢ 0 ≤ n + 1string.false.isFalsen:ℕh✝:¬n = 1⊢ n - 1 ≤ n + 1 omegaAll goals completed! 🐙)

A scan's pending count is bounded by its initial count plus its input length.

theorem foldl_counter_le (w : List Bool) :
    ∀ s : State, (w.foldl step s).2 ≤ s.2 + w.length := byw:List Bool⊢ ∀ (s : State), (List.foldl step s w).2 ≤ s.2 + w.length
  refine List.rec ?_ ?_ wrefine_1w:List Bool⊢ ∀ (s : State), (List.foldl step s []).2 ≤ s.2 + [].lengthrefine_2w:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (∀ (s : State), (List.foldl step s tail).2 ≤ s.2 + tail.length) →
    ∀ (s : State), (List.foldl step s (head :: tail)).2 ≤ s.2 + (head :: tail).length
  ·refine_1w:List Bool⊢ ∀ (s : State), (List.foldl step s []).2 ≤ s.2 + [].length intro srefine_1w:List Bools:State⊢ (List.foldl step s []).2 ≤ s.2 + [].length
    exact Nat.le_refl _All goals completed! 🐙
  ·refine_2w:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (∀ (s : State), (List.foldl step s tail).2 ≤ s.2 + tail.length) →
    ∀ (s : State), (List.foldl step s (head :: tail)).2 ≤ s.2 + (head :: tail).length intro b bs ih srefine_2w:List Boolb:Boolbs:List Boolih:∀ (s : State), (List.foldl step s bs).2 ≤ s.2 + bs.lengths:State⊢ (List.foldl step s (b :: bs)).2 ≤ s.2 + (b :: bs).length
    have h := ih (step s b)refine_2w:List Boolb:Boolbs:List Boolih:∀ (s : State), (List.foldl step s bs).2 ≤ s.2 + bs.lengths:Stateh:(List.foldl step (step s b) bs).2 ≤ (step s b).2 + bs.length⊢ (List.foldl step s (b :: bs)).2 ≤ s.2 + (b :: bs).length
    have hstep := step_counter_le s brefine_2w:List Boolb:Boolbs:List Boolih:∀ (s : State), (List.foldl step s bs).2 ≤ s.2 + bs.lengths:Stateh:(List.foldl step (step s b) bs).2 ≤ (step s b).2 + bs.lengthhstep:(step s b).2 ≤ s.2 + 1⊢ (List.foldl step s (b :: bs)).2 ≤ s.2 + (b :: bs).length
    simp only [List.foldl_cons, List.length_cons]refine_2w:List Boolb:Boolbs:List Boolih:∀ (s : State), (List.foldl step s bs).2 ≤ s.2 + bs.lengths:Stateh:(List.foldl step (step s b) bs).2 ≤ (step s b).2 + bs.lengthhstep:(step s b).2 ≤ s.2 + 1⊢ (List.foldl step (step s b) bs).2 ≤ s.2 + (bs.length + 1)
    omegaAll goals completed! 🐙

There are at most one plus the input length pending subtrees.

theorem scan_counter_le (w : List Bool) : (scan w).2 ≤ w.length + 1 := byw:List Bool⊢ (scan w).2 ≤ w.length + 1
  simpa only [scan, Nat.add_comm] using foldl_counter_le w (.tree, 1)All goals completed! 🐙

Extending the scanned prefix applies one pure transition.

theorem scan_take_succ (w : List Bool) (t : ℕ) (h : t < w.length) :
    scan (w.take (t + 1)) = step (scan (w.take t)) w[t] := byw:List Boolt:ℕh:t < w.length⊢ scan (List.take (t + 1) w) = step (scan (List.take t w)) w[t]
  simp only [scan, List.take_succ_eq_append_getElem h, List.foldl_append,
    List.foldl_cons, List.foldl_nil]All goals completed! 🐙

end Geb.BitTree