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.Scanner
public import Geb.Prototypes.Computability.BitTree.Elias.Code

set_option doc.verso true

Streaming recognition of Elias delta headers

The scanner reads a unary size prefix and two fixed-width binary fields. Complete fields change phases on their last bit; incomplete fields retain a header phase and cannot accept.

Main statements

foldl_header relates successful integer parsing to the streaming header phases.
header_reject excludes acceptance when the integer header is incomplete.

Tags

Elias delta code, streaming recognizer, simulation

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

Scanning a unary zero prefix increases the prefix count by its length.

theorem foldl_replicate_false (k z n : ℕ) :
    (List.replicate k false).foldl step (.zeros z, n) = (.zeros (z + k), n) := byk:ℕz:ℕn:ℕ⊢ List.foldl step (Mode.zeros z, n) (List.replicate k false) = (Mode.zeros (z + k), n)
  revert zk:ℕn:ℕ⊢ ∀ (z : ℕ), List.foldl step (Mode.zeros z, n) (List.replicate k false) = (Mode.zeros (z + k), n)
  apply Nat.rec (motive := fun k ↦ ∀ z,
    (List.replicate k false).foldl step (.zeros z, n) = (.zeros (z + k), n)) ?_ ?_ kk:ℕn:ℕ⊢ ∀ (z : ℕ), List.foldl step (Mode.zeros z, n) (List.replicate Nat.zero false) = (Mode.zeros (z + Nat.zero), n)k:ℕn:ℕ⊢ ∀ (n_1 : ℕ),
  (∀ (z : ℕ), List.foldl step (Mode.zeros z, n) (List.replicate n_1 false) = (Mode.zeros (z + n_1), n)) →
    ∀ (z : ℕ), List.foldl step (Mode.zeros z, n) (List.replicate n_1.succ false) = (Mode.zeros (z + n_1.succ), n)
  ·k:ℕn:ℕ⊢ ∀ (z : ℕ), List.foldl step (Mode.zeros z, n) (List.replicate Nat.zero false) = (Mode.zeros (z + Nat.zero), n) intro zk:ℕn:ℕz:ℕ⊢ List.foldl step (Mode.zeros z, n) (List.replicate Nat.zero false) = (Mode.zeros (z + Nat.zero), n)
    rflAll goals completed! 🐙
  ·k:ℕn:ℕ⊢ ∀ (n_1 : ℕ),
  (∀ (z : ℕ), List.foldl step (Mode.zeros z, n) (List.replicate n_1 false) = (Mode.zeros (z + n_1), n)) →
    ∀ (z : ℕ), List.foldl step (Mode.zeros z, n) (List.replicate n_1.succ false) = (Mode.zeros (z + n_1.succ), n) intro k ih zk✝:ℕn:ℕk:ℕih:∀ (z : ℕ), List.foldl step (Mode.zeros z, n) (List.replicate k false) = (Mode.zeros (z + k), n)z:ℕ⊢ List.foldl step (Mode.zeros z, n) (List.replicate k.succ false) = (Mode.zeros (z + k.succ), n)
    rw [List.replicate_succ,k✝:ℕn:ℕk:ℕih:∀ (z : ℕ), List.foldl step (Mode.zeros z, n) (List.replicate k false) = (Mode.zeros (z + k), n)z:ℕ⊢ List.foldl step (Mode.zeros z, n) (false :: List.replicate k false) = (Mode.zeros (z + k.succ), n) List.foldl_consk✝:ℕn:ℕk:ℕih:∀ (z : ℕ), List.foldl step (Mode.zeros z, n) (List.replicate k false) = (Mode.zeros (z + k), n)z:ℕ⊢ List.foldl step (step (Mode.zeros z, n) false) (List.replicate k false) = (Mode.zeros (z + k.succ), n)]k✝:ℕn:ℕk:ℕih:∀ (z : ℕ), List.foldl step (Mode.zeros z, n) (List.replicate k false) = (Mode.zeros (z + k), n)z:ℕ⊢ List.foldl step (step (Mode.zeros z, n) false) (List.replicate k false) = (Mode.zeros (z + k.succ), n)
    change (List.replicate k false).foldl step (.zeros (z + 1), n) = _k✝:ℕn:ℕk:ℕih:∀ (z : ℕ), List.foldl step (Mode.zeros z, n) (List.replicate k false) = (Mode.zeros (z + k), n)z:ℕ⊢ List.foldl step (Mode.zeros (z + 1), n) (List.replicate k false) = (Mode.zeros (z + k.succ), n)
    rw [ihk✝:ℕn:ℕk:ℕih:∀ (z : ℕ), List.foldl step (Mode.zeros z, n) (List.replicate k false) = (Mode.zeros (z + k), n)z:ℕ⊢ (Mode.zeros (z + 1 + k), n) = (Mode.zeros (z + k.succ), n)]k✝:ℕn:ℕk:ℕih:∀ (z : ℕ), List.foldl step (Mode.zeros z, n) (List.replicate k false) = (Mode.zeros (z + k), n)z:ℕ⊢ (Mode.zeros (z + 1 + k), n) = (Mode.zeros (z + k.succ), n)
    congr 2e_fstk✝:ℕn:ℕk:ℕih:∀ (z : ℕ), List.foldl step (Mode.zeros z, n) (List.replicate k false) = (Mode.zeros (z + k), n)z:ℕ⊢ z + 1 + k = z + k.succ
    omegaAll goals completed! 🐙

A nonempty fixed-width field ends at its final bit, in either binary header phase.

