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 Mathlib.Data.Nat.BinaryRec
public import Mathlib.Data.Nat.Notation
public import Mathlib.Tactic.ToDual

set_option doc.verso true

A bitwise scanner for delta-prefixed leaf payloads

The finite control distinguishes tree tags, the unary part of a delta header, the two binary header fields, and raw payload bits. The pending-subtree counter is changed only by fork tags and completed leaf payloads.

Main definitions

Mode records the current phase and its numeric counters.
step consumes exactly one input bit.
scan folds the transition over the input.

Tags

Elias delta code, binary tree, streaming recognizer

@[expose] public sectionnamespace Geb.BitTree.Elias.Scanner

Header and payload phases, with remaining lengths and partial binary values.

inductive Mode where
  | tree
  | zeros (count : ℕ)
  | size (remaining value : ℕ)
  | length (remaining value : ℕ)
  | payload (remaining : ℕ)
  | done
  | dead
  deriving DecidableEq, Repr, Inhabited

A phase and the number of pending subtrees.

abbrev State := Mode × ℕ

Complete one leaf, recognizing the final pending subtree.

def finish (n : ℕ) : State := if n = 1 then (.done, 0) else (.tree, n - 1)

Read one bit, including all phase changes that consume no additional input.

def step : State → Bool → State
  | (.tree, n), true => (.tree, n + 1)
  | (.tree, n), false => (.zeros 0, n)
  | (.zeros z, n), false => (.zeros (z + 1), n)
  | (.zeros z, n), true => if z = 0 then finish n else (.size z 1, n)
  | (.size r v, n), b =>
    if r = 1 then (.length (Nat.bit b v - 1) 1, n) else (.size (r - 1) (Nat.bit b v), n)
  | (.length r v, n), b =>
    if r = 1 then (.payload (Nat.bit b v - 1), n) else (.length (r - 1) (Nat.bit b v), n)
  | (.payload r, n), _ => if r = 1 then finish n else (.payload (r - 1), n)
  | (.done, n), _ => (.dead, n)
  | (.dead, n), _ => (.dead, n)

Scan from one pending root.

def scan (w : List Bool) : State := w.foldl step (.tree, 1)

Accept exactly when the complete root ends at the end of input.

def validBool (w : List Bool) : Bool := decide ((scan w).1 = .done)

Positive pending counts and positive remaining lengths in the active phases.

def Active : State → Prop
  | (.done, n) | (.dead, n) => n = 0
  | (.tree, n) | (.zeros _, n) => 0 < n
  | (.size r v, n) | (.length r v, n) => 0 < n ∧ 0 < r ∧ 0 < v
  | (.payload r, n) => 0 < n ∧ 0 < r

Completing an active leaf preserves the scanner invariant.

theorem active_finish (n : ℕ) (hn : 0 < n) : Active (finish n) := byn:ℕhn:0 < n⊢ Active (finish n)
  unfold finishn:ℕhn:0 < n⊢ Active (if n = 1 then (Mode.done, 0) else (Mode.tree, n - 1))
  splitisTruen:ℕhn:0 < nh✝:n = 1⊢ Active (Mode.done, 0)isFalsen:ℕhn:0 < nh✝:¬n = 1⊢ Active (Mode.tree, n - 1) <;>isTruen:ℕhn:0 < nh✝:n = 1⊢ Active (Mode.done, 0)isFalsen:ℕhn:0 < nh✝:¬n = 1⊢ Active (Mode.tree, n - 1) simp only [Active]isFalsen:ℕhn:0 < nh✝:¬n = 1⊢ 0 < n - 1 <;>isFalsen:ℕhn:0 < nh✝:¬n = 1⊢ 0 < n - 1 omegaAll goals completed! 🐙

Consuming one bit preserves the invariant.

