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.MachineModel

set_option doc.verso true

Space and transition accounting for the Elias scanner

The scalar phase and its two binary words advance together. Their lengths grow by at most one per input bit, bounding both work space and the cost of each complete bit transition.

Main definitions

account records scalar state and binary words at each input boundary.
runCost sums the machine's transition costs.

Tags

Elias delta code, complexity, binary counter

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

Binary-word updates implement the scalar phase update.

theorem words_step (s : Scanner.State) (bs cs : List Bool) (b : Bool)
    (ha : Scanner.Active s) (hw : Words s.1 bs cs) :
    Words (Scanner.step s b).1 (nextWords s.1 bs cs b).1 (nextWords s.1 bs cs b).2 := bys:Scanner.Statebs:List Boolcs:List Boolb:Boolha:Scanner.Active shw:Words s.1 bs cs⊢ Words (Scanner.step s b).1 (nextWords s.1 bs cs b).1 (nextWords s.1 bs cs b).2
  rcases s with ⟨m, n⟩bs:List Boolcs:List Boolb:Boolm:Scanner.Moden:ℕha:Scanner.Active (m, n)hw:Words (m, n).1 bs cs⊢ Words (Scanner.step (m, n) b).1 (nextWords (m, n).1 bs cs b).1 (nextWords (m, n).1 bs cs b).2
  cases m with
  | tree =>treebs:List Boolcs:List Boolb:Booln:ℕha:Scanner.Active (Scanner.Mode.tree, n)hw:Words (Scanner.Mode.tree, n).1 bs cs⊢ Words (Scanner.step (Scanner.Mode.tree, n) b).1 (nextWords (Scanner.Mode.tree, n).1 bs cs b).1
  (nextWords (Scanner.Mode.tree, n).1 bs cs b).2 cases b with
    | false =>tree.falsebs:List Boolcs:List Booln:ℕha:Scanner.Active (Scanner.Mode.tree, n)hw:Words (Scanner.Mode.tree, n).1 bs cs⊢ Words (Scanner.step (Scanner.Mode.tree, n) false).1 (nextWords (Scanner.Mode.tree, n).1 bs cs false).1
  (nextWords (Scanner.Mode.tree, n).1 bs cs false).2 exact ⟨rfl, rfl⟩All goals completed! 🐙
    | true =>tree.truebs:List Boolcs:List Booln:ℕha:Scanner.Active (Scanner.Mode.tree, n)hw:Words (Scanner.Mode.tree, n).1 bs cs⊢ Words (Scanner.step (Scanner.Mode.tree, n) true).1 (nextWords (Scanner.Mode.tree, n).1 bs cs true).1
  (nextWords (Scanner.Mode.tree, n).1 bs cs true).2 exact hwAll goals completed! 🐙
  | zeros z =>zerosbs:List Boolcs:List Boolb:Booln:ℕz:ℕha:Scanner.Active (Scanner.Mode.zeros z, n)hw:Words (Scanner.Mode.zeros z, n).1 bs cs⊢ Words (Scanner.step (Scanner.Mode.zeros z, n) b).1 (nextWords (Scanner.Mode.zeros z, n).1 bs cs b).1
  (nextWords (Scanner.Mode.zeros z, n).1 bs cs b).2
    cases b with
    | false =>zeros.falsebs:List Boolcs:List Booln:ℕz:ℕha:Scanner.Active (Scanner.Mode.zeros z, n)hw:Words (Scanner.Mode.zeros z, n).1 bs cs⊢ Words (Scanner.step (Scanner.Mode.zeros z, n) false).1 (nextWords (Scanner.Mode.zeros z, n).1 bs cs false).1
  (nextWords (Scanner.Mode.zeros z, n).1 bs cs false).2 exact hwAll goals completed! 🐙
    | true =>zeros.truebs:List Boolcs:List Booln:ℕz:ℕha:Scanner.Active (Scanner.Mode.zeros z, n)hw:Words (Scanner.Mode.zeros z, n).1 bs cs⊢ Words (Scanner.step (Scanner.Mode.zeros z, n) true).1 (nextWords (Scanner.Mode.zeros z, n).1 bs cs true).1
  (nextWords (Scanner.Mode.zeros z, n).1 bs cs true).2
      by_cases hz : z = 0posbs:List Boolcs:List Booln:ℕz:ℕha:Scanner.Active (Scanner.Mode.zeros z, n)hw:Words (Scanner.Mode.zeros z, n).1 bs cshz:z = 0⊢ Words (Scanner.step (Scanner.Mode.zeros z, n) true).1 (nextWords (Scanner.Mode.zeros z, n).1 bs cs true).1
  (nextWords (Scanner.Mode.zeros z, n).1 bs cs true).2negbs:List Boolcs:List Booln:ℕz:ℕha:Scanner.Active (Scanner.Mode.zeros z, n)hw:Words (Scanner.Mode.zeros z, n).1 bs cshz:¬z = 0⊢ Words (Scanner.step (Scanner.Mode.zeros z, n) true).1 (nextWords (Scanner.Mode.zeros z, n).1 bs cs true).1
  (nextWords (Scanner.Mode.zeros z, n).1 bs cs true).2
      ·posbs:List Boolcs:List Booln:ℕz:ℕha:Scanner.Active (Scanner.Mode.zeros z, n)hw:Words (Scanner.Mode.zeros z, n).1 bs cshz:z = 0⊢ Words (Scanner.step (Scanner.Mode.zeros z, n) true).1 (nextWords (Scanner.Mode.zeros z, n).1 bs cs true).1
  (nextWords (Scanner.Mode.zeros z, n).1 bs cs true).2 simp only [Scanner.step, nextWords, hz, ↓reduceIte]posbs:List Boolcs:List Booln:ℕz:ℕha:Scanner.Active (Scanner.Mode.zeros z, n)hw:Words (Scanner.Mode.zeros z, n).1 bs cshz:z = 0⊢ Words (Scanner.finish n).1 [] []
        unfold Scanner.finishposbs:List Boolcs:List Booln:ℕz:ℕha:Scanner.Active (Scanner.Mode.zeros z, n)hw:Words (Scanner.Mode.zeros z, n).1 bs cshz:z = 0⊢ Words (if n = 1 then (Scanner.Mode.done, 0) else (Scanner.Mode.tree, n - 1)).1 [] []
        splitpos.isTruebs:List Boolcs:List Booln:ℕz:ℕha:Scanner.Active (Scanner.Mode.zeros z, n)hw:Words (Scanner.Mode.zeros z, n).1 bs cshz:z = 0h✝:n = 1⊢ Words (Scanner.Mode.done, 0).1 [] []pos.isFalsebs:List Boolcs:List Booln:ℕz:ℕha:Scanner.Active (Scanner.Mode.zeros z, n)hw:Words (Scanner.Mode.zeros z, n).1 bs cshz:z = 0h✝:¬n = 1⊢ Words (Scanner.Mode.tree, n - 1).1 [] [] <;>pos.isTruebs:List Boolcs:List Booln:ℕz:ℕha:Scanner.Active (Scanner.Mode.zeros z, n)hw:Words (Scanner.Mode.zeros z, n).1 bs cshz:z = 0h✝:n = 1⊢ Words (Scanner.Mode.done, 0).1 [] []pos.isFalsebs:List Boolcs:List Booln:ℕz:ℕha:Scanner.Active (Scanner.Mode.zeros z, n)hw:Words (Scanner.Mode.zeros z, n).1 bs cshz:z = 0h✝:¬n = 1⊢ Words (Scanner.Mode.tree, n - 1).1 [] [] exact ⟨rfl, rfl⟩All goals completed! 🐙
      ·negbs:List Boolcs:List Booln:ℕz:ℕha:Scanner.Active (Scanner.Mode.zeros z, n)hw:Words (Scanner.Mode.zeros z, n).1 bs cshz:¬z = 0⊢ Words (Scanner.step (Scanner.Mode.zeros z, n) true).1 (nextWords (Scanner.Mode.zeros z, n).1 bs cs true).1
  (nextWords (Scanner.Mode.zeros z, n).1 bs cs true).2 simp only [Scanner.step, nextWords, hz, ↓reduceIte, Words]negbs:List Boolcs:List Booln:ℕz:ℕha:Scanner.Active (Scanner.Mode.zeros z, n)hw:Words (Scanner.Mode.zeros z, n).1 bs cshz:¬z = 0⊢ Counter.value [true] = 1 ∧ cs = [true]
        exact ⟨rfl, hw.2⟩All goals completed! 🐙
  | size r v =>sizebs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕha:Scanner.Active (Scanner.Mode.size r v, n)hw:Words (Scanner.Mode.size r v, n).1 bs cs⊢ Words (Scanner.step (Scanner.Mode.size r v, n) b).1 (nextWords (Scanner.Mode.size r v, n).1 bs cs b).1
  (nextWords (Scanner.Mode.size r v, n).1 bs cs b).2
    obtain ⟨hn, hr, hv⟩ := hasizebs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhw:Words (Scanner.Mode.size r v, n).1 bs cshn:0 < nhr:0 < rhv:0 < v⊢ Words (Scanner.step (Scanner.Mode.size r v, n) b).1 (nextWords (Scanner.Mode.size r v, n).1 bs cs b).1
  (nextWords (Scanner.Mode.size r v, n).1 bs cs b).2
    obtain ⟨hb, hc⟩ := hwsizebs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = vhc:cs = [true]⊢ Words (Scanner.step (Scanner.Mode.size r v, n) b).1 (nextWords (Scanner.Mode.size r v, n).1 bs cs b).1
  (nextWords (Scanner.Mode.size r v, n).1 bs cs b).2
    have hp : 0 < Counter.value (b :: bs) := bys:Scanner.Statebs:List Boolcs:List Boolb:Boolha:Scanner.Active shw:Words s.1 bs cs⊢ Words (Scanner.step s b).1 (nextWords s.1 bs cs b).1 (nextWords s.1 bs cs b).2
      rw [Counter.value_cons,bs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = vhc:cs = [true]⊢ 0 < 2 * Counter.value bs + b.toNat hbbs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = vhc:cs = [true]⊢ 0 < 2 * v + b.toNat]bs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = vhc:cs = [true]⊢ 0 < 2 * v + b.toNat
      omegasizebs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = vhc:cs = [true]hp:0 < Counter.value (b :: bs)⊢ Words (Scanner.step (Scanner.Mode.size r v, n) b).1 (nextWords (Scanner.Mode.size r v, n).1 bs cs b).1
  (nextWords (Scanner.Mode.size r v, n).1 bs cs b).2
    by_cases he : r = 1posbs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = vhc:cs = [true]hp:0 < Counter.value (b :: bs)he:r = 1⊢ Words (Scanner.step (Scanner.Mode.size r v, n) b).1 (nextWords (Scanner.Mode.size r v, n).1 bs cs b).1
  (nextWords (Scanner.Mode.size r v, n).1 bs cs b).2negbs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = vhc:cs = [true]hp:0 < Counter.value (b :: bs)he:¬r = 1⊢ Words (Scanner.step (Scanner.Mode.size r v, n) b).1 (nextWords (Scanner.Mode.size r v, n).1 bs cs b).1
  (nextWords (Scanner.Mode.size r v, n).1 bs cs b).2
    ·posbs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = vhc:cs = [true]hp:0 < Counter.value (b :: bs)he:r = 1⊢ Words (Scanner.step (Scanner.Mode.size r v, n) b).1 (nextWords (Scanner.Mode.size r v, n).1 bs cs b).1
  (nextWords (Scanner.Mode.size r v, n).1 bs cs b).2 simp only [Scanner.step, nextWords, he, ↓reduceIte, Words,
        Counter.value_decrement _ hp, Counter.value_cons, hb, hc, Nat.bit_val]posbs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = vhc:cs = [true]hp:0 < Counter.value (b :: bs)he:r = 1⊢ True ∧ 2 * Counter.value [] + true.toNat = 1
      exact ⟨trivial, rfl⟩All goals completed! 🐙
    ·negbs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = vhc:cs = [true]hp:0 < Counter.value (b :: bs)he:¬r = 1⊢ Words (Scanner.step (Scanner.Mode.size r v, n) b).1 (nextWords (Scanner.Mode.size r v, n).1 bs cs b).1
  (nextWords (Scanner.Mode.size r v, n).1 bs cs b).2 simp only [Scanner.step, nextWords, he, ↓reduceIte, Words, Counter.value_cons,
        hb, Nat.bit_val]negbs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = vhc:cs = [true]hp:0 < Counter.value (b :: bs)he:¬r = 1⊢ True ∧ cs = [true]
      exact ⟨trivial, hc⟩All goals completed! 🐙
  | length r v =>lengthbs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕha:Scanner.Active (Scanner.Mode.length r v, n)hw:Words (Scanner.Mode.length r v, n).1 bs cs⊢ Words (Scanner.step (Scanner.Mode.length r v, n) b).1 (nextWords (Scanner.Mode.length r v, n).1 bs cs b).1
  (nextWords (Scanner.Mode.length r v, n).1 bs cs b).2
    obtain ⟨hn, hr, hv⟩ := halengthbs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhw:Words (Scanner.Mode.length r v, n).1 bs cshn:0 < nhr:0 < rhv:0 < v⊢ Words (Scanner.step (Scanner.Mode.length r v, n) b).1 (nextWords (Scanner.Mode.length r v, n).1 bs cs b).1
  (nextWords (Scanner.Mode.length r v, n).1 bs cs b).2
    obtain ⟨hb, hc⟩ := hwlengthbs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = rhc:Counter.value cs = v⊢ Words (Scanner.step (Scanner.Mode.length r v, n) b).1 (nextWords (Scanner.Mode.length r v, n).1 bs cs b).1
  (nextWords (Scanner.Mode.length r v, n).1 bs cs b).2
    have hp : 0 < Counter.value (b :: cs) := bys:Scanner.Statebs:List Boolcs:List Boolb:Boolha:Scanner.Active shw:Words s.1 bs cs⊢ Words (Scanner.step s b).1 (nextWords s.1 bs cs b).1 (nextWords s.1 bs cs b).2
      rw [Counter.value_cons,bs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = rhc:Counter.value cs = v⊢ 0 < 2 * Counter.value cs + b.toNat hcbs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = rhc:Counter.value cs = v⊢ 0 < 2 * v + b.toNat]bs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = rhc:Counter.value cs = v⊢ 0 < 2 * v + b.toNat
      omegalengthbs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = rhc:Counter.value cs = vhp:0 < Counter.value (b :: cs)⊢ Words (Scanner.step (Scanner.Mode.length r v, n) b).1 (nextWords (Scanner.Mode.length r v, n).1 bs cs b).1
  (nextWords (Scanner.Mode.length r v, n).1 bs cs b).2
    have hbs : 0 < Counter.value bs := bys:Scanner.Statebs:List Boolcs:List Boolb:Boolha:Scanner.Active shw:Words s.1 bs cs⊢ Words (Scanner.step s b).1 (nextWords s.1 bs cs b).1 (nextWords s.1 bs cs b).2 rw [hbbs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = rhc:Counter.value cs = vhp:0 < Counter.value (b :: cs)⊢ 0 < r]bs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = rhc:Counter.value cs = vhp:0 < Counter.value (b :: cs)⊢ 0 < r; exact hrlengthbs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = rhc:Counter.value cs = vhp:0 < Counter.value (b :: cs)hbs:0 < Counter.value bs⊢ Words (Scanner.step (Scanner.Mode.length r v, n) b).1 (nextWords (Scanner.Mode.length r v, n).1 bs cs b).1
  (nextWords (Scanner.Mode.length r v, n).1 bs cs b).2
    by_cases he : r = 1posbs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = rhc:Counter.value cs = vhp:0 < Counter.value (b :: cs)hbs:0 < Counter.value bshe:r = 1⊢ Words (Scanner.step (Scanner.Mode.length r v, n) b).1 (nextWords (Scanner.Mode.length r v, n).1 bs cs b).1
  (nextWords (Scanner.Mode.length r v, n).1 bs cs b).2negbs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = rhc:Counter.value cs = vhp:0 < Counter.value (b :: cs)hbs:0 < Counter.value bshe:¬r = 1⊢ Words (Scanner.step (Scanner.Mode.length r v, n) b).1 (nextWords (Scanner.Mode.length r v, n).1 bs cs b).1
  (nextWords (Scanner.Mode.length r v, n).1 bs cs b).2
    ·posbs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = rhc:Counter.value cs = vhp:0 < Counter.value (b :: cs)hbs:0 < Counter.value bshe:r = 1⊢ Words (Scanner.step (Scanner.Mode.length r v, n) b).1 (nextWords (Scanner.Mode.length r v, n).1 bs cs b).1
  (nextWords (Scanner.Mode.length r v, n).1 bs cs b).2 simp only [Scanner.step, nextWords, he, ↓reduceIte, Words,
        Counter.value_decrement _ hbs, Counter.value_decrement _ hp,
        Counter.value_cons, hb, hc, Nat.bit_val]posbs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = rhc:Counter.value cs = vhp:0 < Counter.value (b :: cs)hbs:0 < Counter.value bshe:r = 1⊢ True ∧ True
      exact ⟨trivial, trivial⟩All goals completed! 🐙
    ·negbs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = rhc:Counter.value cs = vhp:0 < Counter.value (b :: cs)hbs:0 < Counter.value bshe:¬r = 1⊢ Words (Scanner.step (Scanner.Mode.length r v, n) b).1 (nextWords (Scanner.Mode.length r v, n).1 bs cs b).1
  (nextWords (Scanner.Mode.length r v, n).1 bs cs b).2 simp only [Scanner.step, nextWords, he, ↓reduceIte, Words,
        Counter.value_decrement _ hbs, Counter.value_cons, hb, hc, Nat.bit_val]negbs:List Boolcs:List Boolb:Booln:ℕr:ℕv:ℕhn:0 < nhr:0 < rhv:0 < vhb:Counter.value bs = rhc:Counter.value cs = vhp:0 < Counter.value (b :: cs)hbs:0 < Counter.value bshe:¬r = 1⊢ True ∧ True
      exact ⟨trivial, trivial⟩All goals completed! 🐙
  | payload r =>payloadbs:List Boolcs:List Boolb:Booln:ℕr:ℕha:Scanner.Active (Scanner.Mode.payload r, n)hw:Words (Scanner.Mode.payload r, n).1 bs cs⊢ Words (Scanner.step (Scanner.Mode.payload r, n) b).1 (nextWords (Scanner.Mode.payload r, n).1 bs cs b).1
  (nextWords (Scanner.Mode.payload r, n).1 bs cs b).2
    obtain ⟨hn, hr⟩ := hapayloadbs:List Boolcs:List Boolb:Booln:ℕr:ℕhw:Words (Scanner.Mode.payload r, n).1 bs cshn:0 < nhr:0 < r⊢ Words (Scanner.step (Scanner.Mode.payload r, n) b).1 (nextWords (Scanner.Mode.payload r, n).1 bs cs b).1
  (nextWords (Scanner.Mode.payload r, n).1 bs cs b).2
    obtain ⟨hb, hc⟩ := hwpayloadbs:List Boolcs:List Boolb:Booln:ℕr:ℕhn:0 < nhr:0 < rhb:Counter.value bs = 0hc:Counter.value cs = r⊢ Words (Scanner.step (Scanner.Mode.payload r, n) b).1 (nextWords (Scanner.Mode.payload r, n).1 bs cs b).1
  (nextWords (Scanner.Mode.payload r, n).1 bs cs b).2
    by_cases he : r = 1posbs:List Boolcs:List Boolb:Booln:ℕr:ℕhn:0 < nhr:0 < rhb:Counter.value bs = 0hc:Counter.value cs = rhe:r = 1⊢ Words (Scanner.step (Scanner.Mode.payload r, n) b).1 (nextWords (Scanner.Mode.payload r, n).1 bs cs b).1
  (nextWords (Scanner.Mode.payload r, n).1 bs cs b).2negbs:List Boolcs:List Boolb:Booln:ℕr:ℕhn:0 < nhr:0 < rhb:Counter.value bs = 0hc:Counter.value cs = rhe:¬r = 1⊢ Words (Scanner.step (Scanner.Mode.payload r, n) b).1 (nextWords (Scanner.Mode.payload r, n).1 bs cs b).1
  (nextWords (Scanner.Mode.payload r, n).1 bs cs b).2
    ·posbs:List Boolcs:List Boolb:Booln:ℕr:ℕhn:0 < nhr:0 < rhb:Counter.value bs = 0hc:Counter.value cs = rhe:r = 1⊢ Words (Scanner.step (Scanner.Mode.payload r, n) b).1 (nextWords (Scanner.Mode.payload r, n).1 bs cs b).1
  (nextWords (Scanner.Mode.payload r, n).1 bs cs b).2 simp only [Scanner.step, nextWords, he, ↓reduceIte]posbs:List Boolcs:List Boolb:Booln:ℕr:ℕhn:0 < nhr:0 < rhb:Counter.value bs = 0hc:Counter.value cs = rhe:r = 1⊢ Words (Scanner.finish n).1 [] []
      unfold Scanner.finishposbs:List Boolcs:List Boolb:Booln:ℕr:ℕhn:0 < nhr:0 < rhb:Counter.value bs = 0hc:Counter.value cs = rhe:r = 1⊢ Words (if n = 1 then (Scanner.Mode.done, 0) else (Scanner.Mode.tree, n - 1)).1 [] []
      splitpos.isTruebs:List Boolcs:List Boolb:Booln:ℕr:ℕhn:0 < nhr:0 < rhb:Counter.value bs = 0hc:Counter.value cs = rhe:r = 1h✝:n = 1⊢ Words (Scanner.Mode.done, 0).1 [] []pos.isFalsebs:List Boolcs:List Boolb:Booln:ℕr:ℕhn:0 < nhr:0 < rhb:Counter.value bs = 0hc:Counter.value cs = rhe:r = 1h✝:¬n = 1⊢ Words (Scanner.Mode.tree, n - 1).1 [] [] <;>pos.isTruebs:List Boolcs:List Boolb:Booln:ℕr:ℕhn:0 < nhr:0 < rhb:Counter.value bs = 0hc:Counter.value cs = rhe:r = 1h✝:n = 1⊢ Words (Scanner.Mode.done, 0).1 [] []pos.isFalsebs:List Boolcs:List Boolb:Booln:ℕr:ℕhn:0 < nhr:0 < rhb:Counter.value bs = 0hc:Counter.value cs = rhe:r = 1h✝:¬n = 1⊢ Words (Scanner.Mode.tree, n - 1).1 [] [] exact ⟨rfl, rfl⟩All goals completed! 🐙
    ·negbs:List Boolcs:List Boolb:Booln:ℕr:ℕhn:0 < nhr:0 < rhb:Counter.value bs = 0hc:Counter.value cs = rhe:¬r = 1⊢ Words (Scanner.step (Scanner.Mode.payload r, n) b).1 (nextWords (Scanner.Mode.payload r, n).1 bs cs b).1
  (nextWords (Scanner.Mode.payload r, n).1 bs cs b).2 have hp : 0 < Counter.value cs := bys:Scanner.Statebs:List Boolcs:List Boolb:Boolha:Scanner.Active shw:Words s.1 bs cs⊢ Words (Scanner.step s b).1 (nextWords s.1 bs cs b).1 (nextWords s.1 bs cs b).2 rw [hcbs:List Boolcs:List Boolb:Booln:ℕr:ℕhn:0 < nhr:0 < rhb:Counter.value bs = 0hc:Counter.value cs = rhe:¬r = 1⊢ 0 < r]bs:List Boolcs:List Boolb:Booln:ℕr:ℕhn:0 < nhr:0 < rhb:Counter.value bs = 0hc:Counter.value cs = rhe:¬r = 1⊢ 0 < r; exact hrnegbs:List Boolcs:List Boolb:Booln:ℕr:ℕhn:0 < nhr:0 < rhb:Counter.value bs = 0hc:Counter.value cs = rhe:¬r = 1hp:0 < Counter.value cs⊢ Words (Scanner.step (Scanner.Mode.payload r, n) b).1 (nextWords (Scanner.Mode.payload r, n).1 bs cs b).1
  (nextWords (Scanner.Mode.payload r, n).1 bs cs b).2
      simp only [Scanner.step, nextWords, he, ↓reduceIte, Words,
        Counter.value_decrement _ hp, hc]negbs:List Boolcs:List Boolb:Booln:ℕr:ℕhn:0 < nhr:0 < rhb:Counter.value bs = 0hc:Counter.value cs = rhe:¬r = 1hp:0 < Counter.value cs⊢ Counter.value bs = 0 ∧ True
      exact ⟨hb, trivial⟩All goals completed! 🐙
  | done =>donebs:List Boolcs:List Boolb:Booln:ℕha:Scanner.Active (Scanner.Mode.done, n)hw:Words (Scanner.Mode.done, n).1 bs cs⊢ Words (Scanner.step (Scanner.Mode.done, n) b).1 (nextWords (Scanner.Mode.done, n).1 bs cs b).1
  (nextWords (Scanner.Mode.done, n).1 bs cs b).2 exact hwAll goals completed! 🐙
  | dead =>deadbs:List Boolcs:List Boolb:Booln:ℕha:Scanner.Active (Scanner.Mode.dead, n)hw:Words (Scanner.Mode.dead, n).1 bs cs⊢ Words (Scanner.step (Scanner.Mode.dead, n) b).1 (nextWords (Scanner.Mode.dead, n).1 bs cs b).1
  (nextWords (Scanner.Mode.dead, n).1 bs cs b).2 exact hwAll goals completed! 🐙