theorem foldl_field (isSize : Bool) (bs : List Bool) : ∀ v n, bs ≠ [] →
    bs.foldl step ((if isSize then .size bs.length v else .length bs.length v), n) =
      ((if isSize then .length (bs.foldl (fun a b ↦ Nat.bit b a) v - 1) 1
        else .payload (bs.foldl (fun a b ↦ Nat.bit b a) v - 1)), n) :=
  List.rec (fun _ _ h ↦ (h rfl).elim) (fun b bs ih v n _ ↦ byisSize:Boolbs✝:List Boolb:Boolbs:List Boolih:∀ (v n : ℕ),
  bs ≠ [] →
    List.foldl step (if isSize = true then Mode.size bs.length v else Mode.length bs.length v, n) bs =
      (if isSize = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v bs - 1) 1
        else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v bs - 1),
        n)v:ℕn:ℕx✝:b :: bs ≠ []⊢ List.foldl step (if isSize = true then Mode.size (b :: bs).length v else Mode.length (b :: bs).length v, n) (b :: bs) =
  (if isSize = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v (b :: bs) - 1) 1
    else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v (b :: bs) - 1),
    n)
    cases bs with
    | nil =>nilisSize:Boolbs:List Boolb:Boolv:ℕn:ℕih:∀ (v n : ℕ),
  [] ≠ [] →
    List.foldl step (if isSize = true then Mode.size [].length v else Mode.length [].length v, n) [] =
      (if isSize = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v [] - 1) 1
        else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v [] - 1),
        n)x✝:[b] ≠ []⊢ List.foldl step (if isSize = true then Mode.size [b].length v else Mode.length [b].length v, n) [b] =
  (if isSize = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v [b] - 1) 1
    else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v [b] - 1),
    n) cases isSizenil.falsebs:List Boolb:Boolv:ℕn:ℕx✝:[b] ≠ []ih:∀ (v n : ℕ),
  [] ≠ [] →
    List.foldl step (if false = true then Mode.size [].length v else Mode.length [].length v, n) [] =
      (if false = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v [] - 1) 1
        else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v [] - 1),
        n)⊢ List.foldl step (if false = true then Mode.size [b].length v else Mode.length [b].length v, n) [b] =
  (if false = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v [b] - 1) 1
    else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v [b] - 1),
    n)nil.truebs:List Boolb:Boolv:ℕn:ℕx✝:[b] ≠ []ih:∀ (v n : ℕ),
  [] ≠ [] →
    List.foldl step (if true = true then Mode.size [].length v else Mode.length [].length v, n) [] =
      (if true = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v [] - 1) 1
        else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v [] - 1),
        n)⊢ List.foldl step (if true = true then Mode.size [b].length v else Mode.length [b].length v, n) [b] =
  (if true = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v [b] - 1) 1
    else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v [b] - 1),
    n) <;>nil.falsebs:List Boolb:Boolv:ℕn:ℕx✝:[b] ≠ []ih:∀ (v n : ℕ),
  [] ≠ [] →
    List.foldl step (if false = true then Mode.size [].length v else Mode.length [].length v, n) [] =
      (if false = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v [] - 1) 1
        else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v [] - 1),
        n)⊢ List.foldl step (if false = true then Mode.size [b].length v else Mode.length [b].length v, n) [b] =
  (if false = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v [b] - 1) 1
    else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v [b] - 1),
    n)nil.truebs:List Boolb:Boolv:ℕn:ℕx✝:[b] ≠ []ih:∀ (v n : ℕ),
  [] ≠ [] →
    List.foldl step (if true = true then Mode.size [].length v else Mode.length [].length v, n) [] =
      (if true = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v [] - 1) 1
        else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v [] - 1),
        n)⊢ List.foldl step (if true = true then Mode.size [b].length v else Mode.length [b].length v, n) [b] =
  (if true = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v [b] - 1) 1
    else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v [b] - 1),
    n) rflAll goals completed! 🐙
    | cons c bs =>consisSize:Boolbs✝:List Boolb:Boolv:ℕn:ℕc:Boolbs:List Boolih:∀ (v n : ℕ),
  c :: bs ≠ [] →
    List.foldl step (if isSize = true then Mode.size (c :: bs).length v else Mode.length (c :: bs).length v, n)
        (c :: bs) =
      (if isSize = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v (c :: bs) - 1) 1
        else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v (c :: bs) - 1),
        n)x✝:b :: c :: bs ≠ []⊢ List.foldl step (if isSize = true then Mode.size (b :: c :: bs).length v else Mode.length (b :: c :: bs).length v, n)
    (b :: c :: bs) =
  (if isSize = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v (b :: c :: bs) - 1) 1
    else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v (b :: c :: bs) - 1),
    n)
      have he : bs.length + 1 + 1 ≠ 1 := byisSize:Boolbs✝:List Boolb:Boolbs:List Boolih:∀ (v n : ℕ),
  bs ≠ [] →
    List.foldl step (if isSize = true then Mode.size bs.length v else Mode.length bs.length v, n) bs =
      (if isSize = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v bs - 1) 1
        else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v bs - 1),
        n)v:ℕn:ℕx✝:b :: bs ≠ []⊢ List.foldl step (if isSize = true then Mode.size (b :: bs).length v else Mode.length (b :: bs).length v, n) (b :: bs) =
  (if isSize = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v (b :: bs) - 1) 1
    else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v (b :: bs) - 1),
    n) omegaconsisSize:Boolbs✝:List Boolb:Boolv:ℕn:ℕc:Boolbs:List Boolih:∀ (v n : ℕ),
  c :: bs ≠ [] →
    List.foldl step (if isSize = true then Mode.size (c :: bs).length v else Mode.length (c :: bs).length v, n)
        (c :: bs) =
      (if isSize = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v (c :: bs) - 1) 1
        else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v (c :: bs) - 1),
        n)x✝:b :: c :: bs ≠ []he:bs.length + 1 + 1 ≠ 1⊢ List.foldl step (if isSize = true then Mode.size (b :: c :: bs).length v else Mode.length (b :: c :: bs).length v, n)
    (b :: c :: bs) =
  (if isSize = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v (b :: c :: bs) - 1) 1
    else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v (b :: c :: bs) - 1),
    n)
      cases isSizecons.falsebs✝:List Boolb:Boolv:ℕn:ℕc:Boolbs:List Boolx✝:b :: c :: bs ≠ []he:bs.length + 1 + 1 ≠ 1ih:∀ (v n : ℕ),
  c :: bs ≠ [] →
    List.foldl step (if false = true then Mode.size (c :: bs).length v else Mode.length (c :: bs).length v, n)
        (c :: bs) =
      (if false = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v (c :: bs) - 1) 1
        else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v (c :: bs) - 1),
        n)⊢ List.foldl step (if false = true then Mode.size (b :: c :: bs).length v else Mode.length (b :: c :: bs).length v, n)
    (b :: c :: bs) =
  (if false = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v (b :: c :: bs) - 1) 1
    else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v (b :: c :: bs) - 1),
    n)cons.truebs✝:List Boolb:Boolv:ℕn:ℕc:Boolbs:List Boolx✝:b :: c :: bs ≠ []he:bs.length + 1 + 1 ≠ 1ih:∀ (v n : ℕ),
  c :: bs ≠ [] →
    List.foldl step (if true = true then Mode.size (c :: bs).length v else Mode.length (c :: bs).length v, n)
        (c :: bs) =
      (if true = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v (c :: bs) - 1) 1
        else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v (c :: bs) - 1),
        n)⊢ List.foldl step (if true = true then Mode.size (b :: c :: bs).length v else Mode.length (b :: c :: bs).length v, n)
    (b :: c :: bs) =
  (if true = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v (b :: c :: bs) - 1) 1
    else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v (b :: c :: bs) - 1),
    n) <;>cons.falsebs✝:List Boolb:Boolv:ℕn:ℕc:Boolbs:List Boolx✝:b :: c :: bs ≠ []he:bs.length + 1 + 1 ≠ 1ih:∀ (v n : ℕ),
  c :: bs ≠ [] →
    List.foldl step (if false = true then Mode.size (c :: bs).length v else Mode.length (c :: bs).length v, n)
        (c :: bs) =
      (if false = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v (c :: bs) - 1) 1
        else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v (c :: bs) - 1),
        n)⊢ List.foldl step (if false = true then Mode.size (b :: c :: bs).length v else Mode.length (b :: c :: bs).length v, n)
    (b :: c :: bs) =
  (if false = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v (b :: c :: bs) - 1) 1
    else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v (b :: c :: bs) - 1),
    n)cons.truebs✝:List Boolb:Boolv:ℕn:ℕc:Boolbs:List Boolx✝:b :: c :: bs ≠ []he:bs.length + 1 + 1 ≠ 1ih:∀ (v n : ℕ),
  c :: bs ≠ [] →
    List.foldl step (if true = true then Mode.size (c :: bs).length v else Mode.length (c :: bs).length v, n)
        (c :: bs) =
      (if true = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v (c :: bs) - 1) 1
        else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v (c :: bs) - 1),
        n)⊢ List.foldl step (if true = true then Mode.size (b :: c :: bs).length v else Mode.length (b :: c :: bs).length v, n)
    (b :: c :: bs) =
  (if true = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v (b :: c :: bs) - 1) 1
    else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v (b :: c :: bs) - 1),
    n)
        simpa only [List.foldl_cons, List.length_cons, step, he, Bool.false_eq_true, ↓reduceIte,
          Nat.add_sub_cancel] using ih (Nat.bit b v) n (bybs✝:List Boolb:Boolv:ℕn:ℕc:Boolbs:List Boolx✝:b :: c :: bs ≠ []he:bs.length + 1 + 1 ≠ 1ih:∀ (v n : ℕ),
  c :: bs ≠ [] →
    List.foldl step (if true = true then Mode.size (c :: bs).length v else Mode.length (c :: bs).length v, n)
        (c :: bs) =
      (if true = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) v (c :: bs) - 1) 1
        else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) v (c :: bs) - 1),
        n)⊢ c :: bs ≠ [] simpAll goals completed! 🐙)) bs

A field shorter than its remaining width stays in the same header phase.