theorem active_step (s : State) (b : Bool) (h : Active s) : Active (step s b) := bys:Stateb:Boolh:Active s⊢ Active (step s b)
  rcases s with ⟨m, n⟩b:Boolm:Moden:ℕh:Active (m, n)⊢ Active (step (m, n) b)
  cases m with
  | tree =>treeb:Booln:ℕh:Active (Mode.tree, n)⊢ Active (step (Mode.tree, n) b)
    change 0 < n at htreeb:Booln:ℕh:0 < n⊢ Active (step (Mode.tree, n) b)
    cases btree.falsen:ℕh:0 < n⊢ Active (step (Mode.tree, n) false)tree.truen:ℕh:0 < n⊢ Active (step (Mode.tree, n) true) <;>tree.falsen:ℕh:0 < n⊢ Active (step (Mode.tree, n) false)tree.truen:ℕh:0 < n⊢ Active (step (Mode.tree, n) true) change 0 < _tree.truen:ℕh:0 < n⊢ 0 < n + 1 <;>tree.falsen:ℕh:0 < n⊢ 0 < ntree.truen:ℕh:0 < n⊢ 0 < n + 1 omegaAll goals completed! 🐙
  | zeros z =>zerosb:Booln:ℕz:ℕh:Active (Mode.zeros z, n)⊢ Active (step (Mode.zeros z, n) b)
    cases b with
    | false =>zeros.falsen:ℕz:ℕh:Active (Mode.zeros z, n)⊢ Active (step (Mode.zeros z, n) false) exact hAll goals completed! 🐙
    | true =>zeros.truen:ℕz:ℕh:Active (Mode.zeros z, n)⊢ Active (step (Mode.zeros z, n) true)
      change Active (if z = 0 then finish n else (.size z 1, n))zeros.truen:ℕz:ℕh:Active (Mode.zeros z, n)⊢ Active (if z = 0 then finish n else (Mode.size z 1, n))
      splitzeros.true.isTruen:ℕz:ℕh:Active (Mode.zeros z, n)h✝:z = 0⊢ Active (finish n)zeros.true.isFalsen:ℕz:ℕh:Active (Mode.zeros z, n)h✝:¬z = 0⊢ Active (Mode.size z 1, n)
      ·zeros.true.isTruen:ℕz:ℕh:Active (Mode.zeros z, n)h✝:z = 0⊢ Active (finish n) exact active_finish n hAll goals completed! 🐙
      ·zeros.true.isFalsen:ℕz:ℕh:Active (Mode.zeros z, n)h✝:¬z = 0⊢ Active (Mode.size z 1, n) exact ⟨h, byn:ℕz:ℕh:Active (Mode.zeros z, n)h✝:¬z = 0⊢ 0 < z omegaAll goals completed! 🐙, byn:ℕz:ℕh:Active (Mode.zeros z, n)h✝:¬z = 0⊢ 0 < 1 decideAll goals completed! 🐙⟩
  | size r v =>sizeb:Booln:ℕr:ℕv:ℕh:Active (Mode.size r v, n)⊢ Active (step (Mode.size r v, n) b)
    obtain ⟨hn, hr, hv⟩ := hsizeb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < v⊢ Active (step (Mode.size r v, n) b)
    have hb : 2 ≤ Nat.bit b v := bys:Stateb:Boolh:Active s⊢ Active (step s b) rw [Nat.bit_valb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < v⊢ 2 ≤ 2 * v + b.toNat]b:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < v⊢ 2 ≤ 2 * v + b.toNat; omegasizeb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:2 ≤ Nat.bit b v⊢ Active (step (Mode.size r v, n) b)
    change Active (if r = 1 then _ else _)sizeb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:2 ≤ Nat.bit b v⊢ Active (if r = 1 then (Mode.length (Nat.bit b v - 1) 1, n) else (Mode.size (r - 1) (Nat.bit b v), n))
    splitsize.isTrueb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:2 ≤ Nat.bit b vh✝:r = 1⊢ Active (Mode.length (Nat.bit b v - 1) 1, n)size.isFalseb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:2 ≤ Nat.bit b vh✝:¬r = 1⊢ Active (Mode.size (r - 1) (Nat.bit b v), n)
    ·size.isTrueb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:2 ≤ Nat.bit b vh✝:r = 1⊢ Active (Mode.length (Nat.bit b v - 1) 1, n) exact ⟨hn, byb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:2 ≤ Nat.bit b vh✝:r = 1⊢ 0 < Nat.bit b v - 1 omegaAll goals completed! 🐙, byb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:2 ≤ Nat.bit b vh✝:r = 1⊢ 0 < 1 decideAll goals completed! 🐙⟩
    ·size.isFalseb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:2 ≤ Nat.bit b vh✝:¬r = 1⊢ Active (Mode.size (r - 1) (Nat.bit b v), n) exact ⟨hn, byb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:2 ≤ Nat.bit b vh✝:¬r = 1⊢ 0 < r - 1 omegaAll goals completed! 🐙, byb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:2 ≤ Nat.bit b vh✝:¬r = 1⊢ 0 < Nat.bit b v omegaAll goals completed! 🐙⟩
  | length r v =>lengthb:Booln:ℕr:ℕv:ℕh:Active (Mode.length r v, n)⊢ Active (step (Mode.length r v, n) b)
    obtain ⟨hn, hr, hv⟩ := hlengthb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < v⊢ Active (step (Mode.length r v, n) b)
    have hb : 2 ≤ Nat.bit b v := bys:Stateb:Boolh:Active s⊢ Active (step s b) rw [Nat.bit_valb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < v⊢ 2 ≤ 2 * v + b.toNat]b:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < v⊢ 2 ≤ 2 * v + b.toNat; omegalengthb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:2 ≤ Nat.bit b v⊢ Active (step (Mode.length r v, n) b)
    change Active (if r = 1 then _ else _)lengthb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:2 ≤ Nat.bit b v⊢ Active (if r = 1 then (Mode.payload (Nat.bit b v - 1), n) else (Mode.length (r - 1) (Nat.bit b v), n))
    splitlength.isTrueb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:2 ≤ Nat.bit b vh✝:r = 1⊢ Active (Mode.payload (Nat.bit b v - 1), n)length.isFalseb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:2 ≤ Nat.bit b vh✝:¬r = 1⊢ Active (Mode.length (r - 1) (Nat.bit b v), n)
    ·length.isTrueb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:2 ≤ Nat.bit b vh✝:r = 1⊢ Active (Mode.payload (Nat.bit b v - 1), n) exact ⟨hn, byb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:2 ≤ Nat.bit b vh✝:r = 1⊢ 0 < Nat.bit b v - 1 omegaAll goals completed! 🐙⟩
    ·length.isFalseb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:2 ≤ Nat.bit b vh✝:¬r = 1⊢ Active (Mode.length (r - 1) (Nat.bit b v), n) exact ⟨hn, byb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:2 ≤ Nat.bit b vh✝:¬r = 1⊢ 0 < r - 1 omegaAll goals completed! 🐙, byb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:2 ≤ Nat.bit b vh✝:¬r = 1⊢ 0 < Nat.bit b v omegaAll goals completed! 🐙⟩
  | payload r =>payloadb:Booln:ℕr:ℕh:Active (Mode.payload r, n)⊢ Active (step (Mode.payload r, n) b)
    obtain ⟨hn, hr⟩ := hpayloadb:Booln:ℕr:ℕhn:0 < nhr:0 < r⊢ Active (step (Mode.payload r, n) b)
    change Active (if r = 1 then _ else _)payloadb:Booln:ℕr:ℕhn:0 < nhr:0 < r⊢ Active (if r = 1 then finish n else (Mode.payload (r - 1), n))
    splitpayload.isTrueb:Booln:ℕr:ℕhn:0 < nhr:0 < rh✝:r = 1⊢ Active (finish n)payload.isFalseb:Booln:ℕr:ℕhn:0 < nhr:0 < rh✝:¬r = 1⊢ Active (Mode.payload (r - 1), n)
    ·payload.isTrueb:Booln:ℕr:ℕhn:0 < nhr:0 < rh✝:r = 1⊢ Active (finish n) exact active_finish n hnAll goals completed! 🐙
    ·payload.isFalseb:Booln:ℕr:ℕhn:0 < nhr:0 < rh✝:¬r = 1⊢ Active (Mode.payload (r - 1), n) exact ⟨hn, byb:Booln:ℕr:ℕhn:0 < nhr:0 < rh✝:¬r = 1⊢ 0 < r - 1 omegaAll goals completed! 🐙⟩
  | done =>doneb:Booln:ℕh:Active (Mode.done, n)⊢ Active (step (Mode.done, n) b) exact hAll goals completed! 🐙
  | dead =>deadb:Booln:ℕh:Active (Mode.dead, n)⊢ Active (step (Mode.dead, n) b) exact hAll goals completed! 🐙