A scalar state paired with its two finite binary words.

abbrev Account := Scanner.State × (List Bool × List Bool)

One pending root and initially empty binary fields.

def initialAccount : Account := ((.tree, 1), [], [])

Advance the scalar state and both binary fields by one input bit.

def accountStep (s : Account) (b : Bool) : Account :=
  (Scanner.step s.1 b, nextWords s.1.1 s.2.1 s.2.2 b)

State and fields after a finite input prefix.

def account (w : List Bool) : Account := w.foldl accountStep initialAccount

The two descriptions agree at every boundary.

def AccountValid (s : Account) : Prop := Scanner.Active s.1 ∧ Words s.1.1 s.2.1 s.2.2

A complete bit transition preserves scalar and binary-word invariants.

theorem accountStep_valid (s : Account) (b : Bool) (h : AccountValid s) :
    AccountValid (accountStep s b) :=
  ⟨Scanner.active_step s.1 b h.1, words_step s.1 s.2.1 s.2.2 b h.1 h.2⟩

The invariant is preserved across any input suffix.

theorem account_foldl_valid (w : List Bool) : ∀ s, AccountValid s →
    AccountValid (w.foldl accountStep s) :=
  List.rec (fun _ h ↦ h) (fun b _ ih s h ↦ ih _ (accountStep_valid s b h)) w