theorem foldl_short_field (isSize : Bool) (bs : List Bool) : ∀ r v n, bs.length < r →
    bs.foldl step ((if isSize then .size r v else .length r v), n) =
      ((if isSize then .size (r - bs.length) (bs.foldl (fun a b ↦ Nat.bit b a) v)
        else .length (r - bs.length) (bs.foldl (fun a b ↦ Nat.bit b a) v)), n) :=
  List.rec (fun _ _ _ _ ↦ rfl) (fun b bs ih r v n h ↦ byisSize:Boolbs✝:List Boolb:Boolbs:List Boolih:∀ (r v n : ℕ),
  bs.length < r →
    List.foldl step (if isSize = true then Mode.size r v else Mode.length r v, n) bs =
      (if isSize = true then Mode.size (r - bs.length) (List.foldl (fun a b ↦ Nat.bit b a) v bs)
        else Mode.length (r - bs.length) (List.foldl (fun a b ↦ Nat.bit b a) v bs),
        n)r:ℕv:ℕn:ℕh:(b :: bs).length < r⊢ List.foldl step (if isSize = true then Mode.size r v else Mode.length r v, n) (b :: bs) =
  (if isSize = true then Mode.size (r - (b :: bs).length) (List.foldl (fun a b ↦ Nat.bit b a) v (b :: bs))
    else Mode.length (r - (b :: bs).length) (List.foldl (fun a b ↦ Nat.bit b a) v (b :: bs)),
    n)
    have hr : r ≠ 1 := by simp only [List.length_cons] at hisSize:Boolbs✝:List Boolb:Boolbs:List Boolih:∀ (r v n : ℕ),
  bs.length < r →
    List.foldl step (if isSize = true then Mode.size r v else Mode.length r v, n) bs =
      (if isSize = true then Mode.size (r - bs.length) (List.foldl (fun a b ↦ Nat.bit b a) v bs)
        else Mode.length (r - bs.length) (List.foldl (fun a b ↦ Nat.bit b a) v bs),
        n)r:ℕv:ℕn:ℕh:bs.length + 1 < r⊢ r ≠ 1; omegaisSize:Boolbs✝:List Boolb:Boolbs:List Boolih:∀ (r v n : ℕ),
  bs.length < r →
    List.foldl step (if isSize = true then Mode.size r v else Mode.length r v, n) bs =
      (if isSize = true then Mode.size (r - bs.length) (List.foldl (fun a b ↦ Nat.bit b a) v bs)
        else Mode.length (r - bs.length) (List.foldl (fun a b ↦ Nat.bit b a) v bs),
        n)r:ℕv:ℕn:ℕh:(b :: bs).length < rhr:r ≠ 1⊢ List.foldl step (if isSize = true then Mode.size r v else Mode.length r v, n) (b :: bs) =
  (if isSize = true then Mode.size (r - (b :: bs).length) (List.foldl (fun a b ↦ Nat.bit b a) v (b :: bs))
    else Mode.length (r - (b :: bs).length) (List.foldl (fun a b ↦ Nat.bit b a) v (b :: bs)),
    n)
    have ht : bs.length < r - 1 := by simp only [List.length_cons] at hisSize:Boolbs✝:List Boolb:Boolbs:List Boolih:∀ (r v n : ℕ),
  bs.length < r →
    List.foldl step (if isSize = true then Mode.size r v else Mode.length r v, n) bs =
      (if isSize = true then Mode.size (r - bs.length) (List.foldl (fun a b ↦ Nat.bit b a) v bs)
        else Mode.length (r - bs.length) (List.foldl (fun a b ↦ Nat.bit b a) v bs),
        n)r:ℕv:ℕn:ℕh:bs.length + 1 < rhr:r ≠ 1⊢ bs.length < r - 1; omegaisSize:Boolbs✝:List Boolb:Boolbs:List Boolih:∀ (r v n : ℕ),
  bs.length < r →
    List.foldl step (if isSize = true then Mode.size r v else Mode.length r v, n) bs =
      (if isSize = true then Mode.size (r - bs.length) (List.foldl (fun a b ↦ Nat.bit b a) v bs)
        else Mode.length (r - bs.length) (List.foldl (fun a b ↦ Nat.bit b a) v bs),
        n)r:ℕv:ℕn:ℕh:(b :: bs).length < rhr:r ≠ 1ht:bs.length < r - 1⊢ List.foldl step (if isSize = true then Mode.size r v else Mode.length r v, n) (b :: bs) =
  (if isSize = true then Mode.size (r - (b :: bs).length) (List.foldl (fun a b ↦ Nat.bit b a) v (b :: bs))
    else Mode.length (r - (b :: bs).length) (List.foldl (fun a b ↦ Nat.bit b a) v (b :: bs)),
    n)
    have he : r - 1 - bs.length = r - (bs.length + 1) := by omegaisSize:Boolbs✝:List Boolb:Boolbs:List Boolih:∀ (r v n : ℕ),
  bs.length < r →
    List.foldl step (if isSize = true then Mode.size r v else Mode.length r v, n) bs =
      (if isSize = true then Mode.size (r - bs.length) (List.foldl (fun a b ↦ Nat.bit b a) v bs)
        else Mode.length (r - bs.length) (List.foldl (fun a b ↦ Nat.bit b a) v bs),
        n)r:ℕv:ℕn:ℕh:(b :: bs).length < rhr:r ≠ 1ht:bs.length < r - 1he:r - 1 - bs.length = r - (bs.length + 1)⊢ List.foldl step (if isSize = true then Mode.size r v else Mode.length r v, n) (b :: bs) =
  (if isSize = true then Mode.size (r - (b :: bs).length) (List.foldl (fun a b ↦ Nat.bit b a) v (b :: bs))
    else Mode.length (r - (b :: bs).length) (List.foldl (fun a b ↦ Nat.bit b a) v (b :: bs)),
    n)
    cases isSizefalsebs✝:List Boolb:Boolbs:List Boolr:ℕv:ℕn:ℕh:(b :: bs).length < rhr:r ≠ 1ht:bs.length < r - 1he:r - 1 - bs.length = r - (bs.length + 1)ih:∀ (r v n : ℕ),
  bs.length < r →
    List.foldl step (if false = true then Mode.size r v else Mode.length r v, n) bs =
      (if false = true then Mode.size (r - bs.length) (List.foldl (fun a b ↦ Nat.bit b a) v bs)
        else Mode.length (r - bs.length) (List.foldl (fun a b ↦ Nat.bit b a) v bs),
        n)⊢ List.foldl step (if false = true then Mode.size r v else Mode.length r v, n) (b :: bs) =
  (if false = true then Mode.size (r - (b :: bs).length) (List.foldl (fun a b ↦ Nat.bit b a) v (b :: bs))
    else Mode.length (r - (b :: bs).length) (List.foldl (fun a b ↦ Nat.bit b a) v (b :: bs)),
    n)truebs✝:List Boolb:Boolbs:List Boolr:ℕv:ℕn:ℕh:(b :: bs).length < rhr:r ≠ 1ht:bs.length < r - 1he:r - 1 - bs.length = r - (bs.length + 1)ih:∀ (r v n : ℕ),
  bs.length < r →
    List.foldl step (if true = true then Mode.size r v else Mode.length r v, n) bs =
      (if true = true then Mode.size (r - bs.length) (List.foldl (fun a b ↦ Nat.bit b a) v bs)
        else Mode.length (r - bs.length) (List.foldl (fun a b ↦ Nat.bit b a) v bs),
        n)⊢ List.foldl step (if true = true then Mode.size r v else Mode.length r v, n) (b :: bs) =
  (if true = true then Mode.size (r - (b :: bs).length) (List.foldl (fun a b ↦ Nat.bit b a) v (b :: bs))
    else Mode.length (r - (b :: bs).length) (List.foldl (fun a b ↦ Nat.bit b a) v (b :: bs)),
    n) <;>falsebs✝:List Boolb:Boolbs:List Boolr:ℕv:ℕn:ℕh:(b :: bs).length < rhr:r ≠ 1ht:bs.length < r - 1he:r - 1 - bs.length = r - (bs.length + 1)ih:∀ (r v n : ℕ),
  bs.length < r →
    List.foldl step (if false = true then Mode.size r v else Mode.length r v, n) bs =
      (if false = true then Mode.size (r - bs.length) (List.foldl (fun a b ↦ Nat.bit b a) v bs)
        else Mode.length (r - bs.length) (List.foldl (fun a b ↦ Nat.bit b a) v bs),
        n)⊢ List.foldl step (if false = true then Mode.size r v else Mode.length r v, n) (b :: bs) =
  (if false = true then Mode.size (r - (b :: bs).length) (List.foldl (fun a b ↦ Nat.bit b a) v (b :: bs))
    else Mode.length (r - (b :: bs).length) (List.foldl (fun a b ↦ Nat.bit b a) v (b :: bs)),
    n)truebs✝:List Boolb:Boolbs:List Boolr:ℕv:ℕn:ℕh:(b :: bs).length < rhr:r ≠ 1ht:bs.length < r - 1he:r - 1 - bs.length = r - (bs.length + 1)ih:∀ (r v n : ℕ),
  bs.length < r →
    List.foldl step (if true = true then Mode.size r v else Mode.length r v, n) bs =
      (if true = true then Mode.size (r - bs.length) (List.foldl (fun a b ↦ Nat.bit b a) v bs)
        else Mode.length (r - bs.length) (List.foldl (fun a b ↦ Nat.bit b a) v bs),
        n)⊢ List.foldl step (if true = true then Mode.size r v else Mode.length r v, n) (b :: bs) =
  (if true = true then Mode.size (r - (b :: bs).length) (List.foldl (fun a b ↦ Nat.bit b a) v (b :: bs))
    else Mode.length (r - (b :: bs).length) (List.foldl (fun a b ↦ Nat.bit b a) v (b :: bs)),
    n)
      simpa only [List.foldl_cons, List.length_cons, step, hr, Bool.false_eq_true,
        ↓reduceIte, he] using
        ih (r - 1) (Nat.bit b v) n htAll goals completed! 🐙) bs

A positive integer has an empty binary payload exactly when it is one.