Every prefix of a scan satisfies the invariant.

theorem active_foldl (w : List Bool) : ∀ s, Active s → Active (w.foldl step s) :=
  List.rec (fun _ h ↦ h) (fun b _ ih s h ↦ ih (step s b) (active_step s b h)) w

The scanner starts and remains in an active or terminal state.

theorem scan_active (w : List Bool) : Active (scan w) :=
  active_foldl w (.tree, 1) (show 0 < 1 byAll goals completed! 🐙 decideAll goals completed! 🐙)

An incomplete raw payload stays in the payload phase.

theorem foldl_payload_short (w : List Bool) : ∀ r n, w.length < r →
    w.foldl step (.payload r, n) = (.payload (r - w.length), n) := byw:List Bool⊢ ∀ (r n : ℕ), w.length < r → List.foldl step (Mode.payload r, n) w = (Mode.payload (r - w.length), n)
  refine List.rec ?_ ?_ wrefine_1w:List Bool⊢ ∀ (r n : ℕ), [].length < r → List.foldl step (Mode.payload r, n) [] = (Mode.payload (r - [].length), n)refine_2w:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (∀ (r n : ℕ), tail.length < r → List.foldl step (Mode.payload r, n) tail = (Mode.payload (r - tail.length), n)) →
    ∀ (r n : ℕ),
      (head :: tail).length < r →
        List.foldl step (Mode.payload r, n) (head :: tail) = (Mode.payload (r - (head :: tail).length), n)
  ·refine_1w:List Bool⊢ ∀ (r n : ℕ), [].length < r → List.foldl step (Mode.payload r, n) [] = (Mode.payload (r - [].length), n) intro r n _refine_1w:List Boolr:ℕn:ℕa✝:[].length < r⊢ List.foldl step (Mode.payload r, n) [] = (Mode.payload (r - [].length), n)
    rflAll goals completed! 🐙
  ·refine_2w:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (∀ (r n : ℕ), tail.length < r → List.foldl step (Mode.payload r, n) tail = (Mode.payload (r - tail.length), n)) →
    ∀ (r n : ℕ),
      (head :: tail).length < r →
        List.foldl step (Mode.payload r, n) (head :: tail) = (Mode.payload (r - (head :: tail).length), n) intro b bs ih r n hrefine_2w:List Boolb:Boolbs:List Boolih:∀ (r n : ℕ), bs.length < r → List.foldl step (Mode.payload r, n) bs = (Mode.payload (r - bs.length), n)r:ℕn:ℕh:(b :: bs).length < r⊢ List.foldl step (Mode.payload r, n) (b :: bs) = (Mode.payload (r - (b :: bs).length), n)
    have hr : r ≠ 1 := byw:List Bool⊢ ∀ (r n : ℕ), w.length < r → List.foldl step (Mode.payload r, n) w = (Mode.payload (r - w.length), n) simp only [List.length_cons] at hw:List Boolb:Boolbs:List Boolih:∀ (r n : ℕ), bs.length < r → List.foldl step (Mode.payload r, n) bs = (Mode.payload (r - bs.length), n)r:ℕn:ℕh:bs.length + 1 < r⊢ r ≠ 1; omegarefine_2w:List Boolb:Boolbs:List Boolih:∀ (r n : ℕ), bs.length < r → List.foldl step (Mode.payload r, n) bs = (Mode.payload (r - bs.length), n)r:ℕn:ℕh:(b :: bs).length < rhr:r ≠ 1⊢ List.foldl step (Mode.payload r, n) (b :: bs) = (Mode.payload (r - (b :: bs).length), n)
    simp only [List.foldl_cons, step, ite_eq_right hr]refine_2w:List Boolb:Boolbs:List Boolih:∀ (r n : ℕ), bs.length < r → List.foldl step (Mode.payload r, n) bs = (Mode.payload (r - bs.length), n)r:ℕn:ℕh:(b :: bs).length < rhr:r ≠ 1⊢ List.foldl step (Mode.payload (r - 1), n) bs = (Mode.payload (r - (b :: bs).length), n)
    rw [ih (r - 1) n (byw:List Boolb:Boolbs:List Boolih:∀ (r n : ℕ), bs.length < r → List.foldl step (Mode.payload r, n) bs = (Mode.payload (r - bs.length), n)r:ℕn:ℕh:(b :: bs).length < rhr:r ≠ 1⊢ bs.length < r - 1 simp only [List.length_cons] at hw:List Boolb:Boolbs:List Boolih:∀ (r n : ℕ), bs.length < r → List.foldl step (Mode.payload r, n) bs = (Mode.payload (r - bs.length), n)r:ℕn:ℕh:bs.length + 1 < rhr:r ≠ 1⊢ bs.length < r - 1; omegaAll goals completed! 🐙)]refine_2w:List Boolb:Boolbs:List Boolih:∀ (r n : ℕ), bs.length < r → List.foldl step (Mode.payload r, n) bs = (Mode.payload (r - bs.length), n)r:ℕn:ℕh:(b :: bs).length < rhr:r ≠ 1⊢ (Mode.payload (r - 1 - bs.length), n) = (Mode.payload (r - (b :: bs).length), n)
    congr 2refine_2.e_fstw:List Boolb:Boolbs:List Boolih:∀ (r n : ℕ), bs.length < r → List.foldl step (Mode.payload r, n) bs = (Mode.payload (r - bs.length), n)r:ℕn:ℕh:(b :: bs).length < rhr:r ≠ 1⊢ r - 1 - bs.length = r - (b :: bs).length
    simp only [List.length_cons]refine_2.e_fstw:List Boolb:Boolbs:List Boolih:∀ (r n : ℕ), bs.length < r → List.foldl step (Mode.payload r, n) bs = (Mode.payload (r - bs.length), n)r:ℕn:ℕh:(b :: bs).length < rhr:r ≠ 1⊢ r - 1 - bs.length = r - (bs.length + 1)
    omegaAll goals completed! 🐙