Projection commutes with scanning any suffix.

theorem account_foldl_project (w : List Bool) : ∀ s,
    (w.foldl accountStep s).1 = w.foldl Scanner.step s.1 :=
  List.rec (fun _ ↦ rfl) (fun b _ ih s ↦ ih (accountStep s b)) w

The scalar account component is the streaming scanner state.

theorem account_project (w : List Bool) : (account w).1 = Scanner.scan w :=
  account_foldl_project w initialAccount

The account invariant holds after every input prefix.

theorem account_valid (w : List Bool) : AccountValid (account w) :=
  account_foldl_valid w initialAccount ⟨show 0 < 1 byAll goals completed! 🐙 decideAll goals completed! 🐙, rfl, rfl⟩

The scalar component remains active or terminal.

theorem account_active (w : List Bool) : Scanner.Active (account w).1 :=
  (account_valid w).1

Both finite words represent their scalar phase values.

theorem account_words (w : List Bool) :
    Words (account w).1.1 (account w).2.1 (account w).2.2 := (account_valid w).2

Each binary word grows by at most one per input bit.

theorem nextWords_lengths_le (m : Scanner.Mode) (bs cs : List Bool) (b : Bool) :
    (nextWords m bs cs b).1.length ≤ bs.length + 1 ∧
      (nextWords m bs cs b).2.length ≤ cs.length + 1 := bym:Scanner.Modebs:List Boolcs:List Boolb:Bool⊢ (nextWords m bs cs b).1.length ≤ bs.length + 1 ∧ (nextWords m bs cs b).2.length ≤ cs.length + 1
  cases mtreebs:List Boolcs:List Boolb:Bool⊢ (nextWords Scanner.Mode.tree bs cs b).1.length ≤ bs.length + 1 ∧
  (nextWords Scanner.Mode.tree bs cs b).2.length ≤ cs.length + 1zerosbs:List Boolcs:List Boolb:Boolcount✝:ℕ⊢ (nextWords (Scanner.Mode.zeros count✝) bs cs b).1.length ≤ bs.length + 1 ∧
  (nextWords (Scanner.Mode.zeros count✝) bs cs b).2.length ≤ cs.length + 1sizebs:List Boolcs:List Boolb:Boolremaining✝:ℕvalue✝:ℕ⊢ (nextWords (Scanner.Mode.size remaining✝ value✝) bs cs b).1.length ≤ bs.length + 1 ∧
  (nextWords (Scanner.Mode.size remaining✝ value✝) bs cs b).2.length ≤ cs.length + 1lengthbs:List Boolcs:List Boolb:Boolremaining✝:ℕvalue✝:ℕ⊢ (nextWords (Scanner.Mode.length remaining✝ value✝) bs cs b).1.length ≤ bs.length + 1 ∧
  (nextWords (Scanner.Mode.length remaining✝ value✝) bs cs b).2.length ≤ cs.length + 1payloadbs:List Boolcs:List Boolb:Boolremaining✝:ℕ⊢ (nextWords (Scanner.Mode.payload remaining✝) bs cs b).1.length ≤ bs.length + 1 ∧
  (nextWords (Scanner.Mode.payload remaining✝) bs cs b).2.length ≤ cs.length + 1donebs:List Boolcs:List Boolb:Bool⊢ (nextWords Scanner.Mode.done bs cs b).1.length ≤ bs.length + 1 ∧
  (nextWords Scanner.Mode.done bs cs b).2.length ≤ cs.length + 1deadbs:List Boolcs:List Boolb:Bool⊢ (nextWords Scanner.Mode.dead bs cs b).1.length ≤ bs.length + 1 ∧
  (nextWords Scanner.Mode.dead bs cs b).2.length ≤ cs.length + 1 <;>treebs:List Boolcs:List Boolb:Bool⊢ (nextWords Scanner.Mode.tree bs cs b).1.length ≤ bs.length + 1 ∧
  (nextWords Scanner.Mode.tree bs cs b).2.length ≤ cs.length + 1zerosbs:List Boolcs:List Boolb:Boolcount✝:ℕ⊢ (nextWords (Scanner.Mode.zeros count✝) bs cs b).1.length ≤ bs.length + 1 ∧
  (nextWords (Scanner.Mode.zeros count✝) bs cs b).2.length ≤ cs.length + 1sizebs:List Boolcs:List Boolb:Boolremaining✝:ℕvalue✝:ℕ⊢ (nextWords (Scanner.Mode.size remaining✝ value✝) bs cs b).1.length ≤ bs.length + 1 ∧
  (nextWords (Scanner.Mode.size remaining✝ value✝) bs cs b).2.length ≤ cs.length + 1lengthbs:List Boolcs:List Boolb:Boolremaining✝:ℕvalue✝:ℕ⊢ (nextWords (Scanner.Mode.length remaining✝ value✝) bs cs b).1.length ≤ bs.length + 1 ∧
  (nextWords (Scanner.Mode.length remaining✝ value✝) bs cs b).2.length ≤ cs.length + 1payloadbs:List Boolcs:List Boolb:Boolremaining✝:ℕ⊢ (nextWords (Scanner.Mode.payload remaining✝) bs cs b).1.length ≤ bs.length + 1 ∧
  (nextWords (Scanner.Mode.payload remaining✝) bs cs b).2.length ≤ cs.length + 1donebs:List Boolcs:List Boolb:Bool⊢ (nextWords Scanner.Mode.done bs cs b).1.length ≤ bs.length + 1 ∧
  (nextWords Scanner.Mode.done bs cs b).2.length ≤ cs.length + 1deadbs:List Boolcs:List Boolb:Bool⊢ (nextWords Scanner.Mode.dead bs cs b).1.length ≤ bs.length + 1 ∧
  (nextWords Scanner.Mode.dead bs cs b).2.length ≤ cs.length + 1 cases bdead.falsebs:List Boolcs:List Bool⊢ (nextWords Scanner.Mode.dead bs cs false).1.length ≤ bs.length + 1 ∧
  (nextWords Scanner.Mode.dead bs cs false).2.length ≤ cs.length + 1dead.truebs:List Boolcs:List Bool⊢ (nextWords Scanner.Mode.dead bs cs true).1.length ≤ bs.length + 1 ∧
  (nextWords Scanner.Mode.dead bs cs true).2.length ≤ cs.length + 1 <;>tree.falsebs:List Boolcs:List Bool⊢ (nextWords Scanner.Mode.tree bs cs false).1.length ≤ bs.length + 1 ∧
  (nextWords Scanner.Mode.tree bs cs false).2.length ≤ cs.length + 1tree.truebs:List Boolcs:List Bool⊢ (nextWords Scanner.Mode.tree bs cs true).1.length ≤ bs.length + 1 ∧
  (nextWords Scanner.Mode.tree bs cs true).2.length ≤ cs.length + 1zeros.falsebs:List Boolcs:List Boolcount✝:ℕ⊢ (nextWords (Scanner.Mode.zeros count✝) bs cs false).1.length ≤ bs.length + 1 ∧
  (nextWords (Scanner.Mode.zeros count✝) bs cs false).2.length ≤ cs.length + 1zeros.truebs:List Boolcs:List Boolcount✝:ℕ⊢ (nextWords (Scanner.Mode.zeros count✝) bs cs true).1.length ≤ bs.length + 1 ∧
  (nextWords (Scanner.Mode.zeros count✝) bs cs true).2.length ≤ cs.length + 1size.falsebs:List Boolcs:List Boolremaining✝:ℕvalue✝:ℕ⊢ (nextWords (Scanner.Mode.size remaining✝ value✝) bs cs false).1.length ≤ bs.length + 1 ∧
  (nextWords (Scanner.Mode.size remaining✝ value✝) bs cs false).2.length ≤ cs.length + 1size.truebs:List Boolcs:List Boolremaining✝:ℕvalue✝:ℕ⊢ (nextWords (Scanner.Mode.size remaining✝ value✝) bs cs true).1.length ≤ bs.length + 1 ∧
  (nextWords (Scanner.Mode.size remaining✝ value✝) bs cs true).2.length ≤ cs.length + 1length.falsebs:List Boolcs:List Boolremaining✝:ℕvalue✝:ℕ⊢ (nextWords (Scanner.Mode.length remaining✝ value✝) bs cs false).1.length ≤ bs.length + 1 ∧
  (nextWords (Scanner.Mode.length remaining✝ value✝) bs cs false).2.length ≤ cs.length + 1length.truebs:List Boolcs:List Boolremaining✝:ℕvalue✝:ℕ⊢ (nextWords (Scanner.Mode.length remaining✝ value✝) bs cs true).1.length ≤ bs.length + 1 ∧
  (nextWords (Scanner.Mode.length remaining✝ value✝) bs cs true).2.length ≤ cs.length + 1payload.falsebs:List Boolcs:List Boolremaining✝:ℕ⊢ (nextWords (Scanner.Mode.payload remaining✝) bs cs false).1.length ≤ bs.length + 1 ∧
  (nextWords (Scanner.Mode.payload remaining✝) bs cs false).2.length ≤ cs.length + 1payload.truebs:List Boolcs:List Boolremaining✝:ℕ⊢ (nextWords (Scanner.Mode.payload remaining✝) bs cs true).1.length ≤ bs.length + 1 ∧
  (nextWords (Scanner.Mode.payload remaining✝) bs cs true).2.length ≤ cs.length + 1done.falsebs:List Boolcs:List Bool⊢ (nextWords Scanner.Mode.done bs cs false).1.length ≤ bs.length + 1 ∧
  (nextWords Scanner.Mode.done bs cs false).2.length ≤ cs.length + 1done.truebs:List Boolcs:List Bool⊢ (nextWords Scanner.Mode.done bs cs true).1.length ≤ bs.length + 1 ∧
  (nextWords Scanner.Mode.done bs cs true).2.length ≤ cs.length + 1dead.falsebs:List Boolcs:List Bool⊢ (nextWords Scanner.Mode.dead bs cs false).1.length ≤ bs.length + 1 ∧
  (nextWords Scanner.Mode.dead bs cs false).2.length ≤ cs.length + 1dead.truebs:List Boolcs:List Bool⊢ (nextWords Scanner.Mode.dead bs cs true).1.length ≤ bs.length + 1 ∧
  (nextWords Scanner.Mode.dead bs cs true).2.length ≤ cs.length + 1 simp only [nextWords]dead.truebs:List Boolcs:List Bool⊢ bs.length ≤ bs.length + 1 ∧ cs.length ≤ cs.length + 1 <;>tree.falsebs:List Boolcs:List Bool⊢ [].length ≤ bs.length + 1 ∧ [true].length ≤ cs.length + 1tree.truebs:List Boolcs:List Bool⊢ bs.length ≤ bs.length + 1 ∧ cs.length ≤ cs.length + 1zeros.falsebs:List Boolcs:List Boolcount✝:ℕ⊢ bs.length ≤ bs.length + 1 ∧ cs.length ≤ cs.length + 1zeros.truebs:List Boolcs:List Boolcount✝:ℕ⊢ (if count✝ = 0 then ([], []) else ([true], cs)).1.length ≤ bs.length + 1 ∧
  (if count✝ = 0 then ([], []) else ([true], cs)).2.length ≤ cs.length + 1size.falsebs:List Boolcs:List Boolremaining✝:ℕvalue✝:ℕ⊢ (if remaining✝ = 1 then (Counter.decrement (false :: bs), cs) else (false :: bs, cs)).1.length ≤ bs.length + 1 ∧
  (if remaining✝ = 1 then (Counter.decrement (false :: bs), cs) else (false :: bs, cs)).2.length ≤ cs.length + 1size.truebs:List Boolcs:List Boolremaining✝:ℕvalue✝:ℕ⊢ (if remaining✝ = 1 then (Counter.decrement (true :: bs), cs) else (true :: bs, cs)).1.length ≤ bs.length + 1 ∧
  (if remaining✝ = 1 then (Counter.decrement (true :: bs), cs) else (true :: bs, cs)).2.length ≤ cs.length + 1length.falsebs:List Boolcs:List Boolremaining✝:ℕvalue✝:ℕ⊢ (Counter.decrement bs).length ≤ bs.length + 1 ∧
  (if remaining✝ = 1 then Counter.decrement (false :: cs) else false :: cs).length ≤ cs.length + 1length.truebs:List Boolcs:List Boolremaining✝:ℕvalue✝:ℕ⊢ (Counter.decrement bs).length ≤ bs.length + 1 ∧
  (if remaining✝ = 1 then Counter.decrement (true :: cs) else true :: cs).length ≤ cs.length + 1payload.falsebs:List Boolcs:List Boolremaining✝:ℕ⊢ (if remaining✝ = 1 then ([], []) else (bs, Counter.decrement cs)).1.length ≤ bs.length + 1 ∧
  (if remaining✝ = 1 then ([], []) else (bs, Counter.decrement cs)).2.length ≤ cs.length + 1payload.truebs:List Boolcs:List Boolremaining✝:ℕ⊢ (if remaining✝ = 1 then ([], []) else (bs, Counter.decrement cs)).1.length ≤ bs.length + 1 ∧
  (if remaining✝ = 1 then ([], []) else (bs, Counter.decrement cs)).2.length ≤ cs.length + 1done.falsebs:List Boolcs:List Bool⊢ bs.length ≤ bs.length + 1 ∧ cs.length ≤ cs.length + 1done.truebs:List Boolcs:List Bool⊢ bs.length ≤ bs.length + 1 ∧ cs.length ≤ cs.length + 1dead.falsebs:List Boolcs:List Bool⊢ bs.length ≤ bs.length + 1 ∧ cs.length ≤ cs.length + 1dead.truebs:List Boolcs:List Bool⊢ bs.length ≤ bs.length + 1 ∧ cs.length ≤ cs.length + 1
    first | (constructordead.true.leftbs:List Boolcs:List Bool⊢ bs.length ≤ bs.length + 1dead.true.rightbs:List Boolcs:List Bool⊢ cs.length ≤ cs.length + 1 <;>dead.true.leftbs:List Boolcs:List Bool⊢ bs.length ≤ bs.length + 1dead.true.rightbs:List Boolcs:List Bool⊢ cs.length ≤ cs.length + 1 omegaAll goals completed! 🐙) |
      (splitpayload.true.isTruebs:List Boolcs:List Boolremaining✝:ℕh✝:remaining✝ = 1⊢ ([], []).1.length ≤ bs.length + 1 ∧ ([], []).2.length ≤ cs.length + 1payload.true.isFalsebs:List Boolcs:List Boolremaining✝:ℕh✝:¬remaining✝ = 1⊢ (bs, Counter.decrement cs).1.length ≤ bs.length + 1 ∧ (bs, Counter.decrement cs).2.length ≤ cs.length + 1 <;>payload.true.isTruebs:List Boolcs:List Boolremaining✝:ℕh✝:remaining✝ = 1⊢ ([], []).1.length ≤ bs.length + 1 ∧ ([], []).2.length ≤ cs.length + 1payload.true.isFalsebs:List Boolcs:List Boolremaining✝:ℕh✝:¬remaining✝ = 1⊢ (bs, Counter.decrement cs).1.length ≤ bs.length + 1 ∧ (bs, Counter.decrement cs).2.length ≤ cs.length + 1 constructorpayload.true.isFalse.leftbs:List Boolcs:List Boolremaining✝:ℕh✝:¬remaining✝ = 1⊢ (bs, Counter.decrement cs).1.length ≤ bs.length + 1payload.true.isFalse.rightbs:List Boolcs:List Boolremaining✝:ℕh✝:¬remaining✝ = 1⊢ (bs, Counter.decrement cs).2.length ≤ cs.length + 1 <;>payload.true.isTrue.leftbs:List Boolcs:List Boolremaining✝:ℕh✝:remaining✝ = 1⊢ ([], []).1.length ≤ bs.length + 1payload.true.isTrue.rightbs:List Boolcs:List Boolremaining✝:ℕh✝:remaining✝ = 1⊢ ([], []).2.length ≤ cs.length + 1payload.true.isFalse.leftbs:List Boolcs:List Boolremaining✝:ℕh✝:¬remaining✝ = 1⊢ (bs, Counter.decrement cs).1.length ≤ bs.length + 1payload.true.isFalse.rightbs:List Boolcs:List Boolremaining✝:ℕh✝:¬remaining✝ = 1⊢ (bs, Counter.decrement cs).2.length ≤ cs.length + 1 simp only [List.length_nil, List.length_cons,
        Counter.length_decrement]payload.true.isFalse.rightbs:List Boolcs:List Boolremaining✝:ℕh✝:¬remaining✝ = 1⊢ cs.length ≤ cs.length + 1 <;>payload.true.isTrue.leftbs:List Boolcs:List Boolremaining✝:ℕh✝:remaining✝ = 1⊢ 0 ≤ bs.length + 1payload.true.isTrue.rightbs:List Boolcs:List Boolremaining✝:ℕh✝:remaining✝ = 1⊢ 0 ≤ cs.length + 1payload.true.isFalse.leftbs:List Boolcs:List Boolremaining✝:ℕh✝:¬remaining✝ = 1⊢ bs.length ≤ bs.length + 1payload.true.isFalse.rightbs:List Boolcs:List Boolremaining✝:ℕh✝:¬remaining✝ = 1⊢ cs.length ≤ cs.length + 1 omegaAll goals completed! 🐙) |
      (constructortree.false.leftbs:List Boolcs:List Bool⊢ [].length ≤ bs.length + 1tree.false.rightbs:List Boolcs:List Bool⊢ [true].length ≤ cs.length + 1 <;>tree.false.leftbs:List Boolcs:List Bool⊢ [].length ≤ bs.length + 1tree.false.rightbs:List Boolcs:List Bool⊢ [true].length ≤ cs.length + 1 simp only [List.length_nil, List.length_cons]tree.false.rightbs:List Boolcs:List Bool⊢ 0 + 1 ≤ cs.length + 1 <;>tree.false.leftbs:List Boolcs:List Bool⊢ 0 ≤ bs.length + 1tree.false.rightbs:List Boolcs:List Bool⊢ 0 + 1 ≤ cs.length + 1 omegaAll goals completed! 🐙)