theorem payload_eq_nil_iff (k : ℕ) (hk : k ≠ 0) : payload k = [] ↔ k = 1 := byk:ℕhk:k ≠ 0⊢ payload k = [] ↔ k = 1
  constructormpk:ℕhk:k ≠ 0⊢ payload k = [] → k = 1mprk:ℕhk:k ≠ 0⊢ k = 1 → payload k = []
  ·mpk:ℕhk:k ≠ 0⊢ payload k = [] → k = 1 intro hmpk:ℕhk:k ≠ 0h:payload k = []⊢ k = 1
    have he := fromPayload_payload k hkmpk:ℕhk:k ≠ 0h:payload k = []he:fromPayload (payload k) = k⊢ k = 1
    rw [hmpk:ℕhk:k ≠ 0h:payload k = []he:fromPayload [] = k⊢ k = 1] at hempk:ℕhk:k ≠ 0h:payload k = []he:fromPayload [] = k⊢ k = 1
    exact he.symmAll goals completed! 🐙
  ·mprk:ℕhk:k ≠ 0⊢ k = 1 → payload k = [] rintro rflmprhk:1 ≠ 0⊢ payload 1 = []
    rflAll goals completed! 🐙

Scanning a gamma prefix either completes zero or starts the remaining length field.

theorem foldl_gamma (k : ℕ) (hk : k ≠ 0) (n : ℕ) :
    (encodeGamma k).foldl step (.zeros 0, n) =
      if k = 1 then finish n else (.length (k - 1) 1, n) := byk:ℕhk:k ≠ 0n:ℕ⊢ List.foldl step (Mode.zeros 0, n) (encodeGamma k) = if k = 1 then finish n else (Mode.length (k - 1) 1, n)
  have hp := payload_eq_nil_iff k hkk:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1⊢ List.foldl step (Mode.zeros 0, n) (encodeGamma k) = if k = 1 then finish n else (Mode.length (k - 1) 1, n)
  by_cases hnil : payload k = []posk:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1hnil:payload k = []⊢ List.foldl step (Mode.zeros 0, n) (encodeGamma k) = if k = 1 then finish n else (Mode.length (k - 1) 1, n)negk:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1hnil:¬payload k = []⊢ List.foldl step (Mode.zeros 0, n) (encodeGamma k) = if k = 1 then finish n else (Mode.length (k - 1) 1, n)
  ·posk:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1hnil:payload k = []⊢ List.foldl step (Mode.zeros 0, n) (encodeGamma k) = if k = 1 then finish n else (Mode.length (k - 1) 1, n) have he := hp.mp hnilposk:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1hnil:payload k = []he:k = 1⊢ List.foldl step (Mode.zeros 0, n) (encodeGamma k) = if k = 1 then finish n else (Mode.length (k - 1) 1, n)
    subst kposn:ℕhk:1 ≠ 0hp:payload 1 = [] ↔ 1 = 1hnil:payload 1 = []⊢ List.foldl step (Mode.zeros 0, n) (encodeGamma 1) = if 1 = 1 then finish n else (Mode.length (1 - 1) 1, n)
    rflAll goals completed! 🐙
  ·negk:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1hnil:¬payload k = []⊢ List.foldl step (Mode.zeros 0, n) (encodeGamma k) = if k = 1 then finish n else (Mode.length (k - 1) 1, n) have hlen : (payload k).length ≠ 0 := by
      intro hek:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1hnil:¬payload k = []he:(payload k).length = 0⊢ False
      exact hnil (List.eq_nil_of_length_eq_zero he)negk:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1hnil:¬payload k = []hlen:(payload k).length ≠ 0⊢ List.foldl step (Mode.zeros 0, n) (encodeGamma k) = if k = 1 then finish n else (Mode.length (k - 1) 1, n)
    have hk1 : k ≠ 1 := fun he ↦ hnil (hp.mpr he)negk:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1hnil:¬payload k = []hlen:(payload k).length ≠ 0hk1:k ≠ 1⊢ List.foldl step (Mode.zeros 0, n) (encodeGamma k) = if k = 1 then finish n else (Mode.length (k - 1) 1, n)
    rw [encodeGamma,negk:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1hnil:¬payload k = []hlen:(payload k).length ≠ 0hk1:k ≠ 1⊢ List.foldl step (Mode.zeros 0, n) (List.replicate (k.size - 1) false ++ true :: payload k) =
  if k = 1 then finish n else (Mode.length (k - 1) 1, n) ← length_payload,negk:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1hnil:¬payload k = []hlen:(payload k).length ≠ 0hk1:k ≠ 1⊢ List.foldl step (Mode.zeros 0, n) (List.replicate (payload k).length false ++ true :: payload k) =
  if k = 1 then finish n else (Mode.length (k - 1) 1, n) List.foldl_append,negk:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1hnil:¬payload k = []hlen:(payload k).length ≠ 0hk1:k ≠ 1⊢ List.foldl step (List.foldl step (Mode.zeros 0, n) (List.replicate (payload k).length false)) (true :: payload k) =
  if k = 1 then finish n else (Mode.length (k - 1) 1, n) foldl_replicate_falsenegk:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1hnil:¬payload k = []hlen:(payload k).length ≠ 0hk1:k ≠ 1⊢ List.foldl step (Mode.zeros (0 + (payload k).length), n) (true :: payload k) =
  if k = 1 then finish n else (Mode.length (k - 1) 1, n)]negk:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1hnil:¬payload k = []hlen:(payload k).length ≠ 0hk1:k ≠ 1⊢ List.foldl step (Mode.zeros (0 + (payload k).length), n) (true :: payload k) =
  if k = 1 then finish n else (Mode.length (k - 1) 1, n)
    simp only [Nat.zero_add, List.foldl_cons, step, hlen, ↓reduceIte]negk:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1hnil:¬payload k = []hlen:(payload k).length ≠ 0hk1:k ≠ 1⊢ List.foldl step (Mode.size (payload k).length 1, n) (payload k) = if k = 1 then finish n else (Mode.length (k - 1) 1, n)
    have hf := foldl_field true (payload k) 1 n hnilnegk:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1hnil:¬payload k = []hlen:(payload k).length ≠ 0hk1:k ≠ 1hf:List.foldl step (if true = true then Mode.size (payload k).length 1 else Mode.length (payload k).length 1, n)
    (payload k) =
  (if true = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload k) - 1) 1
    else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload k) - 1),
    n)⊢ List.foldl step (Mode.size (payload k).length 1, n) (payload k) = if k = 1 then finish n else (Mode.length (k - 1) 1, n)
    simp only [↓reduceIte] at hfnegk:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1hnil:¬payload k = []hlen:(payload k).length ≠ 0hk1:k ≠ 1hf:List.foldl step (Mode.size (payload k).length 1, n) (payload k) =
  (Mode.length (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload k) - 1) 1, n)⊢ List.foldl step (Mode.size (payload k).length 1, n) (payload k) = if k = 1 then finish n else (Mode.length (k - 1) 1, n)
    rw [hfnegk:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1hnil:¬payload k = []hlen:(payload k).length ≠ 0hk1:k ≠ 1hf:List.foldl step (Mode.size (payload k).length 1, n) (payload k) =
  (Mode.length (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload k) - 1) 1, n)⊢ (Mode.length (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload k) - 1) 1, n) =
  if k = 1 then finish n else (Mode.length (k - 1) 1, n)]negk:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1hnil:¬payload k = []hlen:(payload k).length ≠ 0hk1:k ≠ 1hf:List.foldl step (Mode.size (payload k).length 1, n) (payload k) =
  (Mode.length (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload k) - 1) 1, n)⊢ (Mode.length (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload k) - 1) 1, n) =
  if k = 1 then finish n else (Mode.length (k - 1) 1, n)
    change (Mode.length (fromPayload (payload k) - 1) 1, n) = _negk:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1hnil:¬payload k = []hlen:(payload k).length ≠ 0hk1:k ≠ 1hf:List.foldl step (Mode.size (payload k).length 1, n) (payload k) =
  (Mode.length (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload k) - 1) 1, n)⊢ (Mode.length (fromPayload (payload k) - 1) 1, n) = if k = 1 then finish n else (Mode.length (k - 1) 1, n)
    rw [fromPayload_payload k hk,negk:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1hnil:¬payload k = []hlen:(payload k).length ≠ 0hk1:k ≠ 1hf:List.foldl step (Mode.size (payload k).length 1, n) (payload k) =
  (Mode.length (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload k) - 1) 1, n)⊢ (Mode.length (k - 1) 1, n) = if k = 1 then finish n else (Mode.length (k - 1) 1, n) ite_eq_right hk1negk:ℕhk:k ≠ 0n:ℕhp:payload k = [] ↔ k = 1hnil:¬payload k = []hlen:(payload k).length ≠ 0hk1:k ≠ 1hf:List.foldl step (Mode.size (payload k).length 1, n) (payload k) =
  (Mode.length (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload k) - 1) 1, n)⊢ (Mode.length (k - 1) 1, n) = (Mode.length (k - 1) 1, n)]All goals completed! 🐙

Scanning a complete delta code sets its raw-payload countdown.