Consuming a complete nonempty raw payload completes one leaf.

theorem foldl_payload (w : List Bool) : ∀ n, w ≠ [] →
    w.foldl step (.payload w.length, n) = finish n := byw:List Bool⊢ ∀ (n : ℕ), w ≠ [] → List.foldl step (Mode.payload w.length, n) w = finish n
  refine List.rec ?_ ?_ wrefine_1w:List Bool⊢ ∀ (n : ℕ), [] ≠ [] → List.foldl step (Mode.payload [].length, n) [] = finish nrefine_2w:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (∀ (n : ℕ), tail ≠ [] → List.foldl step (Mode.payload tail.length, n) tail = finish n) →
    ∀ (n : ℕ), head :: tail ≠ [] → List.foldl step (Mode.payload (head :: tail).length, n) (head :: tail) = finish n
  ·refine_1w:List Bool⊢ ∀ (n : ℕ), [] ≠ [] → List.foldl step (Mode.payload [].length, n) [] = finish n intro n hrefine_1w:List Booln:ℕh:[] ≠ []⊢ List.foldl step (Mode.payload [].length, n) [] = finish n
    exact (h rfl).elimAll goals completed! 🐙
  ·refine_2w:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (∀ (n : ℕ), tail ≠ [] → List.foldl step (Mode.payload tail.length, n) tail = finish n) →
    ∀ (n : ℕ), head :: tail ≠ [] → List.foldl step (Mode.payload (head :: tail).length, n) (head :: tail) = finish n intro b bs ih n _refine_2w:List Boolb:Boolbs:List Boolih:∀ (n : ℕ), bs ≠ [] → List.foldl step (Mode.payload bs.length, n) bs = finish nn:ℕa✝:b :: bs ≠ []⊢ List.foldl step (Mode.payload (b :: bs).length, n) (b :: bs) = finish n
    cases bs with
    | nil =>refine_2.nilw:List Boolb:Booln:ℕih:∀ (n : ℕ), [] ≠ [] → List.foldl step (Mode.payload [].length, n) [] = finish na✝:[b] ≠ []⊢ List.foldl step (Mode.payload [b].length, n) [b] = finish n rflAll goals completed! 🐙
    | cons c cs =>refine_2.consw:List Boolb:Booln:ℕc:Boolcs:List Boolih:∀ (n : ℕ), c :: cs ≠ [] → List.foldl step (Mode.payload (c :: cs).length, n) (c :: cs) = finish na✝:b :: c :: cs ≠ []⊢ List.foldl step (Mode.payload (b :: c :: cs).length, n) (b :: c :: cs) = finish n
      simp only [List.length_cons, List.foldl_cons, step,
        show cs.length + 1 + 1 ≠ 1 by omega, ↓reduceIte]refine_2.consw:List Boolb:Booln:ℕc:Boolcs:List Boolih:∀ (n : ℕ), c :: cs ≠ [] → List.foldl step (Mode.payload (c :: cs).length, n) (c :: cs) = finish na✝:b :: c :: cs ≠ []⊢ List.foldl step (if cs.length + 1 + 1 - 1 = 1 then finish n else (Mode.payload (cs.length + 1 + 1 - 1 - 1), n)) cs =
  finish n
      exact ih n (byw:List Boolb:Booln:ℕc:Boolcs:List Boolih:∀ (n : ℕ), c :: cs ≠ [] → List.foldl step (Mode.payload (c :: cs).length, n) (c :: cs) = finish na✝:b :: c :: cs ≠ []⊢ c :: cs ≠ [] intro hw:List Boolb:Booln:ℕc:Boolcs:List Boolih:∀ (n : ℕ), c :: cs ≠ [] → List.foldl step (Mode.payload (c :: cs).length, n) (c :: cs) = finish na✝:b :: c :: cs ≠ []h:c :: cs = []⊢ False; cases hAll goals completed! 🐙)

A completed scanner with no further input remains completed.