The unary header counter grows by at most one per input bit.

theorem step_zeros_le (s : Scanner.State) (b : Bool) :
    zeroCount (Scanner.step s b).1 ≤ zeroCount s.1 + 1 := bys:Scanner.Stateb:Bool⊢ zeroCount (Scanner.step s b).1 ≤ zeroCount s.1 + 1
  rcases s with ⟨m, n⟩b:Boolm:Scanner.Moden:ℕ⊢ zeroCount (Scanner.step (m, n) b).1 ≤ zeroCount (m, n).1 + 1
  cases mtreeb:Booln:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.tree, n) b).1 ≤ zeroCount (Scanner.Mode.tree, n).1 + 1zerosb:Booln:ℕcount✝:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.zeros count✝, n) b).1 ≤ zeroCount (Scanner.Mode.zeros count✝, n).1 + 1sizeb:Booln:ℕremaining✝:ℕvalue✝:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.size remaining✝ value✝, n) b).1 ≤
  zeroCount (Scanner.Mode.size remaining✝ value✝, n).1 + 1lengthb:Booln:ℕremaining✝:ℕvalue✝:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.length remaining✝ value✝, n) b).1 ≤
  zeroCount (Scanner.Mode.length remaining✝ value✝, n).1 + 1payloadb:Booln:ℕremaining✝:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.payload remaining✝, n) b).1 ≤ zeroCount (Scanner.Mode.payload remaining✝, n).1 + 1doneb:Booln:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.done, n) b).1 ≤ zeroCount (Scanner.Mode.done, n).1 + 1deadb:Booln:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.dead, n) b).1 ≤ zeroCount (Scanner.Mode.dead, n).1 + 1 <;>treeb:Booln:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.tree, n) b).1 ≤ zeroCount (Scanner.Mode.tree, n).1 + 1zerosb:Booln:ℕcount✝:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.zeros count✝, n) b).1 ≤ zeroCount (Scanner.Mode.zeros count✝, n).1 + 1sizeb:Booln:ℕremaining✝:ℕvalue✝:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.size remaining✝ value✝, n) b).1 ≤
  zeroCount (Scanner.Mode.size remaining✝ value✝, n).1 + 1lengthb:Booln:ℕremaining✝:ℕvalue✝:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.length remaining✝ value✝, n) b).1 ≤
  zeroCount (Scanner.Mode.length remaining✝ value✝, n).1 + 1payloadb:Booln:ℕremaining✝:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.payload remaining✝, n) b).1 ≤ zeroCount (Scanner.Mode.payload remaining✝, n).1 + 1doneb:Booln:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.done, n) b).1 ≤ zeroCount (Scanner.Mode.done, n).1 + 1deadb:Booln:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.dead, n) b).1 ≤ zeroCount (Scanner.Mode.dead, n).1 + 1 cases bdead.falsen:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.dead, n) false).1 ≤ zeroCount (Scanner.Mode.dead, n).1 + 1dead.truen:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.dead, n) true).1 ≤ zeroCount (Scanner.Mode.dead, n).1 + 1 <;>tree.falsen:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.tree, n) false).1 ≤ zeroCount (Scanner.Mode.tree, n).1 + 1tree.truen:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.tree, n) true).1 ≤ zeroCount (Scanner.Mode.tree, n).1 + 1zeros.falsen:ℕcount✝:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.zeros count✝, n) false).1 ≤ zeroCount (Scanner.Mode.zeros count✝, n).1 + 1zeros.truen:ℕcount✝:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.zeros count✝, n) true).1 ≤ zeroCount (Scanner.Mode.zeros count✝, n).1 + 1size.falsen:ℕremaining✝:ℕvalue✝:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.size remaining✝ value✝, n) false).1 ≤
  zeroCount (Scanner.Mode.size remaining✝ value✝, n).1 + 1size.truen:ℕremaining✝:ℕvalue✝:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.size remaining✝ value✝, n) true).1 ≤
  zeroCount (Scanner.Mode.size remaining✝ value✝, n).1 + 1length.falsen:ℕremaining✝:ℕvalue✝:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.length remaining✝ value✝, n) false).1 ≤
  zeroCount (Scanner.Mode.length remaining✝ value✝, n).1 + 1length.truen:ℕremaining✝:ℕvalue✝:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.length remaining✝ value✝, n) true).1 ≤
  zeroCount (Scanner.Mode.length remaining✝ value✝, n).1 + 1payload.falsen:ℕremaining✝:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.payload remaining✝, n) false).1 ≤
  zeroCount (Scanner.Mode.payload remaining✝, n).1 + 1payload.truen:ℕremaining✝:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.payload remaining✝, n) true).1 ≤
  zeroCount (Scanner.Mode.payload remaining✝, n).1 + 1done.falsen:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.done, n) false).1 ≤ zeroCount (Scanner.Mode.done, n).1 + 1done.truen:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.done, n) true).1 ≤ zeroCount (Scanner.Mode.done, n).1 + 1dead.falsen:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.dead, n) false).1 ≤ zeroCount (Scanner.Mode.dead, n).1 + 1dead.truen:ℕ⊢ zeroCount (Scanner.step (Scanner.Mode.dead, n) true).1 ≤ zeroCount (Scanner.Mode.dead, n).1 + 1 simp only [Scanner.step]dead.truen:ℕ⊢ zeroCount Scanner.Mode.dead ≤ zeroCount Scanner.Mode.dead + 1 <;>tree.falsen:ℕ⊢ zeroCount (Scanner.Mode.zeros 0) ≤ zeroCount Scanner.Mode.tree + 1tree.truen:ℕ⊢ zeroCount Scanner.Mode.tree ≤ zeroCount Scanner.Mode.tree + 1zeros.falsen:ℕcount✝:ℕ⊢ zeroCount (Scanner.Mode.zeros (count✝ + 1)) ≤ zeroCount (Scanner.Mode.zeros count✝) + 1zeros.truen:ℕcount✝:ℕ⊢ zeroCount (if count✝ = 0 then Scanner.finish n else (Scanner.Mode.size count✝ 1, n)).1 ≤
  zeroCount (Scanner.Mode.zeros count✝) + 1size.falsen:ℕremaining✝:ℕvalue✝:ℕ⊢ zeroCount
    (if remaining✝ = 1 then (Scanner.Mode.length (Nat.bit false value✝ - 1) 1, n)
      else (Scanner.Mode.size (remaining✝ - 1) (Nat.bit false value✝), n)).1 ≤
  zeroCount (Scanner.Mode.size remaining✝ value✝) + 1size.truen:ℕremaining✝:ℕvalue✝:ℕ⊢ zeroCount
    (if remaining✝ = 1 then (Scanner.Mode.length (Nat.bit true value✝ - 1) 1, n)
      else (Scanner.Mode.size (remaining✝ - 1) (Nat.bit true value✝), n)).1 ≤
  zeroCount (Scanner.Mode.size remaining✝ value✝) + 1length.falsen:ℕremaining✝:ℕvalue✝:ℕ⊢ zeroCount
    (if remaining✝ = 1 then (Scanner.Mode.payload (Nat.bit false value✝ - 1), n)
      else (Scanner.Mode.length (remaining✝ - 1) (Nat.bit false value✝), n)).1 ≤
  zeroCount (Scanner.Mode.length remaining✝ value✝) + 1length.truen:ℕremaining✝:ℕvalue✝:ℕ⊢ zeroCount
    (if remaining✝ = 1 then (Scanner.Mode.payload (Nat.bit true value✝ - 1), n)
      else (Scanner.Mode.length (remaining✝ - 1) (Nat.bit true value✝), n)).1 ≤
  zeroCount (Scanner.Mode.length remaining✝ value✝) + 1payload.falsen:ℕremaining✝:ℕ⊢ zeroCount (if remaining✝ = 1 then Scanner.finish n else (Scanner.Mode.payload (remaining✝ - 1), n)).1 ≤
  zeroCount (Scanner.Mode.payload remaining✝) + 1payload.truen:ℕremaining✝:ℕ⊢ zeroCount (if remaining✝ = 1 then Scanner.finish n else (Scanner.Mode.payload (remaining✝ - 1), n)).1 ≤
  zeroCount (Scanner.Mode.payload remaining✝) + 1done.falsen:ℕ⊢ zeroCount Scanner.Mode.dead ≤ zeroCount Scanner.Mode.done + 1done.truen:ℕ⊢ zeroCount Scanner.Mode.dead ≤ zeroCount Scanner.Mode.done + 1dead.falsen:ℕ⊢ zeroCount Scanner.Mode.dead ≤ zeroCount Scanner.Mode.dead + 1dead.truen:ℕ⊢ zeroCount Scanner.Mode.dead ≤ zeroCount Scanner.Mode.dead + 1
    first | (simp only [zeroCount]dead.truen:ℕ⊢ 0 ≤ 0 + 1; omegaAll goals completed! 🐙) |
      (splitpayload.true.isTruen:ℕremaining✝:ℕh✝:remaining✝ = 1⊢ zeroCount (Scanner.finish n).1 ≤ zeroCount (Scanner.Mode.payload remaining✝) + 1payload.true.isFalsen:ℕremaining✝:ℕh✝:¬remaining✝ = 1⊢ zeroCount (Scanner.Mode.payload (remaining✝ - 1), n).1 ≤ zeroCount (Scanner.Mode.payload remaining✝) + 1 <;>payload.true.isTruen:ℕremaining✝:ℕh✝:remaining✝ = 1⊢ zeroCount (Scanner.finish n).1 ≤ zeroCount (Scanner.Mode.payload remaining✝) + 1payload.true.isFalsen:ℕremaining✝:ℕh✝:¬remaining✝ = 1⊢ zeroCount (Scanner.Mode.payload (remaining✝ - 1), n).1 ≤ zeroCount (Scanner.Mode.payload remaining✝) + 1 first | (simp only [zeroCount]payload.true.isFalsen:ℕremaining✝:ℕh✝:¬remaining✝ = 1⊢ 0 ≤ 0 + 1; omegaAll goals completed! 🐙) |
        (unfold Scanner.finishpayload.true.isTruen:ℕremaining✝:ℕh✝:remaining✝ = 1⊢ zeroCount (if n = 1 then (Scanner.Mode.done, 0) else (Scanner.Mode.tree, n - 1)).1 ≤
  zeroCount (Scanner.Mode.payload remaining✝) + 1; splitpayload.true.isTrue.isTruen:ℕremaining✝:ℕh✝¹:remaining✝ = 1h✝:n = 1⊢ zeroCount (Scanner.Mode.done, 0).1 ≤ zeroCount (Scanner.Mode.payload remaining✝) + 1payload.true.isTrue.isFalsen:ℕremaining✝:ℕh✝¹:remaining✝ = 1h✝:¬n = 1⊢ zeroCount (Scanner.Mode.tree, n - 1).1 ≤ zeroCount (Scanner.Mode.payload remaining✝) + 1 <;>payload.true.isTrue.isTruen:ℕremaining✝:ℕh✝¹:remaining✝ = 1h✝:n = 1⊢ zeroCount (Scanner.Mode.done, 0).1 ≤ zeroCount (Scanner.Mode.payload remaining✝) + 1payload.true.isTrue.isFalsen:ℕremaining✝:ℕh✝¹:remaining✝ = 1h✝:¬n = 1⊢ zeroCount (Scanner.Mode.tree, n - 1).1 ≤ zeroCount (Scanner.Mode.payload remaining✝) + 1 simp only [zeroCount]payload.true.isTrue.isFalsen:ℕremaining✝:ℕh✝¹:remaining✝ = 1h✝:¬n = 1⊢ 0 ≤ 0 + 1 <;>payload.true.isTrue.isTruen:ℕremaining✝:ℕh✝¹:remaining✝ = 1h✝:n = 1⊢ 0 ≤ 0 + 1payload.true.isTrue.isFalsen:ℕremaining✝:ℕh✝¹:remaining✝ = 1h✝:¬n = 1⊢ 0 ≤ 0 + 1 omegaAll goals completed! 🐙))