theorem foldl_encodeNat (m n : ℕ) :
    (encodeNat m).foldl step (.zeros 0, n) =
      if m = 0 then finish n else (.payload m, n) := bym:ℕn:ℕ⊢ List.foldl step (Mode.zeros 0, n) (encodeNat m) = if m = 0 then finish n else (Mode.payload m, n)
  cases m with
  | zero =>zeron:ℕ⊢ List.foldl step (Mode.zeros 0, n) (encodeNat 0) = if 0 = 0 then finish n else (Mode.payload 0, n) rflAll goals completed! 🐙
  | succ m =>succn:ℕm:ℕ⊢ List.foldl step (Mode.zeros 0, n) (encodeNat (m + 1)) = if m + 1 = 0 then finish n else (Mode.payload (m + 1), n)
    have hp : m + 1 + 1 ≠ 0 := bym:ℕn:ℕ⊢ List.foldl step (Mode.zeros 0, n) (encodeNat m) = if m = 0 then finish n else (Mode.payload m, n) omegasuccn:ℕm:ℕhp:m + 1 + 1 ≠ 0⊢ List.foldl step (Mode.zeros 0, n) (encodeNat (m + 1)) = if m + 1 = 0 then finish n else (Mode.payload (m + 1), n)
    have hs : (m + 1 + 1).size ≠ 0 := bym:ℕn:ℕ⊢ List.foldl step (Mode.zeros 0, n) (encodeNat m) = if m = 0 then finish n else (Mode.payload m, n) have h := size_pos _ hpn:ℕm:ℕhp:m + 1 + 1 ≠ 0h:0 < (m + 1 + 1).size⊢ (m + 1 + 1).size ≠ 0; omegasuccn:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0⊢ List.foldl step (Mode.zeros 0, n) (encodeNat (m + 1)) = if m + 1 = 0 then finish n else (Mode.payload (m + 1), n)
    have hnil : payload (m + 1 + 1) ≠ [] := bym:ℕn:ℕ⊢ List.foldl step (Mode.zeros 0, n) (encodeNat m) = if m = 0 then finish n else (Mode.payload m, n)
      intro hen:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0he:payload (m + 1 + 1) = []⊢ False
      have hh := (payload_eq_nil_iff _ hp).mp hen:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0he:payload (m + 1 + 1) = []hh:m + 1 + 1 = 1⊢ False
      omegasuccn:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0hnil:payload (m + 1 + 1) ≠ []⊢ List.foldl step (Mode.zeros 0, n) (encodeNat (m + 1)) = if m + 1 = 0 then finish n else (Mode.payload (m + 1), n)
    have hs1 : (m + 1 + 1).size ≠ 1 := bym:ℕn:ℕ⊢ List.foldl step (Mode.zeros 0, n) (encodeNat m) = if m = 0 then finish n else (Mode.payload m, n)
      intro hen:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0hnil:payload (m + 1 + 1) ≠ []he:(m + 1 + 1).size = 1⊢ False
      apply hniln:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0hnil:payload (m + 1 + 1) ≠ []he:(m + 1 + 1).size = 1⊢ payload (m + 1 + 1) = []
      apply List.eq_nil_of_length_eq_zeron:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0hnil:payload (m + 1 + 1) ≠ []he:(m + 1 + 1).size = 1⊢ (payload (m + 1 + 1)).length = 0
      rw [length_payload,n:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0hnil:payload (m + 1 + 1) ≠ []he:(m + 1 + 1).size = 1⊢ (m + 1 + 1).size - 1 = 0 hen:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0hnil:payload (m + 1 + 1) ≠ []he:(m + 1 + 1).size = 1⊢ 1 - 1 = 0]succn:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0hnil:payload (m + 1 + 1) ≠ []hs1:(m + 1 + 1).size ≠ 1⊢ List.foldl step (Mode.zeros 0, n) (encodeNat (m + 1)) = if m + 1 = 0 then finish n else (Mode.payload (m + 1), n)
    have hf := foldl_field false (payload (m + 1 + 1)) 1 n hnilsuccn:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0hnil:payload (m + 1 + 1) ≠ []hs1:(m + 1 + 1).size ≠ 1hf:List.foldl step
    (if false = true then Mode.size (payload (m + 1 + 1)).length 1 else Mode.length (payload (m + 1 + 1)).length 1, n)
    (payload (m + 1 + 1)) =
  (if false = true then Mode.length (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload (m + 1 + 1)) - 1) 1
    else Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload (m + 1 + 1)) - 1),
    n)⊢ List.foldl step (Mode.zeros 0, n) (encodeNat (m + 1)) = if m + 1 = 0 then finish n else (Mode.payload (m + 1), n)
    simp only [Bool.false_eq_true, ↓reduceIte] at hfsuccn:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0hnil:payload (m + 1 + 1) ≠ []hs1:(m + 1 + 1).size ≠ 1hf:List.foldl step (Mode.length (payload (m + 1 + 1)).length 1, n) (payload (m + 1 + 1)) =
  (Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload (m + 1 + 1)) - 1), n)⊢ List.foldl step (Mode.zeros 0, n) (encodeNat (m + 1)) = if m + 1 = 0 then finish n else (Mode.payload (m + 1), n)
    rw [encodeNat,succn:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0hnil:payload (m + 1 + 1) ≠ []hs1:(m + 1 + 1).size ≠ 1hf:List.foldl step (Mode.length (payload (m + 1 + 1)).length 1, n) (payload (m + 1 + 1)) =
  (Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload (m + 1 + 1)) - 1), n)⊢ List.foldl step (Mode.zeros 0, n) (encodeGamma (m + 1 + 1).size ++ payload (m + 1 + 1)) =
  if m + 1 = 0 then finish n else (Mode.payload (m + 1), n) List.foldl_append,succn:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0hnil:payload (m + 1 + 1) ≠ []hs1:(m + 1 + 1).size ≠ 1hf:List.foldl step (Mode.length (payload (m + 1 + 1)).length 1, n) (payload (m + 1 + 1)) =
  (Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload (m + 1 + 1)) - 1), n)⊢ List.foldl step (List.foldl step (Mode.zeros 0, n) (encodeGamma (m + 1 + 1).size)) (payload (m + 1 + 1)) =
  if m + 1 = 0 then finish n else (Mode.payload (m + 1), n) foldl_gamma _ hs n,succn:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0hnil:payload (m + 1 + 1) ≠ []hs1:(m + 1 + 1).size ≠ 1hf:List.foldl step (Mode.length (payload (m + 1 + 1)).length 1, n) (payload (m + 1 + 1)) =
  (Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload (m + 1 + 1)) - 1), n)⊢ List.foldl step (if (m + 1 + 1).size = 1 then finish n else (Mode.length ((m + 1 + 1).size - 1) 1, n))
    (payload (m + 1 + 1)) =
  if m + 1 = 0 then finish n else (Mode.payload (m + 1), n) ite_eq_right hs1,succn:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0hnil:payload (m + 1 + 1) ≠ []hs1:(m + 1 + 1).size ≠ 1hf:List.foldl step (Mode.length (payload (m + 1 + 1)).length 1, n) (payload (m + 1 + 1)) =
  (Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload (m + 1 + 1)) - 1), n)⊢ List.foldl step (Mode.length ((m + 1 + 1).size - 1) 1, n) (payload (m + 1 + 1)) =
  if m + 1 = 0 then finish n else (Mode.payload (m + 1), n)
      ← length_payload,succn:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0hnil:payload (m + 1 + 1) ≠ []hs1:(m + 1 + 1).size ≠ 1hf:List.foldl step (Mode.length (payload (m + 1 + 1)).length 1, n) (payload (m + 1 + 1)) =
  (Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload (m + 1 + 1)) - 1), n)⊢ List.foldl step (Mode.length (payload (m + 1 + 1)).length 1, n) (payload (m + 1 + 1)) =
  if m + 1 = 0 then finish n else (Mode.payload (m + 1), n) hfsuccn:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0hnil:payload (m + 1 + 1) ≠ []hs1:(m + 1 + 1).size ≠ 1hf:List.foldl step (Mode.length (payload (m + 1 + 1)).length 1, n) (payload (m + 1 + 1)) =
  (Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload (m + 1 + 1)) - 1), n)⊢ (Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload (m + 1 + 1)) - 1), n) =
  if m + 1 = 0 then finish n else (Mode.payload (m + 1), n)]succn:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0hnil:payload (m + 1 + 1) ≠ []hs1:(m + 1 + 1).size ≠ 1hf:List.foldl step (Mode.length (payload (m + 1 + 1)).length 1, n) (payload (m + 1 + 1)) =
  (Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload (m + 1 + 1)) - 1), n)⊢ (Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload (m + 1 + 1)) - 1), n) =
  if m + 1 = 0 then finish n else (Mode.payload (m + 1), n)
    change (Mode.payload (fromPayload (payload (m + 1 + 1)) - 1), n) = _succn:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0hnil:payload (m + 1 + 1) ≠ []hs1:(m + 1 + 1).size ≠ 1hf:List.foldl step (Mode.length (payload (m + 1 + 1)).length 1, n) (payload (m + 1 + 1)) =
  (Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload (m + 1 + 1)) - 1), n)⊢ (Mode.payload (fromPayload (payload (m + 1 + 1)) - 1), n) = if m + 1 = 0 then finish n else (Mode.payload (m + 1), n)
    rw [fromPayload_payload _ hpsuccn:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0hnil:payload (m + 1 + 1) ≠ []hs1:(m + 1 + 1).size ≠ 1hf:List.foldl step (Mode.length (payload (m + 1 + 1)).length 1, n) (payload (m + 1 + 1)) =
  (Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload (m + 1 + 1)) - 1), n)⊢ (Mode.payload (m + 1 + 1 - 1), n) = if m + 1 = 0 then finish n else (Mode.payload (m + 1), n)]succn:ℕm:ℕhp:m + 1 + 1 ≠ 0hs:(m + 1 + 1).size ≠ 0hnil:payload (m + 1 + 1) ≠ []hs1:(m + 1 + 1).size ≠ 1hf:List.foldl step (Mode.length (payload (m + 1 + 1)).length 1, n) (payload (m + 1 + 1)) =
  (Mode.payload (List.foldl (fun a b ↦ Nat.bit b a) 1 (payload (m + 1 + 1)) - 1), n)⊢ (Mode.payload (m + 1 + 1 - 1), n) = if m + 1 = 0 then finish n else (Mode.payload (m + 1), n)
    rflAll goals completed! 🐙