theorem foldl_done (w : List Bool) (n : ℕ) :
    (w.foldl step (.done, n)).1 = .done ↔ w = [] := byw:List Booln:ℕ⊢ (List.foldl step (Mode.done, n) w).fst = Mode.done ↔ w = []
  have hd (bs : List Bool) : bs.foldl step (.dead, n) = (.dead, n) :=
    List.rec rfl (fun _ _ ih ↦ ih) bsw:List Booln:ℕhd:∀ (bs : List Bool), List.foldl step (Mode.dead, n) bs = (Mode.dead, n)⊢ (List.foldl step (Mode.done, n) w).fst = Mode.done ↔ w = []
  cases w with
  | nil =>niln:ℕhd:∀ (bs : List Bool), List.foldl step (Mode.dead, n) bs = (Mode.dead, n)⊢ (List.foldl step (Mode.done, n) []).fst = Mode.done ↔ [] = [] exact ⟨fun _ ↦ rfl, fun _ ↦ rfl⟩All goals completed! 🐙
  | cons b bs =>consn:ℕhd:∀ (bs : List Bool), List.foldl step (Mode.dead, n) bs = (Mode.dead, n)b:Boolbs:List Bool⊢ (List.foldl step (Mode.done, n) (b :: bs)).fst = Mode.done ↔ b :: bs = []
    change (bs.foldl step (.dead, n)).1 = .done ↔ b :: bs = []consn:ℕhd:∀ (bs : List Bool), List.foldl step (Mode.dead, n) bs = (Mode.dead, n)b:Boolbs:List Bool⊢ (List.foldl step (Mode.dead, n) bs).fst = Mode.done ↔ b :: bs = []
    rw [hdconsn:ℕhd:∀ (bs : List Bool), List.foldl step (Mode.dead, n) bs = (Mode.dead, n)b:Boolbs:List Bool⊢ (Mode.dead, n).fst = Mode.done ↔ b :: bs = []]consn:ℕhd:∀ (bs : List Bool), List.foldl step (Mode.dead, n) bs = (Mode.dead, n)b:Boolbs:List Bool⊢ (Mode.dead, n).fst = Mode.done ↔ b :: bs = []
    constructorcons.mpn:ℕhd:∀ (bs : List Bool), List.foldl step (Mode.dead, n) bs = (Mode.dead, n)b:Boolbs:List Bool⊢ (Mode.dead, n).fst = Mode.done → b :: bs = []cons.mprn:ℕhd:∀ (bs : List Bool), List.foldl step (Mode.dead, n) bs = (Mode.dead, n)b:Boolbs:List Bool⊢ b :: bs = [] → (Mode.dead, n).fst = Mode.done <;>cons.mpn:ℕhd:∀ (bs : List Bool), List.foldl step (Mode.dead, n) bs = (Mode.dead, n)b:Boolbs:List Bool⊢ (Mode.dead, n).fst = Mode.done → b :: bs = []cons.mprn:ℕhd:∀ (bs : List Bool), List.foldl step (Mode.dead, n) bs = (Mode.dead, n)b:Boolbs:List Bool⊢ b :: bs = [] → (Mode.dead, n).fst = Mode.done intro hcons.mprn:ℕhd:∀ (bs : List Bool), List.foldl step (Mode.dead, n) bs = (Mode.dead, n)b:Boolbs:List Boolh:b :: bs = []⊢ (Mode.dead, n).fst = Mode.done <;>cons.mpn:ℕhd:∀ (bs : List Bool), List.foldl step (Mode.dead, n) bs = (Mode.dead, n)b:Boolbs:List Boolh:(Mode.dead, n).fst = Mode.done⊢ b :: bs = []cons.mprn:ℕhd:∀ (bs : List Bool), List.foldl step (Mode.dead, n) bs = (Mode.dead, n)b:Boolbs:List Boolh:b :: bs = []⊢ (Mode.dead, n).fst = Mode.done cases hAll goals completed! 🐙

Acceptance after a declared payload supplies exactly that many raw bits and a suffix.