Any suffix adds at most its length to both word widths and the unary header counter.

theorem account_foldl_bounds (w : List Bool) : ∀ s,
    (w.foldl accountStep s).2.1.length ≤ s.2.1.length + w.length ∧
    (w.foldl accountStep s).2.2.length ≤ s.2.2.length + w.length ∧
    zeroCount (w.foldl accountStep s).1.1 ≤ zeroCount s.1.1 + w.length :=
  List.rec (fun s ↦ ⟨Nat.le_refl _, Nat.le_refl _, Nat.le_refl _⟩)
    (fun b bs ih s ↦ byw:List Boolb:Boolbs:List Boolih:∀ (s : Account),
  (List.foldl accountStep s bs).2.1.length ≤ s.2.1.length + bs.length ∧
    (List.foldl accountStep s bs).2.2.length ≤ s.2.2.length + bs.length ∧
      zeroCount (List.foldl accountStep s bs).1.1 ≤ zeroCount s.1.1 + bs.lengths:Account⊢ (List.foldl accountStep s (b :: bs)).2.1.length ≤ s.2.1.length + (b :: bs).length ∧
  (List.foldl accountStep s (b :: bs)).2.2.length ≤ s.2.2.length + (b :: bs).length ∧
    zeroCount (List.foldl accountStep s (b :: bs)).1.1 ≤ zeroCount s.1.1 + (b :: bs).length
      obtain ⟨hb, hc, hz⟩ := ih (accountStep s b)w:List Boolb:Boolbs:List Boolih:∀ (s : Account),
  (List.foldl accountStep s bs).2.1.length ≤ s.2.1.length + bs.length ∧
    (List.foldl accountStep s bs).2.2.length ≤ s.2.2.length + bs.length ∧
      zeroCount (List.foldl accountStep s bs).1.1 ≤ zeroCount s.1.1 + bs.lengths:Accounthb:(List.foldl accountStep (accountStep s b) bs).2.1.length ≤ (accountStep s b).2.1.length + bs.lengthhc:(List.foldl accountStep (accountStep s b) bs).2.2.length ≤ (accountStep s b).2.2.length + bs.lengthhz:zeroCount (List.foldl accountStep (accountStep s b) bs).1.1 ≤ zeroCount (accountStep s b).1.1 + bs.length⊢ (List.foldl accountStep s (b :: bs)).2.1.length ≤ s.2.1.length + (b :: bs).length ∧
  (List.foldl accountStep s (b :: bs)).2.2.length ≤ s.2.2.length + (b :: bs).length ∧
    zeroCount (List.foldl accountStep s (b :: bs)).1.1 ≤ zeroCount s.1.1 + (b :: bs).length
      obtain ⟨hbs, hcs⟩ := nextWords_lengths_le s.1.1 s.2.1 s.2.2 bw:List Boolb:Boolbs:List Boolih:∀ (s : Account),
  (List.foldl accountStep s bs).2.1.length ≤ s.2.1.length + bs.length ∧
    (List.foldl accountStep s bs).2.2.length ≤ s.2.2.length + bs.length ∧
      zeroCount (List.foldl accountStep s bs).1.1 ≤ zeroCount s.1.1 + bs.lengths:Accounthb:(List.foldl accountStep (accountStep s b) bs).2.1.length ≤ (accountStep s b).2.1.length + bs.lengthhc:(List.foldl accountStep (accountStep s b) bs).2.2.length ≤ (accountStep s b).2.2.length + bs.lengthhz:zeroCount (List.foldl accountStep (accountStep s b) bs).1.1 ≤ zeroCount (accountStep s b).1.1 + bs.lengthhbs:(nextWords s.1.1 s.2.1 s.2.2 b).1.length ≤ s.2.1.length + 1hcs:(nextWords s.1.1 s.2.1 s.2.2 b).2.length ≤ s.2.2.length + 1⊢ (List.foldl accountStep s (b :: bs)).2.1.length ≤ s.2.1.length + (b :: bs).length ∧
  (List.foldl accountStep s (b :: bs)).2.2.length ≤ s.2.2.length + (b :: bs).length ∧
    zeroCount (List.foldl accountStep s (b :: bs)).1.1 ≤ zeroCount s.1.1 + (b :: bs).length
      have hzs := step_zeros_le s.1 bw:List Boolb:Boolbs:List Boolih:∀ (s : Account),
  (List.foldl accountStep s bs).2.1.length ≤ s.2.1.length + bs.length ∧
    (List.foldl accountStep s bs).2.2.length ≤ s.2.2.length + bs.length ∧
      zeroCount (List.foldl accountStep s bs).1.1 ≤ zeroCount s.1.1 + bs.lengths:Accounthb:(List.foldl accountStep (accountStep s b) bs).2.1.length ≤ (accountStep s b).2.1.length + bs.lengthhc:(List.foldl accountStep (accountStep s b) bs).2.2.length ≤ (accountStep s b).2.2.length + bs.lengthhz:zeroCount (List.foldl accountStep (accountStep s b) bs).1.1 ≤ zeroCount (accountStep s b).1.1 + bs.lengthhbs:(nextWords s.1.1 s.2.1 s.2.2 b).1.length ≤ s.2.1.length + 1hcs:(nextWords s.1.1 s.2.1 s.2.2 b).2.length ≤ s.2.2.length + 1hzs:zeroCount (Scanner.step s.1 b).1 ≤ zeroCount s.1.1 + 1⊢ (List.foldl accountStep s (b :: bs)).2.1.length ≤ s.2.1.length + (b :: bs).length ∧
  (List.foldl accountStep s (b :: bs)).2.2.length ≤ s.2.2.length + (b :: bs).length ∧
    zeroCount (List.foldl accountStep s (b :: bs)).1.1 ≤ zeroCount s.1.1 + (b :: bs).length
      simp only [List.foldl_cons, List.length_cons]w:List Boolb:Boolbs:List Boolih:∀ (s : Account),
  (List.foldl accountStep s bs).2.1.length ≤ s.2.1.length + bs.length ∧
    (List.foldl accountStep s bs).2.2.length ≤ s.2.2.length + bs.length ∧
      zeroCount (List.foldl accountStep s bs).1.1 ≤ zeroCount s.1.1 + bs.lengths:Accounthb:(List.foldl accountStep (accountStep s b) bs).2.1.length ≤ (accountStep s b).2.1.length + bs.lengthhc:(List.foldl accountStep (accountStep s b) bs).2.2.length ≤ (accountStep s b).2.2.length + bs.lengthhz:zeroCount (List.foldl accountStep (accountStep s b) bs).1.1 ≤ zeroCount (accountStep s b).1.1 + bs.lengthhbs:(nextWords s.1.1 s.2.1 s.2.2 b).1.length ≤ s.2.1.length + 1hcs:(nextWords s.1.1 s.2.1 s.2.2 b).2.length ≤ s.2.2.length + 1hzs:zeroCount (Scanner.step s.1 b).1 ≤ zeroCount s.1.1 + 1⊢ (List.foldl accountStep (accountStep s b) bs).2.1.length ≤ s.2.1.length + (bs.length + 1) ∧
  (List.foldl accountStep (accountStep s b) bs).2.2.length ≤ s.2.2.length + (bs.length + 1) ∧
    zeroCount (List.foldl accountStep (accountStep s b) bs).1.1 ≤ zeroCount s.1.1 + (bs.length + 1)
      change _ ≤ _ at hb hc hzw:List Boolb:Boolbs:List Boolih:∀ (s : Account),
  (List.foldl accountStep s bs).2.1.length ≤ s.2.1.length + bs.length ∧
    (List.foldl accountStep s bs).2.2.length ≤ s.2.2.length + bs.length ∧
      zeroCount (List.foldl accountStep s bs).1.1 ≤ zeroCount s.1.1 + bs.lengths:Accounthbs:(nextWords s.1.1 s.2.1 s.2.2 b).1.length ≤ s.2.1.length + 1hcs:(nextWords s.1.1 s.2.1 s.2.2 b).2.length ≤ s.2.2.length + 1hzs:zeroCount (Scanner.step s.1 b).1 ≤ zeroCount s.1.1 + 1hb:(List.foldl accountStep (accountStep s b) bs).2.1.length ≤ (accountStep s b).2.1.length + bs.lengthhc:(List.foldl accountStep (accountStep s b) bs).2.2.length ≤ (accountStep s b).2.2.length + bs.lengthhz:zeroCount (List.foldl accountStep (accountStep s b) bs).1.1 ≤ zeroCount (accountStep s b).1.1 + bs.length⊢ (List.foldl accountStep (accountStep s b) bs).2.1.length ≤ s.2.1.length + (bs.length + 1) ∧
  (List.foldl accountStep (accountStep s b) bs).2.2.length ≤ s.2.2.length + (bs.length + 1) ∧
    zeroCount (List.foldl accountStep (accountStep s b) bs).1.1 ≤ zeroCount s.1.1 + (bs.length + 1)
      dsimp only [accountStep] at hb hc hz ⊢w:List Boolb:Boolbs:List Boolih:∀ (s : Account),
  (List.foldl accountStep s bs).2.1.length ≤ s.2.1.length + bs.length ∧
    (List.foldl accountStep s bs).2.2.length ≤ s.2.2.length + bs.length ∧
      zeroCount (List.foldl accountStep s bs).1.1 ≤ zeroCount s.1.1 + bs.lengths:Accounthbs:(nextWords s.1.1 s.2.1 s.2.2 b).1.length ≤ s.2.1.length + 1hcs:(nextWords s.1.1 s.2.1 s.2.2 b).2.length ≤ s.2.2.length + 1hzs:zeroCount (Scanner.step s.1 b).1 ≤ zeroCount s.1.1 + 1hb:(List.foldl accountStep (Scanner.step s.1 b, nextWords s.1.1 s.2.1 s.2.2 b) bs).2.1.length ≤
  (nextWords s.1.1 s.2.1 s.2.2 b).1.length + bs.lengthhc:(List.foldl accountStep (Scanner.step s.1 b, nextWords s.1.1 s.2.1 s.2.2 b) bs).2.2.length ≤
  (nextWords s.1.1 s.2.1 s.2.2 b).2.length + bs.lengthhz:zeroCount (List.foldl accountStep (Scanner.step s.1 b, nextWords s.1.1 s.2.1 s.2.2 b) bs).1.1 ≤
  zeroCount (Scanner.step s.1 b).1 + bs.length⊢ (List.foldl accountStep (Scanner.step s.1 b, nextWords s.1.1 s.2.1 s.2.2 b) bs).2.1.length ≤
    s.2.1.length + (bs.length + 1) ∧
  (List.foldl accountStep (Scanner.step s.1 b, nextWords s.1.1 s.2.1 s.2.2 b) bs).2.2.length ≤
      s.2.2.length + (bs.length + 1) ∧
    zeroCount (List.foldl accountStep (Scanner.step s.1 b, nextWords s.1.1 s.2.1 s.2.2 b) bs).1.1 ≤
      zeroCount s.1.1 + (bs.length + 1)
      exact ⟨byw:List Boolb:Boolbs:List Boolih:∀ (s : Account),
  (List.foldl accountStep s bs).2.1.length ≤ s.2.1.length + bs.length ∧
    (List.foldl accountStep s bs).2.2.length ≤ s.2.2.length + bs.length ∧
      zeroCount (List.foldl accountStep s bs).1.1 ≤ zeroCount s.1.1 + bs.lengths:Accounthbs:(nextWords s.1.1 s.2.1 s.2.2 b).1.length ≤ s.2.1.length + 1hcs:(nextWords s.1.1 s.2.1 s.2.2 b).2.length ≤ s.2.2.length + 1hzs:zeroCount (Scanner.step s.1 b).1 ≤ zeroCount s.1.1 + 1hb:(List.foldl accountStep (Scanner.step s.1 b, nextWords s.1.1 s.2.1 s.2.2 b) bs).2.1.length ≤
  (nextWords s.1.1 s.2.1 s.2.2 b).1.length + bs.lengthhc:(List.foldl accountStep (Scanner.step s.1 b, nextWords s.1.1 s.2.1 s.2.2 b) bs).2.2.length ≤
  (nextWords s.1.1 s.2.1 s.2.2 b).2.length + bs.lengthhz:zeroCount (List.foldl accountStep (Scanner.step s.1 b, nextWords s.1.1 s.2.1 s.2.2 b) bs).1.1 ≤
  zeroCount (Scanner.step s.1 b).1 + bs.length⊢ (List.foldl accountStep (Scanner.step s.1 b, nextWords s.1.1 s.2.1 s.2.2 b) bs).2.1.length ≤
  s.2.1.length + (bs.length + 1) omegaAll goals completed! 🐙, byw:List Boolb:Boolbs:List Boolih:∀ (s : Account),
  (List.foldl accountStep s bs).2.1.length ≤ s.2.1.length + bs.length ∧
    (List.foldl accountStep s bs).2.2.length ≤ s.2.2.length + bs.length ∧
      zeroCount (List.foldl accountStep s bs).1.1 ≤ zeroCount s.1.1 + bs.lengths:Accounthbs:(nextWords s.1.1 s.2.1 s.2.2 b).1.length ≤ s.2.1.length + 1hcs:(nextWords s.1.1 s.2.1 s.2.2 b).2.length ≤ s.2.2.length + 1hzs:zeroCount (Scanner.step s.1 b).1 ≤ zeroCount s.1.1 + 1hb:(List.foldl accountStep (Scanner.step s.1 b, nextWords s.1.1 s.2.1 s.2.2 b) bs).2.1.length ≤
  (nextWords s.1.1 s.2.1 s.2.2 b).1.length + bs.lengthhc:(List.foldl accountStep (Scanner.step s.1 b, nextWords s.1.1 s.2.1 s.2.2 b) bs).2.2.length ≤
  (nextWords s.1.1 s.2.1 s.2.2 b).2.length + bs.lengthhz:zeroCount (List.foldl accountStep (Scanner.step s.1 b, nextWords s.1.1 s.2.1 s.2.2 b) bs).1.1 ≤
  zeroCount (Scanner.step s.1 b).1 + bs.length⊢ (List.foldl accountStep (Scanner.step s.1 b, nextWords s.1.1 s.2.1 s.2.2 b) bs).2.2.length ≤
  s.2.2.length + (bs.length + 1) omegaAll goals completed! 🐙, byw:List Boolb:Boolbs:List Boolih:∀ (s : Account),
  (List.foldl accountStep s bs).2.1.length ≤ s.2.1.length + bs.length ∧
    (List.foldl accountStep s bs).2.2.length ≤ s.2.2.length + bs.length ∧
      zeroCount (List.foldl accountStep s bs).1.1 ≤ zeroCount s.1.1 + bs.lengths:Accounthbs:(nextWords s.1.1 s.2.1 s.2.2 b).1.length ≤ s.2.1.length + 1hcs:(nextWords s.1.1 s.2.1 s.2.2 b).2.length ≤ s.2.2.length + 1hzs:zeroCount (Scanner.step s.1 b).1 ≤ zeroCount s.1.1 + 1hb:(List.foldl accountStep (Scanner.step s.1 b, nextWords s.1.1 s.2.1 s.2.2 b) bs).2.1.length ≤
  (nextWords s.1.1 s.2.1 s.2.2 b).1.length + bs.lengthhc:(List.foldl accountStep (Scanner.step s.1 b, nextWords s.1.1 s.2.1 s.2.2 b) bs).2.2.length ≤
  (nextWords s.1.1 s.2.1 s.2.2 b).2.length + bs.lengthhz:zeroCount (List.foldl accountStep (Scanner.step s.1 b, nextWords s.1.1 s.2.1 s.2.2 b) bs).1.1 ≤
  zeroCount (Scanner.step s.1 b).1 + bs.length⊢ zeroCount (List.foldl accountStep (Scanner.step s.1 b, nextWords s.1.1 s.2.1 s.2.2 b) bs).1.1 ≤
  zeroCount s.1.1 + (bs.length + 1) omegaAll goals completed! 🐙⟩) w