A successfully parsed header has the same effect as its bitwise scan.

theorem foldl_header (w : List Bool) (m : ℕ) (rest : List Bool) (n : ℕ)
    (h : readNat w = some (m, rest)) :
    w.foldl step (.zeros 0, n) =
      rest.foldl step (if m = 0 then finish n else (.payload m, n)) := byw:List Boolm:ℕrest:List Booln:ℕh:readNat w = some (m, rest)⊢ List.foldl step (Mode.zeros 0, n) w = List.foldl step (if m = 0 then finish n else (Mode.payload m, n)) rest
  rw [readNat_eq_some w m rest h,w:List Boolm:ℕrest:List Booln:ℕh:readNat w = some (m, rest)⊢ List.foldl step (Mode.zeros 0, n) (encodeNat m ++ rest) =
  List.foldl step (if m = 0 then finish n else (Mode.payload m, n)) rest List.foldl_append,w:List Boolm:ℕrest:List Booln:ℕh:readNat w = some (m, rest)⊢ List.foldl step (List.foldl step (Mode.zeros 0, n) (encodeNat m)) rest =
  List.foldl step (if m = 0 then finish n else (Mode.payload m, n)) rest foldl_encodeNatw:List Boolm:ℕrest:List Booln:ℕh:readNat w = some (m, rest)⊢ List.foldl step (if m = 0 then finish n else (Mode.payload m, n)) rest =
  List.foldl step (if m = 0 then finish n else (Mode.payload m, n)) rest]All goals completed! 🐙

A prefix with no terminating one remains in the unary header phase.

theorem foldl_zeros_none (w : List Bool) : ∀ z n, readZeros w = none →
    w.foldl step (.zeros z, n) = (.zeros (z + w.length), n) :=
  List.rec (fun _ _ _ ↦ rfl) (fun b bs ih z n h ↦ byw:List Boolb:Boolbs:List Boolih:∀ (z n : ℕ), readZeros bs = none → List.foldl step (Mode.zeros z, n) bs = (Mode.zeros (z + bs.length), n)z:ℕn:ℕh:readZeros (b :: bs) = none⊢ List.foldl step (Mode.zeros z, n) (b :: bs) = (Mode.zeros (z + (b :: bs).length), n)
    cases b with
    | true =>truew:List Boolbs:List Boolih:∀ (z n : ℕ), readZeros bs = none → List.foldl step (Mode.zeros z, n) bs = (Mode.zeros (z + bs.length), n)z:ℕn:ℕh:readZeros (true :: bs) = none⊢ List.foldl step (Mode.zeros z, n) (true :: bs) = (Mode.zeros (z + (true :: bs).length), n) cases hAll goals completed! 🐙
    | false =>falsew:List Boolbs:List Boolih:∀ (z n : ℕ), readZeros bs = none → List.foldl step (Mode.zeros z, n) bs = (Mode.zeros (z + bs.length), n)z:ℕn:ℕh:readZeros (false :: bs) = none⊢ List.foldl step (Mode.zeros z, n) (false :: bs) = (Mode.zeros (z + (false :: bs).length), n)
      have ht : readZeros bs = none := byw:List Boolb:Boolbs:List Boolih:∀ (z n : ℕ), readZeros bs = none → List.foldl step (Mode.zeros z, n) bs = (Mode.zeros (z + bs.length), n)z:ℕn:ℕh:readZeros (b :: bs) = none⊢ List.foldl step (Mode.zeros z, n) (b :: bs) = (Mode.zeros (z + (b :: bs).length), n)
        cases hx : readZeros bs with
        | none =>nonew:List Boolbs:List Boolih:∀ (z n : ℕ), readZeros bs = none → List.foldl step (Mode.zeros z, n) bs = (Mode.zeros (z + bs.length), n)z:ℕn:ℕh:readZeros (false :: bs) = nonehx:readZeros bs = none⊢ none = none rflAll goals completed! 🐙
        | some p =>somew:List Boolbs:List Boolih:∀ (z n : ℕ), readZeros bs = none → List.foldl step (Mode.zeros z, n) bs = (Mode.zeros (z + bs.length), n)z:ℕn:ℕh:readZeros (false :: bs) = nonep:ℕ × List Boolhx:readZeros bs = some p⊢ some p = none
          rw [readZeros_cons,somew:List Boolbs:List Boolih:∀ (z n : ℕ), readZeros bs = none → List.foldl step (Mode.zeros z, n) bs = (Mode.zeros (z + bs.length), n)z:ℕn:ℕh:(if false = true then some (0, bs) else Option.map (fun p ↦ (p.fst + 1, p.snd)) (readZeros bs)) = nonep:ℕ × List Boolhx:readZeros bs = some p⊢ some p = none hxsomew:List Boolbs:List Boolih:∀ (z n : ℕ), readZeros bs = none → List.foldl step (Mode.zeros z, n) bs = (Mode.zeros (z + bs.length), n)z:ℕn:ℕp:ℕ × List Boolh:(if false = true then some (0, bs) else Option.map (fun p ↦ (p.fst + 1, p.snd)) (some p)) = nonehx:readZeros bs = some p⊢ some p = none] at hsomew:List Boolbs:List Boolih:∀ (z n : ℕ), readZeros bs = none → List.foldl step (Mode.zeros z, n) bs = (Mode.zeros (z + bs.length), n)z:ℕn:ℕp:ℕ × List Boolh:(if false = true then some (0, bs) else Option.map (fun p ↦ (p.fst + 1, p.snd)) (some p)) = nonehx:readZeros bs = some p⊢ some p = none
          simp only [Bool.false_eq_true, ↓reduceIte, Option.map_some, reduceCtorEq] at hfalsew:List Boolbs:List Boolih:∀ (z n : ℕ), readZeros bs = none → List.foldl step (Mode.zeros z, n) bs = (Mode.zeros (z + bs.length), n)z:ℕn:ℕh:readZeros (false :: bs) = noneht:readZeros bs = none⊢ List.foldl step (Mode.zeros z, n) (false :: bs) = (Mode.zeros (z + (false :: bs).length), n)
      rw [List.foldl_consfalsew:List Boolbs:List Boolih:∀ (z n : ℕ), readZeros bs = none → List.foldl step (Mode.zeros z, n) bs = (Mode.zeros (z + bs.length), n)z:ℕn:ℕh:readZeros (false :: bs) = noneht:readZeros bs = none⊢ List.foldl step (step (Mode.zeros z, n) false) bs = (Mode.zeros (z + (false :: bs).length), n)]falsew:List Boolbs:List Boolih:∀ (z n : ℕ), readZeros bs = none → List.foldl step (Mode.zeros z, n) bs = (Mode.zeros (z + bs.length), n)z:ℕn:ℕh:readZeros (false :: bs) = noneht:readZeros bs = none⊢ List.foldl step (step (Mode.zeros z, n) false) bs = (Mode.zeros (z + (false :: bs).length), n)
      change bs.foldl step (.zeros (z + 1), n) = _falsew:List Boolbs:List Boolih:∀ (z n : ℕ), readZeros bs = none → List.foldl step (Mode.zeros z, n) bs = (Mode.zeros (z + bs.length), n)z:ℕn:ℕh:readZeros (false :: bs) = noneht:readZeros bs = none⊢ List.foldl step (Mode.zeros (z + 1), n) bs = (Mode.zeros (z + (false :: bs).length), n)
      rw [ih (z + 1) n htfalsew:List Boolbs:List Boolih:∀ (z n : ℕ), readZeros bs = none → List.foldl step (Mode.zeros z, n) bs = (Mode.zeros (z + bs.length), n)z:ℕn:ℕh:readZeros (false :: bs) = noneht:readZeros bs = none⊢ (Mode.zeros (z + 1 + bs.length), n) = (Mode.zeros (z + (false :: bs).length), n)]falsew:List Boolbs:List Boolih:∀ (z n : ℕ), readZeros bs = none → List.foldl step (Mode.zeros z, n) bs = (Mode.zeros (z + bs.length), n)z:ℕn:ℕh:readZeros (false :: bs) = noneht:readZeros bs = none⊢ (Mode.zeros (z + 1 + bs.length), n) = (Mode.zeros (z + (false :: bs).length), n)
      congr 2false.e_fstw:List Boolbs:List Boolih:∀ (z n : ℕ), readZeros bs = none → List.foldl step (Mode.zeros z, n) bs = (Mode.zeros (z + bs.length), n)z:ℕn:ℕh:readZeros (false :: bs) = noneht:readZeros bs = none⊢ z + 1 + bs.length = z + (false :: bs).length
      simp only [List.length_cons]false.e_fstw:List Boolbs:List Boolih:∀ (z n : ℕ), readZeros bs = none → List.foldl step (Mode.zeros z, n) bs = (Mode.zeros (z + bs.length), n)z:ℕn:ℕh:readZeros (false :: bs) = noneht:readZeros bs = none⊢ z + 1 + bs.length = z + (bs.length + 1)
      omegaAll goals completed! 🐙) w