theorem payload_of_accept (w : List Bool) (m n : ℕ)
    (h : (w.foldl step (if m = 0 then finish n else (.payload m, n))).1 = .done) :
    ∃ s rest, s.length = m ∧ w = s ++ rest ∧ (rest.foldl step (finish n)).1 = .done := byw:List Boolm:ℕn:ℕh:(List.foldl step (if m = 0 then finish n else (Mode.payload m, n)) w).fst = Mode.done⊢ ∃ s rest, s.length = m ∧ w = s ++ rest ∧ (List.foldl step (finish n) rest).fst = Mode.done
  by_cases hm : m = 0posw:List Boolm:ℕn:ℕh:(List.foldl step (if m = 0 then finish n else (Mode.payload m, n)) w).fst = Mode.donehm:m = 0⊢ ∃ s rest, s.length = m ∧ w = s ++ rest ∧ (List.foldl step (finish n) rest).fst = Mode.donenegw:List Boolm:ℕn:ℕh:(List.foldl step (if m = 0 then finish n else (Mode.payload m, n)) w).fst = Mode.donehm:¬m = 0⊢ ∃ s rest, s.length = m ∧ w = s ++ rest ∧ (List.foldl step (finish n) rest).fst = Mode.done
  ·posw:List Boolm:ℕn:ℕh:(List.foldl step (if m = 0 then finish n else (Mode.payload m, n)) w).fst = Mode.donehm:m = 0⊢ ∃ s rest, s.length = m ∧ w = s ++ rest ∧ (List.foldl step (finish n) rest).fst = Mode.done subst mposw:List Booln:ℕh:(List.foldl step (if 0 = 0 then finish n else (Mode.payload 0, n)) w).fst = Mode.done⊢ ∃ s rest, s.length = 0 ∧ w = s ++ rest ∧ (List.foldl step (finish n) rest).fst = Mode.done
    exact ⟨[], w, rfl, rfl, h⟩All goals completed! 🐙
  ·negw:List Boolm:ℕn:ℕh:(List.foldl step (if m = 0 then finish n else (Mode.payload m, n)) w).fst = Mode.donehm:¬m = 0⊢ ∃ s rest, s.length = m ∧ w = s ++ rest ∧ (List.foldl step (finish n) rest).fst = Mode.done rw [ite_eq_right hmnegw:List Boolm:ℕn:ℕh:(List.foldl step (Mode.payload m, n) w).fst = Mode.donehm:¬m = 0⊢ ∃ s rest, s.length = m ∧ w = s ++ rest ∧ (List.foldl step (finish n) rest).fst = Mode.done] at hnegw:List Boolm:ℕn:ℕh:(List.foldl step (Mode.payload m, n) w).fst = Mode.donehm:¬m = 0⊢ ∃ s rest, s.length = m ∧ w = s ++ rest ∧ (List.foldl step (finish n) rest).fst = Mode.done
    by_cases hl : m ≤ w.lengthposw:List Boolm:ℕn:ℕh:(List.foldl step (Mode.payload m, n) w).fst = Mode.donehm:¬m = 0hl:m ≤ w.length⊢ ∃ s rest, s.length = m ∧ w = s ++ rest ∧ (List.foldl step (finish n) rest).fst = Mode.donenegw:List Boolm:ℕn:ℕh:(List.foldl step (Mode.payload m, n) w).fst = Mode.donehm:¬m = 0hl:¬m ≤ w.length⊢ ∃ s rest, s.length = m ∧ w = s ++ rest ∧ (List.foldl step (finish n) rest).fst = Mode.done
    ·posw:List Boolm:ℕn:ℕh:(List.foldl step (Mode.payload m, n) w).fst = Mode.donehm:¬m = 0hl:m ≤ w.length⊢ ∃ s rest, s.length = m ∧ w = s ++ rest ∧ (List.foldl step (finish n) rest).fst = Mode.done have hs : (w.take m).length = m := List.length_take_of_le hlposw:List Boolm:ℕn:ℕh:(List.foldl step (Mode.payload m, n) w).fst = Mode.donehm:¬m = 0hl:m ≤ w.lengthhs:(List.take m w).length = m⊢ ∃ s rest, s.length = m ∧ w = s ++ rest ∧ (List.foldl step (finish n) rest).fst = Mode.done
      have hne : w.take m ≠ [] := by
        intro hew:List Boolm:ℕn:ℕh:(List.foldl step (Mode.payload m, n) w).fst = Mode.donehm:¬m = 0hl:m ≤ w.lengthhs:(List.take m w).length = mhe:List.take m w = []⊢ False
        rw [hew:List Boolm:ℕn:ℕh:(List.foldl step (Mode.payload m, n) w).fst = Mode.donehm:¬m = 0hl:m ≤ w.lengthhs:[].length = mhe:List.take m w = []⊢ False] at hsw:List Boolm:ℕn:ℕh:(List.foldl step (Mode.payload m, n) w).fst = Mode.donehm:¬m = 0hl:m ≤ w.lengthhs:[].length = mhe:List.take m w = []⊢ False
        exact hm hs.symmposw:List Boolm:ℕn:ℕh:(List.foldl step (Mode.payload m, n) w).fst = Mode.donehm:¬m = 0hl:m ≤ w.lengthhs:(List.take m w).length = mhne:List.take m w ≠ []⊢ ∃ s rest, s.length = m ∧ w = s ++ rest ∧ (List.foldl step (finish n) rest).fst = Mode.done
      refine ⟨w.take m, w.drop m, hs, (List.take_append_drop m w).symm, ?_⟩posw:List Boolm:ℕn:ℕh:(List.foldl step (Mode.payload m, n) w).fst = Mode.donehm:¬m = 0hl:m ≤ w.lengthhs:(List.take m w).length = mhne:List.take m w ≠ []⊢ (List.foldl step (finish n) (List.drop m w)).fst = Mode.done
      have hf := foldl_payload (w.take m) n hneposw:List Boolm:ℕn:ℕh:(List.foldl step (Mode.payload m, n) w).fst = Mode.donehm:¬m = 0hl:m ≤ w.lengthhs:(List.take m w).length = mhne:List.take m w ≠ []hf:List.foldl step (Mode.payload (List.take m w).length, n) (List.take m w) = finish n⊢ (List.foldl step (finish n) (List.drop m w)).fst = Mode.done
      rw [hsposw:List Boolm:ℕn:ℕh:(List.foldl step (Mode.payload m, n) w).fst = Mode.donehm:¬m = 0hl:m ≤ w.lengthhs:(List.take m w).length = mhne:List.take m w ≠ []hf:List.foldl step (Mode.payload m, n) (List.take m w) = finish n⊢ (List.foldl step (finish n) (List.drop m w)).fst = Mode.done] at hfposw:List Boolm:ℕn:ℕh:(List.foldl step (Mode.payload m, n) w).fst = Mode.donehm:¬m = 0hl:m ≤ w.lengthhs:(List.take m w).length = mhne:List.take m w ≠ []hf:List.foldl step (Mode.payload m, n) (List.take m w) = finish n⊢ (List.foldl step (finish n) (List.drop m w)).fst = Mode.done
      rw [← List.take_append_drop m w,posw:List Boolm:ℕn:ℕh:(List.foldl step (Mode.payload m, n) (List.take m w ++ List.drop m w)).fst = Mode.donehm:¬m = 0hl:m ≤ w.lengthhs:(List.take m w).length = mhne:List.take m w ≠ []hf:List.foldl step (Mode.payload m, n) (List.take m w) = finish n⊢ (List.foldl step (finish n) (List.drop m w)).fst = Mode.done List.foldl_append,posw:List Boolm:ℕn:ℕh:(List.foldl step (List.foldl step (Mode.payload m, n) (List.take m w)) (List.drop m w)).fst = Mode.donehm:¬m = 0hl:m ≤ w.lengthhs:(List.take m w).length = mhne:List.take m w ≠ []hf:List.foldl step (Mode.payload m, n) (List.take m w) = finish n⊢ (List.foldl step (finish n) (List.drop m w)).fst = Mode.done hfposw:List Boolm:ℕn:ℕh:(List.foldl step (finish n) (List.drop m w)).fst = Mode.donehm:¬m = 0hl:m ≤ w.lengthhs:(List.take m w).length = mhne:List.take m w ≠ []hf:List.foldl step (Mode.payload m, n) (List.take m w) = finish n⊢ (List.foldl step (finish n) (List.drop m w)).fst = Mode.done] at hposw:List Boolm:ℕn:ℕh:(List.foldl step (finish n) (List.drop m w)).fst = Mode.donehm:¬m = 0hl:m ≤ w.lengthhs:(List.take m w).length = mhne:List.take m w ≠ []hf:List.foldl step (Mode.payload m, n) (List.take m w) = finish n⊢ (List.foldl step (finish n) (List.drop m w)).fst = Mode.done
      exact hAll goals completed! 🐙
    ·negw:List Boolm:ℕn:ℕh:(List.foldl step (Mode.payload m, n) w).fst = Mode.donehm:¬m = 0hl:¬m ≤ w.length⊢ ∃ s rest, s.length = m ∧ w = s ++ rest ∧ (List.foldl step (finish n) rest).fst = Mode.done rw [foldl_payload_short w m n (byw:List Boolm:ℕn:ℕh:(List.foldl step (Mode.payload m, n) w).fst = Mode.donehm:¬m = 0hl:¬m ≤ w.length⊢ w.length < m omegaAll goals completed! 🐙)] at hnegw:List Boolm:ℕn:ℕh:(Mode.payload (m - w.length), n).fst = Mode.donehm:¬m = 0hl:¬m ≤ w.length⊢ ∃ s rest, s.length = m ∧ w = s ++ rest ∧ (List.foldl step (finish n) rest).fst = Mode.done
      cases hAll goals completed! 🐙

One input bit introduces at most one additional pending subtree.