Each binary field uses at most the input length.

theorem account_lengths_le (w : List Bool) :
    (account w).2.1.length ≤ w.length ∧ (account w).2.2.length ≤ w.length := byw:List Bool⊢ (account w).2.1.length ≤ w.length ∧ (account w).2.2.length ≤ w.length
  obtain ⟨hb, hc, _⟩ := account_foldl_bounds w initialAccountw:List Boolhb:(List.foldl accountStep initialAccount w).2.1.length ≤ initialAccount.2.1.length + w.lengthhc:(List.foldl accountStep initialAccount w).2.2.length ≤ initialAccount.2.2.length + w.lengthright✝:zeroCount (List.foldl accountStep initialAccount w).1.1 ≤ zeroCount initialAccount.1.1 + w.length⊢ (account w).2.1.length ≤ w.length ∧ (account w).2.2.length ≤ w.length
  simpa only [account, initialAccount, List.length_nil, Nat.zero_add] using And.intro hb hcAll goals completed! 🐙

The unary header counter is bounded by the input length.

theorem account_zeros_le (w : List Bool) : zeroCount (account w).1.1 ≤ w.length := byw:List Bool⊢ zeroCount (account w).1.1 ≤ w.length
  simpa only [account, initialAccount, zeroCount, Nat.zero_add] using
    (account_foldl_bounds w initialAccount).2.2All goals completed! 🐙

Pending subtrees use at most one plus the input length.

theorem account_pending_le (w : List Bool) : (account w).1.2 ≤ w.length + 1 := byw:List Bool⊢ (account w).1.2 ≤ w.length + 1
  rw [account_projectw:List Bool⊢ (Scanner.scan w).2 ≤ w.length + 1]w:List Bool⊢ (Scanner.scan w).2 ≤ w.length + 1
  exact Scanner.scan_pending_le wAll goals completed! 🐙

Appending one bit advances the account once.