Failure of a fixed-width read means the available input is too short.

theorem readFixed_none_lt (k : ℕ) (w : List Bool) (h : readFixed k w = none) :
    w.length < k := byk:ℕw:List Boolh:readFixed k w = none⊢ w.length < k
  unfold readFixed at hk:ℕw:List Boolh:(if k ≤ w.length then some (fromPayload (List.take k w), List.drop k w) else none) = none⊢ w.length < k
  split at hisTruek:ℕw:List Boolh✝:k ≤ w.lengthh:some (fromPayload (List.take k w), List.drop k w) = none⊢ w.length < kisFalsek:ℕw:List Boolh✝:¬k ≤ w.lengthh:none = none⊢ w.length < k
  next =>k:ℕw:List Boolh✝:k ≤ w.lengthh:some (fromPayload (List.take k w), List.drop k w) = none⊢ w.length < k contradictionAll goals completed! 🐙
  next hk =>k:ℕw:List Boolhk:¬k ≤ w.lengthh:none = none⊢ w.length < k omegaAll goals completed! 🐙

An incomplete gamma prefix cannot leave the header phases.

theorem gamma_reject (w : List Bool) (n : ℕ) (h : readGamma w = none) :
    (w.foldl step (.zeros 0, n)).1 ≠ .done := byw:List Booln:ℕh:readGamma w = none⊢ (List.foldl step (Mode.zeros 0, n) w).fst ≠ Mode.done
  cases hz : readZeros w with
  | none =>nonew:List Booln:ℕh:readGamma w = nonehz:readZeros w = none⊢ (List.foldl step (Mode.zeros 0, n) w).fst ≠ Mode.done rw [foldl_zeros_none w 0 n hznonew:List Booln:ℕh:readGamma w = nonehz:readZeros w = none⊢ (Mode.zeros (0 + w.length), n).fst ≠ Mode.done]nonew:List Booln:ℕh:readGamma w = nonehz:readZeros w = none⊢ (Mode.zeros (0 + w.length), n).fst ≠ Mode.done; intro henonew:List Booln:ℕh:readGamma w = nonehz:readZeros w = nonehe:(Mode.zeros (0 + w.length), n).fst = Mode.done⊢ False; cases heAll goals completed! 🐙
  | some p =>somew:List Booln:ℕh:readGamma w = nonep:ℕ × List Boolhz:readZeros w = some p⊢ (List.foldl step (Mode.zeros 0, n) w).fst ≠ Mode.done
    rcases p with ⟨z, suffix⟩somew:List Booln:ℕh:readGamma w = nonez:ℕsuffix:List Boolhz:readZeros w = some (z, suffix)⊢ (List.foldl step (Mode.zeros 0, n) w).fst ≠ Mode.done
    have hf : readFixed z suffix = none := by
      simpa only [readGamma, hz, Option.bind_some] using hsomew:List Booln:ℕh:readGamma w = nonez:ℕsuffix:List Boolhz:readZeros w = some (z, suffix)hf:readFixed z suffix = none⊢ (List.foldl step (Mode.zeros 0, n) w).fst ≠ Mode.done
    have hlt := readFixed_none_lt z suffix hfsomew:List Booln:ℕh:readGamma w = nonez:ℕsuffix:List Boolhz:readZeros w = some (z, suffix)hf:readFixed z suffix = nonehlt:suffix.length < z⊢ (List.foldl step (Mode.zeros 0, n) w).fst ≠ Mode.done
    have hz0 : z ≠ 0 := by omegasomew:List Booln:ℕh:readGamma w = nonez:ℕsuffix:List Boolhz:readZeros w = some (z, suffix)hf:readFixed z suffix = nonehlt:suffix.length < zhz0:z ≠ 0⊢ (List.foldl step (Mode.zeros 0, n) w).fst ≠ Mode.done
    rw [readZeros_eq_some w z suffix hz,somew:List Booln:ℕh:readGamma w = nonez:ℕsuffix:List Boolhz:readZeros w = some (z, suffix)hf:readFixed z suffix = nonehlt:suffix.length < zhz0:z ≠ 0⊢ (List.foldl step (Mode.zeros 0, n) (List.replicate z false ++ true :: suffix)).fst ≠ Mode.done List.foldl_append,somew:List Booln:ℕh:readGamma w = nonez:ℕsuffix:List Boolhz:readZeros w = some (z, suffix)hf:readFixed z suffix = nonehlt:suffix.length < zhz0:z ≠ 0⊢ (List.foldl step (List.foldl step (Mode.zeros 0, n) (List.replicate z false)) (true :: suffix)).fst ≠ Mode.done foldl_replicate_falsesomew:List Booln:ℕh:readGamma w = nonez:ℕsuffix:List Boolhz:readZeros w = some (z, suffix)hf:readFixed z suffix = nonehlt:suffix.length < zhz0:z ≠ 0⊢ (List.foldl step (Mode.zeros (0 + z), n) (true :: suffix)).fst ≠ Mode.done]somew:List Booln:ℕh:readGamma w = nonez:ℕsuffix:List Boolhz:readZeros w = some (z, suffix)hf:readFixed z suffix = nonehlt:suffix.length < zhz0:z ≠ 0⊢ (List.foldl step (Mode.zeros (0 + z), n) (true :: suffix)).fst ≠ Mode.done
    simp only [Nat.zero_add, List.foldl_cons, step, hz0, ↓reduceIte]somew:List Booln:ℕh:readGamma w = nonez:ℕsuffix:List Boolhz:readZeros w = some (z, suffix)hf:readFixed z suffix = nonehlt:suffix.length < zhz0:z ≠ 0⊢ (List.foldl step (Mode.size z 1, n) suffix).fst ≠ Mode.done
    have he := foldl_short_field true suffix z 1 n hltsomew:List Booln:ℕh:readGamma w = nonez:ℕsuffix:List Boolhz:readZeros w = some (z, suffix)hf:readFixed z suffix = nonehlt:suffix.length < zhz0:z ≠ 0he:List.foldl step (if true = true then Mode.size z 1 else Mode.length z 1, n) suffix =
  (if true = true then Mode.size (z - suffix.length) (List.foldl (fun a b ↦ Nat.bit b a) 1 suffix)
    else Mode.length (z - suffix.length) (List.foldl (fun a b ↦ Nat.bit b a) 1 suffix),
    n)⊢ (List.foldl step (Mode.size z 1, n) suffix).fst ≠ Mode.done
    simp only [↓reduceIte] at hesomew:List Booln:ℕh:readGamma w = nonez:ℕsuffix:List Boolhz:readZeros w = some (z, suffix)hf:readFixed z suffix = nonehlt:suffix.length < zhz0:z ≠ 0he:List.foldl step (Mode.size z 1, n) suffix =
  (Mode.size (z - suffix.length) (List.foldl (fun a b ↦ Nat.bit b a) 1 suffix), n)⊢ (List.foldl step (Mode.size z 1, n) suffix).fst ≠ Mode.done
    rw [hesomew:List Booln:ℕh:readGamma w = nonez:ℕsuffix:List Boolhz:readZeros w = some (z, suffix)hf:readFixed z suffix = nonehlt:suffix.length < zhz0:z ≠ 0he:List.foldl step (Mode.size z 1, n) suffix =
  (Mode.size (z - suffix.length) (List.foldl (fun a b ↦ Nat.bit b a) 1 suffix), n)⊢ (Mode.size (z - suffix.length) (List.foldl (fun a b ↦ Nat.bit b a) 1 suffix), n).fst ≠ Mode.done]somew:List Booln:ℕh:readGamma w = nonez:ℕsuffix:List Boolhz:readZeros w = some (z, suffix)hf:readFixed z suffix = nonehlt:suffix.length < zhz0:z ≠ 0he:List.foldl step (Mode.size z 1, n) suffix =
  (Mode.size (z - suffix.length) (List.foldl (fun a b ↦ Nat.bit b a) 1 suffix), n)⊢ (Mode.size (z - suffix.length) (List.foldl (fun a b ↦ Nat.bit b a) 1 suffix), n).fst ≠ Mode.done
    intro hhsomew:List Booln:ℕh:readGamma w = nonez:ℕsuffix:List Boolhz:readZeros w = some (z, suffix)hf:readFixed z suffix = nonehlt:suffix.length < zhz0:z ≠ 0he:List.foldl step (Mode.size z 1, n) suffix =
  (Mode.size (z - suffix.length) (List.foldl (fun a b ↦ Nat.bit b a) 1 suffix), n)hh:(Mode.size (z - suffix.length) (List.foldl (fun a b ↦ Nat.bit b a) 1 suffix), n).fst = Mode.done⊢ False
    cases hhAll goals completed! 🐙