theorem step_pending_le (s : State) (b : Bool) : (step s b).2 ≤ s.2 + 1 := bys:Stateb:Bool⊢ (step s b).snd ≤ s.snd + 1
  have hf (n : ℕ) : (finish n).2 ≤ n + 1 := by
    unfold finishs:Stateb:Booln:ℕ⊢ (if n = 1 then (Mode.done, 0) else (Mode.tree, n - 1)).snd ≤ n + 1
    splitisTrues:Stateb:Booln:ℕh✝:n = 1⊢ (Mode.done, 0).snd ≤ n + 1isFalses:Stateb:Booln:ℕh✝:¬n = 1⊢ (Mode.tree, n - 1).snd ≤ n + 1 <;>isTrues:Stateb:Booln:ℕh✝:n = 1⊢ (Mode.done, 0).snd ≤ n + 1isFalses:Stateb:Booln:ℕh✝:¬n = 1⊢ (Mode.tree, n - 1).snd ≤ n + 1 dsimp onlyisFalses:Stateb:Booln:ℕh✝:¬n = 1⊢ n - 1 ≤ n + 1 <;>isTrues:Stateb:Booln:ℕh✝:n = 1⊢ 0 ≤ n + 1isFalses:Stateb:Booln:ℕh✝:¬n = 1⊢ n - 1 ≤ n + 1 omegas:Stateb:Boolhf:∀ (n : ℕ), (finish n).snd ≤ n + 1⊢ (step s b).snd ≤ s.snd + 1
  rcases s with ⟨m, n⟩b:Boolhf:∀ (n : ℕ), (finish n).snd ≤ n + 1m:Moden:ℕ⊢ (step (m, n) b).snd ≤ (m, n).snd + 1
  cases mtreeb:Boolhf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ (step (Mode.tree, n) b).snd ≤ (Mode.tree, n).snd + 1zerosb:Boolhf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕcount✝:ℕ⊢ (step (Mode.zeros count✝, n) b).snd ≤ (Mode.zeros count✝, n).snd + 1sizeb:Boolhf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕvalue✝:ℕ⊢ (step (Mode.size remaining✝ value✝, n) b).snd ≤ (Mode.size remaining✝ value✝, n).snd + 1lengthb:Boolhf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕvalue✝:ℕ⊢ (step (Mode.length remaining✝ value✝, n) b).snd ≤ (Mode.length remaining✝ value✝, n).snd + 1payloadb:Boolhf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕ⊢ (step (Mode.payload remaining✝, n) b).snd ≤ (Mode.payload remaining✝, n).snd + 1doneb:Boolhf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ (step (Mode.done, n) b).snd ≤ (Mode.done, n).snd + 1deadb:Boolhf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ (step (Mode.dead, n) b).snd ≤ (Mode.dead, n).snd + 1 <;>treeb:Boolhf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ (step (Mode.tree, n) b).snd ≤ (Mode.tree, n).snd + 1zerosb:Boolhf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕcount✝:ℕ⊢ (step (Mode.zeros count✝, n) b).snd ≤ (Mode.zeros count✝, n).snd + 1sizeb:Boolhf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕvalue✝:ℕ⊢ (step (Mode.size remaining✝ value✝, n) b).snd ≤ (Mode.size remaining✝ value✝, n).snd + 1lengthb:Boolhf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕvalue✝:ℕ⊢ (step (Mode.length remaining✝ value✝, n) b).snd ≤ (Mode.length remaining✝ value✝, n).snd + 1payloadb:Boolhf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕ⊢ (step (Mode.payload remaining✝, n) b).snd ≤ (Mode.payload remaining✝, n).snd + 1doneb:Boolhf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ (step (Mode.done, n) b).snd ≤ (Mode.done, n).snd + 1deadb:Boolhf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ (step (Mode.dead, n) b).snd ≤ (Mode.dead, n).snd + 1 cases bdead.falsehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ (step (Mode.dead, n) false).snd ≤ (Mode.dead, n).snd + 1dead.truehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ (step (Mode.dead, n) true).snd ≤ (Mode.dead, n).snd + 1 <;>tree.falsehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ (step (Mode.tree, n) false).snd ≤ (Mode.tree, n).snd + 1tree.truehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ (step (Mode.tree, n) true).snd ≤ (Mode.tree, n).snd + 1zeros.falsehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕcount✝:ℕ⊢ (step (Mode.zeros count✝, n) false).snd ≤ (Mode.zeros count✝, n).snd + 1zeros.truehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕcount✝:ℕ⊢ (step (Mode.zeros count✝, n) true).snd ≤ (Mode.zeros count✝, n).snd + 1size.falsehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕvalue✝:ℕ⊢ (step (Mode.size remaining✝ value✝, n) false).snd ≤ (Mode.size remaining✝ value✝, n).snd + 1size.truehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕvalue✝:ℕ⊢ (step (Mode.size remaining✝ value✝, n) true).snd ≤ (Mode.size remaining✝ value✝, n).snd + 1length.falsehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕvalue✝:ℕ⊢ (step (Mode.length remaining✝ value✝, n) false).snd ≤ (Mode.length remaining✝ value✝, n).snd + 1length.truehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕvalue✝:ℕ⊢ (step (Mode.length remaining✝ value✝, n) true).snd ≤ (Mode.length remaining✝ value✝, n).snd + 1payload.falsehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕ⊢ (step (Mode.payload remaining✝, n) false).snd ≤ (Mode.payload remaining✝, n).snd + 1payload.truehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕ⊢ (step (Mode.payload remaining✝, n) true).snd ≤ (Mode.payload remaining✝, n).snd + 1done.falsehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ (step (Mode.done, n) false).snd ≤ (Mode.done, n).snd + 1done.truehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ (step (Mode.done, n) true).snd ≤ (Mode.done, n).snd + 1dead.falsehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ (step (Mode.dead, n) false).snd ≤ (Mode.dead, n).snd + 1dead.truehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ (step (Mode.dead, n) true).snd ≤ (Mode.dead, n).snd + 1 simp only [step]dead.truehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ n ≤ n + 1 <;>tree.falsehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ n ≤ n + 1tree.truehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ n + 1 ≤ n + 1zeros.falsehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕcount✝:ℕ⊢ n ≤ n + 1zeros.truehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕcount✝:ℕ⊢ (if count✝ = 0 then finish n else (Mode.size count✝ 1, n)).snd ≤ n + 1size.falsehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕvalue✝:ℕ⊢ (if remaining✝ = 1 then (Mode.length (Nat.bit false value✝ - 1) 1, n)
    else (Mode.size (remaining✝ - 1) (Nat.bit false value✝), n)).snd ≤
  n + 1size.truehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕvalue✝:ℕ⊢ (if remaining✝ = 1 then (Mode.length (Nat.bit true value✝ - 1) 1, n)
    else (Mode.size (remaining✝ - 1) (Nat.bit true value✝), n)).snd ≤
  n + 1length.falsehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕvalue✝:ℕ⊢ (if remaining✝ = 1 then (Mode.payload (Nat.bit false value✝ - 1), n)
    else (Mode.length (remaining✝ - 1) (Nat.bit false value✝), n)).snd ≤
  n + 1length.truehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕvalue✝:ℕ⊢ (if remaining✝ = 1 then (Mode.payload (Nat.bit true value✝ - 1), n)
    else (Mode.length (remaining✝ - 1) (Nat.bit true value✝), n)).snd ≤
  n + 1payload.falsehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕ⊢ (if remaining✝ = 1 then finish n else (Mode.payload (remaining✝ - 1), n)).snd ≤ n + 1payload.truehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕ⊢ (if remaining✝ = 1 then finish n else (Mode.payload (remaining✝ - 1), n)).snd ≤ n + 1done.falsehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ n ≤ n + 1done.truehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ n ≤ n + 1dead.falsehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ n ≤ n + 1dead.truehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ n ≤ n + 1
    first | exact Nat.le_refl _dead.truehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕ⊢ n ≤ n + 1 | exact Nat.le_succ _All goals completed! 🐙 |
      (splitpayload.true.isTruehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕh✝:remaining✝ = 1⊢ (finish n).snd ≤ n + 1payload.true.isFalsehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕh✝:¬remaining✝ = 1⊢ (Mode.payload (remaining✝ - 1), n).snd ≤ n + 1 <;>payload.true.isTruehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕh✝:remaining✝ = 1⊢ (finish n).snd ≤ n + 1payload.true.isFalsehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕh✝:¬remaining✝ = 1⊢ (Mode.payload (remaining✝ - 1), n).snd ≤ n + 1 first | exact hf npayload.true.isFalsehf:∀ (n : ℕ), (finish n).snd ≤ n + 1n:ℕremaining✝:ℕh✝:¬remaining✝ = 1⊢ (Mode.payload (remaining✝ - 1), n).snd ≤ n + 1 | exact Nat.le_succ _All goals completed! 🐙)