theorem account_append (w : List Bool) (b : Bool) :
    account (w ++ [b]) = accountStep (account w) b := byw:List Boolb:Bool⊢ account (w ++ [b]) = accountStep (account w) b
  simp only [account, List.foldl_append, List.foldl_cons, List.foldl_nil]All goals completed! 🐙

Machine time for one complete input transition.

def macroCost (s : Account) (b : Bool) : ℕ := bitCost s.1.1 s.2.1 s.2.2 b

Advance the account while accumulating machine time.

def costStep (s : Account × ℕ) (b : Bool) : Account × ℕ :=
  (accountStep s.1 b, s.2 + macroCost s.1 b)

Time accounting leaves the account projection unchanged.

theorem cost_foldl_fst (w : List Bool) : ∀ s c,
    (w.foldl costStep (s, c)).1 = w.foldl accountStep s :=
  List.rec (fun _ _ ↦ rfl) (fun b _ ih s c ↦ ih (accountStep s b) (c + macroCost s b)) w

Total transition time before the final end-marker decision.

def runCost (w : List Bool) : ℕ := (w.foldl costStep (initialAccount, 0)).2

Appending one input bit adds its exact macro cost.

theorem runCost_append (w : List Bool) (b : Bool) :
    runCost (w ++ [b]) = runCost w + macroCost (account w) b := byw:List Boolb:Bool⊢ runCost (w ++ [b]) = runCost w + macroCost (account w) b
  simp only [runCost, List.foldl_append, List.foldl_cons, List.foldl_nil, costStep,
    cost_foldl_fst, account]All goals completed! 🐙

A width bound gives a uniform linear bound for one macro transition.

theorem bitCost_le (m : Scanner.Mode) (bs cs : List Bool) (b : Bool) (width : ℕ)
    (hb : bs.length ≤ width) (hc : cs.length ≤ width) :
    bitCost m bs cs b ≤ 5 * width + 16 := bym:Scanner.Modebs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ bitCost m bs cs b ≤ 5 * width + 16
  cases mtreebs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ bitCost Scanner.Mode.tree bs cs b ≤ 5 * width + 16zerosbs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthcount✝:ℕ⊢ bitCost (Scanner.Mode.zeros count✝) bs cs b ≤ 5 * width + 16sizebs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕvalue✝:ℕ⊢ bitCost (Scanner.Mode.size remaining✝ value✝) bs cs b ≤ 5 * width + 16lengthbs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕvalue✝:ℕ⊢ bitCost (Scanner.Mode.length remaining✝ value✝) bs cs b ≤ 5 * width + 16payloadbs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕ⊢ bitCost (Scanner.Mode.payload remaining✝) bs cs b ≤ 5 * width + 16donebs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ bitCost Scanner.Mode.done bs cs b ≤ 5 * width + 16deadbs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ bitCost Scanner.Mode.dead bs cs b ≤ 5 * width + 16 <;>treebs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ bitCost Scanner.Mode.tree bs cs b ≤ 5 * width + 16zerosbs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthcount✝:ℕ⊢ bitCost (Scanner.Mode.zeros count✝) bs cs b ≤ 5 * width + 16sizebs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕvalue✝:ℕ⊢ bitCost (Scanner.Mode.size remaining✝ value✝) bs cs b ≤ 5 * width + 16lengthbs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕvalue✝:ℕ⊢ bitCost (Scanner.Mode.length remaining✝ value✝) bs cs b ≤ 5 * width + 16payloadbs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕ⊢ bitCost (Scanner.Mode.payload remaining✝) bs cs b ≤ 5 * width + 16donebs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ bitCost Scanner.Mode.done bs cs b ≤ 5 * width + 16deadbs:List Boolcs:List Boolb:Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ bitCost Scanner.Mode.dead bs cs b ≤ 5 * width + 16 cases bdead.falsebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ bitCost Scanner.Mode.dead bs cs false ≤ 5 * width + 16dead.truebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ bitCost Scanner.Mode.dead bs cs true ≤ 5 * width + 16 <;>tree.falsebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ bitCost Scanner.Mode.tree bs cs false ≤ 5 * width + 16tree.truebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ bitCost Scanner.Mode.tree bs cs true ≤ 5 * width + 16zeros.falsebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthcount✝:ℕ⊢ bitCost (Scanner.Mode.zeros count✝) bs cs false ≤ 5 * width + 16zeros.truebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthcount✝:ℕ⊢ bitCost (Scanner.Mode.zeros count✝) bs cs true ≤ 5 * width + 16size.falsebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕvalue✝:ℕ⊢ bitCost (Scanner.Mode.size remaining✝ value✝) bs cs false ≤ 5 * width + 16size.truebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕvalue✝:ℕ⊢ bitCost (Scanner.Mode.size remaining✝ value✝) bs cs true ≤ 5 * width + 16length.falsebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕvalue✝:ℕ⊢ bitCost (Scanner.Mode.length remaining✝ value✝) bs cs false ≤ 5 * width + 16length.truebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕvalue✝:ℕ⊢ bitCost (Scanner.Mode.length remaining✝ value✝) bs cs true ≤ 5 * width + 16payload.falsebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕ⊢ bitCost (Scanner.Mode.payload remaining✝) bs cs false ≤ 5 * width + 16payload.truebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕ⊢ bitCost (Scanner.Mode.payload remaining✝) bs cs true ≤ 5 * width + 16done.falsebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ bitCost Scanner.Mode.done bs cs false ≤ 5 * width + 16done.truebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ bitCost Scanner.Mode.done bs cs true ≤ 5 * width + 16dead.falsebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ bitCost Scanner.Mode.dead bs cs false ≤ 5 * width + 16dead.truebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ bitCost Scanner.Mode.dead bs cs true ≤ 5 * width + 16 simp only [bitCost]dead.truebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ 1 ≤ 5 * width + 16 <;>tree.falsebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ 1 ≤ 5 * width + 16tree.truebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ 1 ≤ 5 * width + 16zeros.falsebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthcount✝:ℕ⊢ 1 ≤ 5 * width + 16zeros.truebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthcount✝:ℕ⊢ (if count✝ = 0 then 16 else 2) ≤ 5 * width + 16size.falsebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕvalue✝:ℕ⊢ (if remaining✝ = 1 then 2 * bs.length + 7 else 2) ≤ 5 * width + 16size.truebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕvalue✝:ℕ⊢ (if remaining✝ = 1 then 2 * bs.length + 7 else 2) ≤ 5 * width + 16length.falsebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕvalue✝:ℕ⊢ (if remaining✝ = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4) ≤ 5 * width + 16length.truebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕvalue✝:ℕ⊢ (if remaining✝ = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4) ≤ 5 * width + 16payload.falsebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕ⊢ (if remaining✝ = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) ≤ 5 * width + 16payload.truebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕ⊢ (if remaining✝ = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4) ≤ 5 * width + 16done.falsebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ 1 ≤ 5 * width + 16done.truebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ 1 ≤ 5 * width + 16dead.falsebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ 1 ≤ 5 * width + 16dead.truebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ width⊢ 1 ≤ 5 * width + 16
    first | omegaAll goals completed! 🐙 | (splitpayload.true.isTruebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕh✝:remaining✝ = 1⊢ 2 * cs.length + max bs.length cs.length + 7 ≤ 5 * width + 16payload.true.isFalsebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕh✝:¬remaining✝ = 1⊢ 2 * cs.length + 4 ≤ 5 * width + 16 <;>payload.true.isTruebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕh✝:remaining✝ = 1⊢ 2 * cs.length + max bs.length cs.length + 7 ≤ 5 * width + 16payload.true.isFalsebs:List Boolcs:List Boolwidth:ℕhb:bs.length ≤ widthhc:cs.length ≤ widthremaining✝:ℕh✝:¬remaining✝ = 1⊢ 2 * cs.length + 4 ≤ 5 * width + 16 omegaAll goals completed! 🐙)

Every transition cost is positive.

theorem macroCost_pos (s : Account) (b : Bool) : 0 < macroCost s b := bys:Accountb:Bool⊢ 0 < macroCost s b
  rcases s with ⟨⟨m, n⟩, bs, cs⟩b:Boolm:Scanner.Moden:ℕbs:List Boolcs:List Bool⊢ 0 < macroCost ((m, n), bs, cs) b
  cases mtreeb:Booln:ℕbs:List Boolcs:List Bool⊢ 0 < macroCost ((Scanner.Mode.tree, n), bs, cs) bzerosb:Booln:ℕbs:List Boolcs:List Boolcount✝:ℕ⊢ 0 < macroCost ((Scanner.Mode.zeros count✝, n), bs, cs) bsizeb:Booln:ℕbs:List Boolcs:List Boolremaining✝:ℕvalue✝:ℕ⊢ 0 < macroCost ((Scanner.Mode.size remaining✝ value✝, n), bs, cs) blengthb:Booln:ℕbs:List Boolcs:List Boolremaining✝:ℕvalue✝:ℕ⊢ 0 < macroCost ((Scanner.Mode.length remaining✝ value✝, n), bs, cs) bpayloadb:Booln:ℕbs:List Boolcs:List Boolremaining✝:ℕ⊢ 0 < macroCost ((Scanner.Mode.payload remaining✝, n), bs, cs) bdoneb:Booln:ℕbs:List Boolcs:List Bool⊢ 0 < macroCost ((Scanner.Mode.done, n), bs, cs) bdeadb:Booln:ℕbs:List Boolcs:List Bool⊢ 0 < macroCost ((Scanner.Mode.dead, n), bs, cs) b <;>treeb:Booln:ℕbs:List Boolcs:List Bool⊢ 0 < macroCost ((Scanner.Mode.tree, n), bs, cs) bzerosb:Booln:ℕbs:List Boolcs:List Boolcount✝:ℕ⊢ 0 < macroCost ((Scanner.Mode.zeros count✝, n), bs, cs) bsizeb:Booln:ℕbs:List Boolcs:List Boolremaining✝:ℕvalue✝:ℕ⊢ 0 < macroCost ((Scanner.Mode.size remaining✝ value✝, n), bs, cs) blengthb:Booln:ℕbs:List Boolcs:List Boolremaining✝:ℕvalue✝:ℕ⊢ 0 < macroCost ((Scanner.Mode.length remaining✝ value✝, n), bs, cs) bpayloadb:Booln:ℕbs:List Boolcs:List Boolremaining✝:ℕ⊢ 0 < macroCost ((Scanner.Mode.payload remaining✝, n), bs, cs) bdoneb:Booln:ℕbs:List Boolcs:List Bool⊢ 0 < macroCost ((Scanner.Mode.done, n), bs, cs) bdeadb:Booln:ℕbs:List Boolcs:List Bool⊢ 0 < macroCost ((Scanner.Mode.dead, n), bs, cs) b cases bdead.falsen:ℕbs:List Boolcs:List Bool⊢ 0 < macroCost ((Scanner.Mode.dead, n), bs, cs) falsedead.truen:ℕbs:List Boolcs:List Bool⊢ 0 < macroCost ((Scanner.Mode.dead, n), bs, cs) true <;>tree.falsen:ℕbs:List Boolcs:List Bool⊢ 0 < macroCost ((Scanner.Mode.tree, n), bs, cs) falsetree.truen:ℕbs:List Boolcs:List Bool⊢ 0 < macroCost ((Scanner.Mode.tree, n), bs, cs) truezeros.falsen:ℕbs:List Boolcs:List Boolcount✝:ℕ⊢ 0 < macroCost ((Scanner.Mode.zeros count✝, n), bs, cs) falsezeros.truen:ℕbs:List Boolcs:List Boolcount✝:ℕ⊢ 0 < macroCost ((Scanner.Mode.zeros count✝, n), bs, cs) truesize.falsen:ℕbs:List Boolcs:List Boolremaining✝:ℕvalue✝:ℕ⊢ 0 < macroCost ((Scanner.Mode.size remaining✝ value✝, n), bs, cs) falsesize.truen:ℕbs:List Boolcs:List Boolremaining✝:ℕvalue✝:ℕ⊢ 0 < macroCost ((Scanner.Mode.size remaining✝ value✝, n), bs, cs) truelength.falsen:ℕbs:List Boolcs:List Boolremaining✝:ℕvalue✝:ℕ⊢ 0 < macroCost ((Scanner.Mode.length remaining✝ value✝, n), bs, cs) falselength.truen:ℕbs:List Boolcs:List Boolremaining✝:ℕvalue✝:ℕ⊢ 0 < macroCost ((Scanner.Mode.length remaining✝ value✝, n), bs, cs) truepayload.falsen:ℕbs:List Boolcs:List Boolremaining✝:ℕ⊢ 0 < macroCost ((Scanner.Mode.payload remaining✝, n), bs, cs) falsepayload.truen:ℕbs:List Boolcs:List Boolremaining✝:ℕ⊢ 0 < macroCost ((Scanner.Mode.payload remaining✝, n), bs, cs) truedone.falsen:ℕbs:List Boolcs:List Bool⊢ 0 < macroCost ((Scanner.Mode.done, n), bs, cs) falsedone.truen:ℕbs:List Boolcs:List Bool⊢ 0 < macroCost ((Scanner.Mode.done, n), bs, cs) truedead.falsen:ℕbs:List Boolcs:List Bool⊢ 0 < macroCost ((Scanner.Mode.dead, n), bs, cs) falsedead.truen:ℕbs:List Boolcs:List Bool⊢ 0 < macroCost ((Scanner.Mode.dead, n), bs, cs) true simp only [macroCost, bitCost]dead.truen:ℕbs:List Boolcs:List Bool⊢ 0 < 1 <;>tree.falsen:ℕbs:List Boolcs:List Bool⊢ 0 < 1tree.truen:ℕbs:List Boolcs:List Bool⊢ 0 < 1zeros.falsen:ℕbs:List Boolcs:List Boolcount✝:ℕ⊢ 0 < 1zeros.truen:ℕbs:List Boolcs:List Boolcount✝:ℕ⊢ 0 < if count✝ = 0 then 16 else 2size.falsen:ℕbs:List Boolcs:List Boolremaining✝:ℕvalue✝:ℕ⊢ 0 < if remaining✝ = 1 then 2 * bs.length + 7 else 2size.truen:ℕbs:List Boolcs:List Boolremaining✝:ℕvalue✝:ℕ⊢ 0 < if remaining✝ = 1 then 2 * bs.length + 7 else 2length.falsen:ℕbs:List Boolcs:List Boolremaining✝:ℕvalue✝:ℕ⊢ 0 < if remaining✝ = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4length.truen:ℕbs:List Boolcs:List Boolremaining✝:ℕvalue✝:ℕ⊢ 0 < if remaining✝ = 1 then 2 * bs.length + 2 * cs.length + 9 else 2 * bs.length + 4payload.falsen:ℕbs:List Boolcs:List Boolremaining✝:ℕ⊢ 0 < if remaining✝ = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4payload.truen:ℕbs:List Boolcs:List Boolremaining✝:ℕ⊢ 0 < if remaining✝ = 1 then 2 * cs.length + max bs.length cs.length + 7 else 2 * cs.length + 4done.falsen:ℕbs:List Boolcs:List Bool⊢ 0 < 1done.truen:ℕbs:List Boolcs:List Bool⊢ 0 < 1dead.falsen:ℕbs:List Boolcs:List Bool⊢ 0 < 1dead.truen:ℕbs:List Boolcs:List Bool⊢ 0 < 1
    first | omegaAll goals completed! 🐙 | (splitpayload.true.isTruen:ℕbs:List Boolcs:List Boolremaining✝:ℕh✝:remaining✝ = 1⊢ 0 < 2 * cs.length + max bs.length cs.length + 7payload.true.isFalsen:ℕbs:List Boolcs:List Boolremaining✝:ℕh✝:¬remaining✝ = 1⊢ 0 < 2 * cs.length + 4 <;>payload.true.isTruen:ℕbs:List Boolcs:List Boolremaining✝:ℕh✝:remaining✝ = 1⊢ 0 < 2 * cs.length + max bs.length cs.length + 7payload.true.isFalsen:ℕbs:List Boolcs:List Boolremaining✝:ℕh✝:¬remaining✝ = 1⊢ 0 < 2 * cs.length + 4 omegaAll goals completed! 🐙)