An incomplete delta header cannot cause acceptance.

theorem header_reject (w : List Bool) (n : ℕ) (h : readNat w = none) :
    (w.foldl step (.zeros 0, n)).1 ≠ .done := byw:List Booln:ℕh:readNat w = none⊢ (List.foldl step (Mode.zeros 0, n) w).fst ≠ Mode.done
  cases hg : readGamma w with
  | none =>nonew:List Booln:ℕh:readNat w = nonehg:readGamma w = none⊢ (List.foldl step (Mode.zeros 0, n) w).fst ≠ Mode.done exact gamma_reject w n hgAll goals completed! 🐙
  | some p =>somew:List Booln:ℕh:readNat w = nonep:ℕ × List Boolhg:readGamma w = some p⊢ (List.foldl step (Mode.zeros 0, n) w).fst ≠ Mode.done
    rcases p with ⟨k, suffix⟩somew:List Booln:ℕh:readNat w = nonek:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)⊢ (List.foldl step (Mode.zeros 0, n) w).fst ≠ Mode.done
    obtain ⟨hk, hw⟩ := readGamma_eq_some w k suffix hgsomew:List Booln:ℕh:readNat w = nonek:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffix⊢ (List.foldl step (Mode.zeros 0, n) w).fst ≠ Mode.done
    have hf : readFixed (k - 1) suffix = none := by
      cases hx : readFixed (k - 1) suffix with
      | none =>nonew:List Booln:ℕh:readNat w = nonek:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixhx:readFixed (k - 1) suffix = none⊢ none = none rflAll goals completed! 🐙
      | some p =>somew:List Booln:ℕh:readNat w = nonek:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixp:ℕ × List Boolhx:readFixed (k - 1) suffix = some p⊢ some p = none
        simp only [readNat, hg, Option.bind_some, hx, reduceCtorEq] at hsomew:List Booln:ℕh:readNat w = nonek:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixhf:readFixed (k - 1) suffix = none⊢ (List.foldl step (Mode.zeros 0, n) w).fst ≠ Mode.done
    have hlt := readFixed_none_lt (k - 1) suffix hfsomew:List Booln:ℕh:readNat w = nonek:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixhf:readFixed (k - 1) suffix = nonehlt:suffix.length < k - 1⊢ (List.foldl step (Mode.zeros 0, n) w).fst ≠ Mode.done
    have hk1 : k ≠ 1 := by omegasomew:List Booln:ℕh:readNat w = nonek:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixhf:readFixed (k - 1) suffix = nonehlt:suffix.length < k - 1hk1:k ≠ 1⊢ (List.foldl step (Mode.zeros 0, n) w).fst ≠ Mode.done
    rw [hw,somew:List Booln:ℕh:readNat w = nonek:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixhf:readFixed (k - 1) suffix = nonehlt:suffix.length < k - 1hk1:k ≠ 1⊢ (List.foldl step (Mode.zeros 0, n) (encodeGamma k ++ suffix)).fst ≠ Mode.done List.foldl_append,somew:List Booln:ℕh:readNat w = nonek:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixhf:readFixed (k - 1) suffix = nonehlt:suffix.length < k - 1hk1:k ≠ 1⊢ (List.foldl step (List.foldl step (Mode.zeros 0, n) (encodeGamma k)) suffix).fst ≠ Mode.done foldl_gamma k hk n,somew:List Booln:ℕh:readNat w = nonek:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixhf:readFixed (k - 1) suffix = nonehlt:suffix.length < k - 1hk1:k ≠ 1⊢ (List.foldl step (if k = 1 then finish n else (Mode.length (k - 1) 1, n)) suffix).fst ≠ Mode.done ite_eq_right hk1somew:List Booln:ℕh:readNat w = nonek:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixhf:readFixed (k - 1) suffix = nonehlt:suffix.length < k - 1hk1:k ≠ 1⊢ (List.foldl step (Mode.length (k - 1) 1, n) suffix).fst ≠ Mode.done]somew:List Booln:ℕh:readNat w = nonek:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixhf:readFixed (k - 1) suffix = nonehlt:suffix.length < k - 1hk1:k ≠ 1⊢ (List.foldl step (Mode.length (k - 1) 1, n) suffix).fst ≠ Mode.done
    have he := foldl_short_field false suffix (k - 1) 1 n hltsomew:List Booln:ℕh:readNat w = nonek:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixhf:readFixed (k - 1) suffix = nonehlt:suffix.length < k - 1hk1:k ≠ 1he:List.foldl step (if false = true then Mode.size (k - 1) 1 else Mode.length (k - 1) 1, n) suffix =
  (if false = true then Mode.size (k - 1 - suffix.length) (List.foldl (fun a b ↦ Nat.bit b a) 1 suffix)
    else Mode.length (k - 1 - suffix.length) (List.foldl (fun a b ↦ Nat.bit b a) 1 suffix),
    n)⊢ (List.foldl step (Mode.length (k - 1) 1, n) suffix).fst ≠ Mode.done
    simp only [Bool.false_eq_true, ↓reduceIte] at hesomew:List Booln:ℕh:readNat w = nonek:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixhf:readFixed (k - 1) suffix = nonehlt:suffix.length < k - 1hk1:k ≠ 1he:List.foldl step (Mode.length (k - 1) 1, n) suffix =
  (Mode.length (k - 1 - suffix.length) (List.foldl (fun a b ↦ Nat.bit b a) 1 suffix), n)⊢ (List.foldl step (Mode.length (k - 1) 1, n) suffix).fst ≠ Mode.done
    rw [hesomew:List Booln:ℕh:readNat w = nonek:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixhf:readFixed (k - 1) suffix = nonehlt:suffix.length < k - 1hk1:k ≠ 1he:List.foldl step (Mode.length (k - 1) 1, n) suffix =
  (Mode.length (k - 1 - suffix.length) (List.foldl (fun a b ↦ Nat.bit b a) 1 suffix), n)⊢ (Mode.length (k - 1 - suffix.length) (List.foldl (fun a b ↦ Nat.bit b a) 1 suffix), n).fst ≠ Mode.done]somew:List Booln:ℕh:readNat w = nonek:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixhf:readFixed (k - 1) suffix = nonehlt:suffix.length < k - 1hk1:k ≠ 1he:List.foldl step (Mode.length (k - 1) 1, n) suffix =
  (Mode.length (k - 1 - suffix.length) (List.foldl (fun a b ↦ Nat.bit b a) 1 suffix), n)⊢ (Mode.length (k - 1 - suffix.length) (List.foldl (fun a b ↦ Nat.bit b a) 1 suffix), n).fst ≠ Mode.done
    intro hhsomew:List Booln:ℕh:readNat w = nonek:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixhf:readFixed (k - 1) suffix = nonehlt:suffix.length < k - 1hk1:k ≠ 1he:List.foldl step (Mode.length (k - 1) 1, n) suffix =
  (Mode.length (k - 1 - suffix.length) (List.foldl (fun a b ↦ Nat.bit b a) 1 suffix), n)hh:(Mode.length (k - 1 - suffix.length) (List.foldl (fun a b ↦ Nat.bit b a) 1 suffix), n).fst = Mode.done⊢ False
    cases hhAll goals completed! 🐙

end Geb.BitTree.Elias.Scanner