Pending subtrees are bounded by the initial count and the number of bits read.

theorem foldl_pending_le (w : List Bool) : ∀ s,
    (w.foldl step s).2 ≤ s.2 + w.length := byw:List Bool⊢ ∀ (s : State), (List.foldl step s w).snd ≤ s.snd + w.length
  refine List.rec ?_ ?_ wrefine_1w:List Bool⊢ ∀ (s : State), (List.foldl step s []).snd ≤ s.snd + [].lengthrefine_2w:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (∀ (s : State), (List.foldl step s tail).snd ≤ s.snd + tail.length) →
    ∀ (s : State), (List.foldl step s (head :: tail)).snd ≤ s.snd + (head :: tail).length
  ·refine_1w:List Bool⊢ ∀ (s : State), (List.foldl step s []).snd ≤ s.snd + [].length intro srefine_1w:List Bools:State⊢ (List.foldl step s []).snd ≤ s.snd + [].length
    exact Nat.le_refl _All goals completed! 🐙
  ·refine_2w:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (∀ (s : State), (List.foldl step s tail).snd ≤ s.snd + tail.length) →
    ∀ (s : State), (List.foldl step s (head :: tail)).snd ≤ s.snd + (head :: tail).length intro b bs ih srefine_2w:List Boolb:Boolbs:List Boolih:∀ (s : State), (List.foldl step s bs).snd ≤ s.snd + bs.lengths:State⊢ (List.foldl step s (b :: bs)).snd ≤ s.snd + (b :: bs).length
    have h := ih (step s b)refine_2w:List Boolb:Boolbs:List Boolih:∀ (s : State), (List.foldl step s bs).snd ≤ s.snd + bs.lengths:Stateh:(List.foldl step (step s b) bs).snd ≤ (step s b).snd + bs.length⊢ (List.foldl step s (b :: bs)).snd ≤ s.snd + (b :: bs).length
    have hb := step_pending_le s brefine_2w:List Boolb:Boolbs:List Boolih:∀ (s : State), (List.foldl step s bs).snd ≤ s.snd + bs.lengths:Stateh:(List.foldl step (step s b) bs).snd ≤ (step s b).snd + bs.lengthhb:(step s b).snd ≤ s.snd + 1⊢ (List.foldl step s (b :: bs)).snd ≤ s.snd + (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).snd ≤ s.snd + bs.lengths:Stateh:(List.foldl step (step s b) bs).snd ≤ (step s b).snd + bs.lengthhb:(step s b).snd ≤ s.snd + 1⊢ (List.foldl step (step s b) bs).snd ≤ s.snd + (bs.length + 1)
    omegaAll goals completed! 🐙

The unary structural counter uses at most one plus the input length.

theorem scan_pending_le (w : List Bool) : (scan w).2 ≤ w.length + 1 := byw:List Bool⊢ (scan w).snd ≤ w.length + 1
  have h := foldl_pending_le w (.tree, 1)w:List Boolh:(List.foldl step (Mode.tree, 1) w).snd ≤ (Mode.tree, 1).snd + w.length⊢ (scan w).snd ≤ w.length + 1
  change (scan w).2 ≤ 1 + w.length at hw:List Boolh:(scan w).snd ≤ 1 + w.length⊢ (scan w).snd ≤ w.length + 1
  omegaAll goals completed! 🐙

end Geb.BitTree.Elias.Scanner