The total macro time is bounded by a quadratic polynomial in input length.

theorem runCost_le (w : List Bool) : runCost w ≤ 5 * w.length ^ 2 + 16 * w.length := byw:List Bool⊢ runCost w ≤ 5 * w.length ^ 2 + 16 * w.length
  refine List.reverseRecOn w ?_ ?_refine_1w:List Bool⊢ runCost [] ≤ 5 * [].length ^ 2 + 16 * [].lengthrefine_2w:List Bool⊢ ∀ (l : List Bool) (a : Bool),
  runCost l ≤ 5 * l.length ^ 2 + 16 * l.length → runCost (l ++ [a]) ≤ 5 * (l ++ [a]).length ^ 2 + 16 * (l ++ [a]).length
  ·refine_1w:List Bool⊢ runCost [] ≤ 5 * [].length ^ 2 + 16 * [].length exact Nat.le_refl 0All goals completed! 🐙
  ·refine_2w:List Bool⊢ ∀ (l : List Bool) (a : Bool),
  runCost l ≤ 5 * l.length ^ 2 + 16 * l.length → runCost (l ++ [a]) ≤ 5 * (l ++ [a]).length ^ 2 + 16 * (l ++ [a]).length intro bs b ihrefine_2w:List Boolbs:List Boolb:Boolih:runCost bs ≤ 5 * bs.length ^ 2 + 16 * bs.length⊢ runCost (bs ++ [b]) ≤ 5 * (bs ++ [b]).length ^ 2 + 16 * (bs ++ [b]).length
    obtain ⟨hb, hc⟩ := account_lengths_le bsrefine_2w:List Boolbs:List Boolb:Boolih:runCost bs ≤ 5 * bs.length ^ 2 + 16 * bs.lengthhb:(account bs).2.1.length ≤ bs.lengthhc:(account bs).2.2.length ≤ bs.length⊢ runCost (bs ++ [b]) ≤ 5 * (bs ++ [b]).length ^ 2 + 16 * (bs ++ [b]).length
    have hcost := bitCost_le (account bs).1.1 (account bs).2.1 (account bs).2.2
      b bs.length hb hcrefine_2w:List Boolbs:List Boolb:Boolih:runCost bs ≤ 5 * bs.length ^ 2 + 16 * bs.lengthhb:(account bs).2.1.length ≤ bs.lengthhc:(account bs).2.2.length ≤ bs.lengthhcost:bitCost (account bs).1.1 (account bs).2.1 (account bs).2.2 b ≤ 5 * bs.length + 16⊢ runCost (bs ++ [b]) ≤ 5 * (bs ++ [b]).length ^ 2 + 16 * (bs ++ [b]).length
    change macroCost (account bs) b ≤ _ at hcostrefine_2w:List Boolbs:List Boolb:Boolih:runCost bs ≤ 5 * bs.length ^ 2 + 16 * bs.lengthhb:(account bs).2.1.length ≤ bs.lengthhc:(account bs).2.2.length ≤ bs.lengthhcost:macroCost (account bs) b ≤ 5 * bs.length + 16⊢ runCost (bs ++ [b]) ≤ 5 * (bs ++ [b]).length ^ 2 + 16 * (bs ++ [b]).length
    rw [runCost_appendrefine_2w:List Boolbs:List Boolb:Boolih:runCost bs ≤ 5 * bs.length ^ 2 + 16 * bs.lengthhb:(account bs).2.1.length ≤ bs.lengthhc:(account bs).2.2.length ≤ bs.lengthhcost:macroCost (account bs) b ≤ 5 * bs.length + 16⊢ runCost bs + macroCost (account bs) b ≤ 5 * (bs ++ [b]).length ^ 2 + 16 * (bs ++ [b]).length]refine_2w:List Boolbs:List Boolb:Boolih:runCost bs ≤ 5 * bs.length ^ 2 + 16 * bs.lengthhb:(account bs).2.1.length ≤ bs.lengthhc:(account bs).2.2.length ≤ bs.lengthhcost:macroCost (account bs) b ≤ 5 * bs.length + 16⊢ runCost bs + macroCost (account bs) b ≤ 5 * (bs ++ [b]).length ^ 2 + 16 * (bs ++ [b]).length
    simp only [List.length_append, List.length_cons, List.length_nil, Nat.zero_add,
      Nat.pow_two, Nat.add_mul, Nat.mul_add, Nat.mul_one, Nat.one_mul]refine_2w:List Boolbs:List Boolb:Boolih:runCost bs ≤ 5 * bs.length ^ 2 + 16 * bs.lengthhb:(account bs).2.1.length ≤ bs.lengthhc:(account bs).2.2.length ≤ bs.lengthhcost:macroCost (account bs) b ≤ 5 * bs.length + 16⊢ runCost bs + macroCost (account bs) b ≤
  5 * (bs.length * bs.length) + 5 * bs.length + (5 * bs.length + 5) + (16 * bs.length + 16)
    rw [Nat.pow_tworefine_2w:List Boolbs:List Boolb:Boolih:runCost bs ≤ 5 * (bs.length * bs.length) + 16 * bs.lengthhb:(account bs).2.1.length ≤ bs.lengthhc:(account bs).2.2.length ≤ bs.lengthhcost:macroCost (account bs) b ≤ 5 * bs.length + 16⊢ runCost bs + macroCost (account bs) b ≤
  5 * (bs.length * bs.length) + 5 * bs.length + (5 * bs.length + 5) + (16 * bs.length + 16)] at ihrefine_2w:List Boolbs:List Boolb:Boolih:runCost bs ≤ 5 * (bs.length * bs.length) + 16 * bs.lengthhb:(account bs).2.1.length ≤ bs.lengthhc:(account bs).2.2.length ≤ bs.lengthhcost:macroCost (account bs) b ≤ 5 * bs.length + 16⊢ runCost bs + macroCost (account bs) b ≤
  5 * (bs.length * bs.length) + 5 * bs.length + (5 * bs.length + 5) + (16 * bs.length + 16)
    omegaAll goals completed! 🐙

The account at the next prefix is a single update of the current account.

theorem account_take_succ (w : List Bool) (t : ℕ) (h : t < w.length) :
    account (w.take (t + 1)) = accountStep (account (w.take t)) w[t] := byw:List Boolt:ℕh:t < w.length⊢ account (List.take (t + 1) w) = accountStep (account (List.take t w)) w[t]
  rw [List.take_succ_eq_append_getElem h,w:List Boolt:ℕh:t < w.length⊢ account (List.take t w ++ [w[t]]) = accountStep (account (List.take t w)) w[t] account_appendw:List Boolt:ℕh:t < w.length⊢ accountStep (account (List.take t w)) w[t] = accountStep (account (List.take t w)) w[t]]All goals completed! 🐙

The next prefix adds exactly one complete transition cost.

theorem runCost_take_succ (w : List Bool) (t : ℕ) (h : t < w.length) :
    runCost (w.take (t + 1)) =
      runCost (w.take t) + macroCost (account (w.take t)) w[t] := byw:List Boolt:ℕh:t < w.length⊢ runCost (List.take (t + 1) w) = runCost (List.take t w) + macroCost (account (List.take t w)) w[t]
  rw [List.take_succ_eq_append_getElem h,w:List Boolt:ℕh:t < w.length⊢ runCost (List.take t w ++ [w[t]]) = runCost (List.take t w) + macroCost (account (List.take t w)) w[t] runCost_appendw:List Boolt:ℕh:t < w.length⊢ runCost (List.take t w) + macroCost (account (List.take t w)) w[t] =
  runCost (List.take t w) + macroCost (account (List.take t w)) w[t]]All goals completed! 🐙

Binary fields at any prefix fit within the length of the whole input.

theorem prefix_lengths_le (w : List Bool) (t : ℕ) :
    (account (w.take t)).2.1.length ≤ w.length ∧
      (account (w.take t)).2.2.length ≤ w.length := byw:List Boolt:ℕ⊢ (account (List.take t w)).2.1.length ≤ w.length ∧ (account (List.take t w)).2.2.length ≤ w.length
  obtain ⟨hb, hc⟩ := account_lengths_le (w.take t)w:List Boolt:ℕhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhc:(account (List.take t w)).2.2.length ≤ (List.take t w).length⊢ (account (List.take t w)).2.1.length ≤ w.length ∧ (account (List.take t w)).2.2.length ≤ w.length
  have ht : (w.take t).length ≤ w.length := by simp only [List.length_take]w:List Boolt:ℕhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhc:(account (List.take t w)).2.2.length ≤ (List.take t w).length⊢ min t w.length ≤ w.length; omegaw:List Boolt:ℕhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhc:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthht:(List.take t w).length ≤ w.length⊢ (account (List.take t w)).2.1.length ≤ w.length ∧ (account (List.take t w)).2.2.length ≤ w.length
  exact ⟨Nat.le_trans hb ht, Nat.le_trans hc ht⟩All goals completed! 🐙

end Geb.BitTree.Elias.Machine