Geb.Mathlib.Data.Tree.Ranked.Code

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.Mathlib.Data.Tree.Ranked.Basic
public import Mathlib.Algebra.GroupWithZero.Nat

Symbol codes

The block spelling a symbol of a ranked alphabet: its index in binary, least significant bit first, padded to the alphabet's width. A block decodes to the symbol it spells, which is what makes the padding lossless, and a block denoting no symbol has no arity.

Main definitions

RankedAlphabet.code — the block spelling a symbol.

RankedAlphabet.decodeBits — the value a block denotes.

RankedAlphabet.arOf — the arity of the symbol a block denotes.

Main statements

RankedAlphabet.length_code — every block has the alphabet's width.

RankedAlphabet.decodeBits_code — a block decodes to its own symbol.

RankedAlphabet.arOf_decodeBits_code — and so has that symbol's arity.

RankedAlphabet.testBit_decodeBits — a block's entries are its value's bits.

RankedAlphabet.getElem_code_eq — and a block's entries are the bits of the symbol's index.

RankedAlphabet.le_maxArity_of_arOf_eq_some — an arity a block yields is at most the largest.

Implementation notes

decodeBits is a bare List.rec, so Lean generates no equation lemma for it; decodeBits_cons is stated for the rewrites that need one.

mod_two_mul is stated here rather than taken from Nat's division API: Nat.mod_mul states the same identity and depends on Classical.choice, which the axiom linter rejects for this module, and its modulus is a variable, so omega cannot discharge the identity directly. The proof below runs through Nat.div_add_mod, Nat.mul_add_mod and Nat.mod_eq_of_lt, all of which are choice-free.

Tags

ranked alphabet, code, binary representation, decoding

namespace RankedAlphabetpublic section

The block spelling a symbol: its index in binary, least significant bit first, padded to the alphabet's width.

@[`@[expose]` has no effect outside a `module` fileexpose] def code (R : RankedAlphabet) (i : Fin R.card) : List Bool :=
  (List.range R.width).map fun j ↦ i.val.testBit j

The value a block denotes, its head the least significant bit.

@[`@[expose]` has no effect outside a `module` fileexpose] def decodeBits : List Bool → ℕ :=
  List.rec 0 fun b _ ih ↦ 2 * ih + (if b then 1 else 0)

decodeBits unfolded on a non-empty block. decodeBits is a bare List.rec, for which Lean generates no equation lemma.

theorem decodeBits_cons (b : Bool) (l : List Bool) :
    decodeBits (b :: l) = 2 * decodeBits l + (if b then 1 else 0) := rfl

The arity of the symbol a block denotes, absent at a block denoting none.

@[`@[expose]` has no effect outside a `module` fileexpose] def arOf (R : RankedAlphabet) (v : ℕ) : Option ℕ :=
  if h : v < R.card then some (R.arity ⟨v, h⟩) else none

Every block has the alphabet's width.

@[simp] theorem length_code (R : RankedAlphabet) (i : Fin R.card) :
    (R.code i).length = R.width := byR:RankedAlphabeti:Fin R.card⊢ (R.code i).length = R.width
  simp only [code, List.length_map, List.length_range]All goals completed! 🐙

Splitting a residue by a factor of two, choice-free.

theorem mod_two_mul (v m : ℕ) (hm : 0 < m) :
    v % (2 * m) = 2 * (v / 2 % m) + v % 2 := byv:ℕm:ℕhm:0 < m⊢ v % (2 * m) = 2 * (v / 2 % m) + v % 2
  have h2 : (0 : ℕ) < 2 := by omegav:ℕm:ℕhm:0 < mh2:0 < 2⊢ v % (2 * m) = 2 * (v / 2 % m) + v % 2
  have hlt1 : v / 2 % m < m := Nat.mod_lt _ hmv:ℕm:ℕhm:0 < mh2:0 < 2hlt1:v / 2 % m < m⊢ v % (2 * m) = 2 * (v / 2 % m) + v % 2
  have hlt2 : v % 2 < 2 := Nat.mod_lt _ h2v:ℕm:ℕhm:0 < mh2:0 < 2hlt1:v / 2 % m < mhlt2:v % 2 < 2⊢ v % (2 * m) = 2 * (v / 2 % m) + v % 2
  conv_lhs => rw [← Nat.div_add_mod v 2, ← Nat.div_add_mod (v / 2) m]v:ℕm:ℕhm:0 < mh2:0 < 2hlt1:v / 2 % m < mhlt2:v % 2 < 2| (2 * (m * (v / 2 / m) + v / 2 % m) + v % 2) % (2 * m)
  rw [Nat.mul_add,v:ℕm:ℕhm:0 < mh2:0 < 2hlt1:v / 2 % m < mhlt2:v % 2 < 2⊢ (2 * (m * (v / 2 / m)) + 2 * (v / 2 % m) + v % 2) % (2 * m) = 2 * (v / 2 % m) + v % 2 ← Nat.mul_assoc,v:ℕm:ℕhm:0 < mh2:0 < 2hlt1:v / 2 % m < mhlt2:v % 2 < 2⊢ (2 * m * (v / 2 / m) + 2 * (v / 2 % m) + v % 2) % (2 * m) = 2 * (v / 2 % m) + v % 2 Nat.add_assoc,v:ℕm:ℕhm:0 < mh2:0 < 2hlt1:v / 2 % m < mhlt2:v % 2 < 2⊢ (2 * m * (v / 2 / m) + (2 * (v / 2 % m) + v % 2)) % (2 * m) = 2 * (v / 2 % m) + v % 2 Nat.mul_add_modv:ℕm:ℕhm:0 < mh2:0 < 2hlt1:v / 2 % m < mhlt2:v % 2 < 2⊢ (2 * (v / 2 % m) + v % 2) % (2 * m) = 2 * (v / 2 % m) + v % 2]v:ℕm:ℕhm:0 < mh2:0 < 2hlt1:v / 2 % m < mhlt2:v % 2 < 2⊢ (2 * (v / 2 % m) + v % 2) % (2 * m) = 2 * (v / 2 % m) + v % 2
  exact Nat.mod_eq_of_lt (byv:ℕm:ℕhm:0 < mh2:0 < 2hlt1:v / 2 % m < mhlt2:v % 2 < 2⊢ 2 * (v / 2 % m) + v % 2 < 2 * m omegaAll goals completed! 🐙)

A block decodes to the symbol it spells. The bound i.val < 2 ^ width comes from card_le_two_pow_width, and is what makes the padding lossless.

theorem decodeBits_code (R : RankedAlphabet) (i : Fin R.card) :
    decodeBits (R.code i) = i.val := byR:RankedAlphabeti:Fin R.card⊢ decodeBits (R.code i) = ↑i
  have hlt : i.val < 2 ^ R.width :=
    Nat.lt_of_lt_of_le i.isLt R.card_le_two_pow_widthR:RankedAlphabeti:Fin R.cardhlt:↑i < 2 ^ R.width⊢ decodeBits (R.code i) = ↑i
  have key : ∀ (n : ℕ) (v : ℕ),
      decodeBits ((List.range n).map fun j ↦ v.testBit j) = v % 2 ^ n := by
    refine Nat.rec (motive := fun n ↦ ∀ v : ℕ,
        decodeBits ((List.range n).map fun j ↦ v.testBit j) = v % 2 ^ n)
      (fun v ↦ byR:RankedAlphabeti:Fin R.cardhlt:↑i < 2 ^ R.widthv:ℕ⊢ decodeBits (List.map (fun j ↦ v.testBit j) (List.range Nat.zero)) = v % 2 ^ Nat.zero
        simp only [List.range_zero, List.map_nil, decodeBits, Nat.pow_zero, Nat.mod_one]All goals completed! 🐙)
      (fun n ihn v ↦ ?_)
    rw [List.range_succ_eq_map,R:RankedAlphabeti:Fin R.cardhlt:↑i < 2 ^ R.widthn:ℕihn:∀ (v : ℕ), decodeBits (List.map (fun j ↦ v.testBit j) (List.range n)) = v % 2 ^ nv:ℕ⊢ decodeBits (List.map (fun j ↦ v.testBit j) (0 :: List.map Nat.succ (List.range n))) = v % 2 ^ n.succ List.map_cons,R:RankedAlphabeti:Fin R.cardhlt:↑i < 2 ^ R.widthn:ℕihn:∀ (v : ℕ), decodeBits (List.map (fun j ↦ v.testBit j) (List.range n)) = v % 2 ^ nv:ℕ⊢ decodeBits (v.testBit 0 :: List.map (fun j ↦ v.testBit j) (List.map Nat.succ (List.range n))) = v % 2 ^ n.succ List.map_mapR:RankedAlphabeti:Fin R.cardhlt:↑i < 2 ^ R.widthn:ℕihn:∀ (v : ℕ), decodeBits (List.map (fun j ↦ v.testBit j) (List.range n)) = v % 2 ^ nv:ℕ⊢ decodeBits (v.testBit 0 :: List.map ((fun j ↦ v.testBit j) ∘ Nat.succ) (List.range n)) = v % 2 ^ n.succ]R:RankedAlphabeti:Fin R.cardhlt:↑i < 2 ^ R.widthn:ℕihn:∀ (v : ℕ), decodeBits (List.map (fun j ↦ v.testBit j) (List.range n)) = v % 2 ^ nv:ℕ⊢ decodeBits (v.testBit 0 :: List.map ((fun j ↦ v.testBit j) ∘ Nat.succ) (List.range n)) = v % 2 ^ n.succ
    simp only [Function.comp_def, Nat.succ_eq_add_one, Nat.testBit_add_one]R:RankedAlphabeti:Fin R.cardhlt:↑i < 2 ^ R.widthn:ℕihn:∀ (v : ℕ), decodeBits (List.map (fun j ↦ v.testBit j) (List.range n)) = v % 2 ^ nv:ℕ⊢ decodeBits (v.testBit 0 :: List.map (fun x ↦ (v / 2).testBit x) (List.range n)) = v % 2 ^ (n + 1)
    rw [decodeBits_cons,R:RankedAlphabeti:Fin R.cardhlt:↑i < 2 ^ R.widthn:ℕihn:∀ (v : ℕ), decodeBits (List.map (fun j ↦ v.testBit j) (List.range n)) = v % 2 ^ nv:ℕ⊢ (2 * decodeBits (List.map (fun x ↦ (v / 2).testBit x) (List.range n)) + if v.testBit 0 = true then 1 else 0) =
  v % 2 ^ (n + 1) ihn (v / 2),R:RankedAlphabeti:Fin R.cardhlt:↑i < 2 ^ R.widthn:ℕihn:∀ (v : ℕ), decodeBits (List.map (fun j ↦ v.testBit j) (List.range n)) = v % 2 ^ nv:ℕ⊢ (2 * (v / 2 % 2 ^ n) + if v.testBit 0 = true then 1 else 0) = v % 2 ^ (n + 1) Nat.testBit_zero,R:RankedAlphabeti:Fin R.cardhlt:↑i < 2 ^ R.widthn:ℕihn:∀ (v : ℕ), decodeBits (List.map (fun j ↦ v.testBit j) (List.range n)) = v % 2 ^ nv:ℕ⊢ (2 * (v / 2 % 2 ^ n) + if decide (v % 2 = 1) = true then 1 else 0) = v % 2 ^ (n + 1) pow_succ',R:RankedAlphabeti:Fin R.cardhlt:↑i < 2 ^ R.widthn:ℕihn:∀ (v : ℕ), decodeBits (List.map (fun j ↦ v.testBit j) (List.range n)) = v % 2 ^ nv:ℕ⊢ (2 * (v / 2 % 2 ^ n) + if decide (v % 2 = 1) = true then 1 else 0) = v % (2 * 2 ^ n)
      mod_two_mul _ _ (Nat.two_pow_pos n)R:RankedAlphabeti:Fin R.cardhlt:↑i < 2 ^ R.widthn:ℕihn:∀ (v : ℕ), decodeBits (List.map (fun j ↦ v.testBit j) (List.range n)) = v % 2 ^ nv:ℕ⊢ (2 * (v / 2 % 2 ^ n) + if decide (v % 2 = 1) = true then 1 else 0) = 2 * (v / 2 % 2 ^ n) + v % 2]R:RankedAlphabeti:Fin R.cardhlt:↑i < 2 ^ R.widthn:ℕihn:∀ (v : ℕ), decodeBits (List.map (fun j ↦ v.testBit j) (List.range n)) = v % 2 ^ nv:ℕ⊢ (2 * (v / 2 % 2 ^ n) + if decide (v % 2 = 1) = true then 1 else 0) = 2 * (v / 2 % 2 ^ n) + v % 2
    rcases Nat.mod_two_eq_zero_or_one v with h | hinlR:RankedAlphabeti:Fin R.cardhlt:↑i < 2 ^ R.widthn:ℕihn:∀ (v : ℕ), decodeBits (List.map (fun j ↦ v.testBit j) (List.range n)) = v % 2 ^ nv:ℕh:v % 2 = 0⊢ (2 * (v / 2 % 2 ^ n) + if decide (v % 2 = 1) = true then 1 else 0) = 2 * (v / 2 % 2 ^ n) + v % 2inrR:RankedAlphabeti:Fin R.cardhlt:↑i < 2 ^ R.widthn:ℕihn:∀ (v : ℕ), decodeBits (List.map (fun j ↦ v.testBit j) (List.range n)) = v % 2 ^ nv:ℕh:v % 2 = 1⊢ (2 * (v / 2 % 2 ^ n) + if decide (v % 2 = 1) = true then 1 else 0) = 2 * (v / 2 % 2 ^ n) + v % 2 <;>inlR:RankedAlphabeti:Fin R.cardhlt:↑i < 2 ^ R.widthn:ℕihn:∀ (v : ℕ), decodeBits (List.map (fun j ↦ v.testBit j) (List.range n)) = v % 2 ^ nv:ℕh:v % 2 = 0⊢ (2 * (v / 2 % 2 ^ n) + if decide (v % 2 = 1) = true then 1 else 0) = 2 * (v / 2 % 2 ^ n) + v % 2inrR:RankedAlphabeti:Fin R.cardhlt:↑i < 2 ^ R.widthn:ℕihn:∀ (v : ℕ), decodeBits (List.map (fun j ↦ v.testBit j) (List.range n)) = v % 2 ^ nv:ℕh:v % 2 = 1⊢ (2 * (v / 2 % 2 ^ n) + if decide (v % 2 = 1) = true then 1 else 0) = 2 * (v / 2 % 2 ^ n) + v % 2 simp [h, Nat.add_comm]R:RankedAlphabeti:Fin R.cardhlt:↑i < 2 ^ R.widthkey:∀ (n v : ℕ), decodeBits (List.map (fun j ↦ v.testBit j) (List.range n)) = v % 2 ^ n⊢ decodeBits (R.code i) = ↑i
  rw [code,R:RankedAlphabeti:Fin R.cardhlt:↑i < 2 ^ R.widthkey:∀ (n v : ℕ), decodeBits (List.map (fun j ↦ v.testBit j) (List.range n)) = v % 2 ^ n⊢ decodeBits (List.map (fun j ↦ (↑i).testBit j) (List.range R.width)) = ↑i key,R:RankedAlphabeti:Fin R.cardhlt:↑i < 2 ^ R.widthkey:∀ (n v : ℕ), decodeBits (List.map (fun j ↦ v.testBit j) (List.range n)) = v % 2 ^ n⊢ ↑i % 2 ^ R.width = ↑i Nat.mod_eq_of_lt hltR:RankedAlphabeti:Fin R.cardhlt:↑i < 2 ^ R.widthkey:∀ (n v : ℕ), decodeBits (List.map (fun j ↦ v.testBit j) (List.range n)) = v % 2 ^ n⊢ ↑i = ↑i]All goals completed! 🐙

A block spelling a symbol has that symbol's arity.

theorem arOf_decodeBits_code (R : RankedAlphabet) (i : Fin R.card) :
    R.arOf (decodeBits (R.code i)) = some (R.arity i) := byR:RankedAlphabeti:Fin R.card⊢ R.arOf (decodeBits (R.code i)) = some (R.arity i)
  rw [decodeBits_code,R:RankedAlphabeti:Fin R.card⊢ R.arOf ↑i = some (R.arity i) arOf,R:RankedAlphabeti:Fin R.card⊢ (if h : ↑i < R.card then some (R.arity ⟨↑i, h⟩) else none) = some (R.arity i) dite_eq_left i.isLtR:RankedAlphabeti:Fin R.card⊢ some (R.arity ⟨↑i, ⋯⟩) = some (R.arity i)]All goals completed! 🐙

The nth bit of a block is the nth bit of the symbol's index.

theorem getElem_code_eq (R : RankedAlphabet) (i : Fin R.card) (n : ℕ)
    (h : n < (R.code i).length) : (R.code i)[n] = i.val.testBit n := byR:RankedAlphabeti:Fin R.cardn:ℕh:n < (R.code i).length⊢ (R.code i)[n] = (↑i).testBit n
  simp only [code, List.getElem_map, List.getElem_range]All goals completed! 🐙

The nth bit of a block's value is the block's nth entry.

theorem testBit_decodeBits : ∀ (bs : List Bool) (n : ℕ) (_ : n < bs.length),
    (decodeBits bs).testBit n = bs[n] :=
  List.rec (fun n h ↦ absurd h (byn:ℕh:n < [].length⊢ ¬n < [].length simpAll goals completed! 🐙))
    (fun b bs ih n h ↦ byb:Boolbs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]n:ℕh:n < (b :: bs).length⊢ (decodeBits (b :: bs)).testBit n = (b :: bs)[n]
      cases n with
      | zero =>zerob:Boolbs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]h:0 < (b :: bs).length⊢ (decodeBits (b :: bs)).testBit 0 = (b :: bs)[0]
        rw [decodeBits_cons,zerob:Boolbs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]h:0 < (b :: bs).length⊢ (2 * decodeBits bs + if b = true then 1 else 0).testBit 0 = (b :: bs)[0] Nat.testBit_zero,zerob:Boolbs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]h:0 < (b :: bs).length⊢ decide ((2 * decodeBits bs + if b = true then 1 else 0) % 2 = 1) = (b :: bs)[0] List.getElem_cons_zerozerob:Boolbs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]h:0 < (b :: bs).length⊢ decide ((2 * decodeBits bs + if b = true then 1 else 0) % 2 = 1) = b]zerob:Boolbs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]h:0 < (b :: bs).length⊢ decide ((2 * decodeBits bs + if b = true then 1 else 0) % 2 = 1) = b
        cases bzero.falsebs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]h:0 < (false :: bs).length⊢ decide ((2 * decodeBits bs + if false = true then 1 else 0) % 2 = 1) = falsezero.truebs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]h:0 < (true :: bs).length⊢ decide ((2 * decodeBits bs + if true = true then 1 else 0) % 2 = 1) = true <;>zero.falsebs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]h:0 < (false :: bs).length⊢ decide ((2 * decodeBits bs + if false = true then 1 else 0) % 2 = 1) = falsezero.truebs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]h:0 < (true :: bs).length⊢ decide ((2 * decodeBits bs + if true = true then 1 else 0) % 2 = 1) = true simpAll goals completed! 🐙
      | succ n =>succb:Boolbs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]n:ℕh:n + 1 < (b :: bs).length⊢ (decodeBits (b :: bs)).testBit (n + 1) = (b :: bs)[n + 1]
        rw [decodeBits_cons,succb:Boolbs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]n:ℕh:n + 1 < (b :: bs).length⊢ (2 * decodeBits bs + if b = true then 1 else 0).testBit (n + 1) = (b :: bs)[n + 1] Nat.testBit_add_onesuccb:Boolbs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]n:ℕh:n + 1 < (b :: bs).length⊢ ((2 * decodeBits bs + if b = true then 1 else 0) / 2).testBit n = (b :: bs)[n + 1]]succb:Boolbs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]n:ℕh:n + 1 < (b :: bs).length⊢ ((2 * decodeBits bs + if b = true then 1 else 0) / 2).testBit n = (b :: bs)[n + 1]
        have hd : (2 * decodeBits bs + (if b then 1 else 0)) / 2 = decodeBits bs := byb:Boolbs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]n:ℕh:n < (b :: bs).length⊢ (decodeBits (b :: bs)).testBit n = (b :: bs)[n]
          cases bfalsebs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]n:ℕh:n + 1 < (false :: bs).length⊢ (2 * decodeBits bs + if false = true then 1 else 0) / 2 = decodeBits bstruebs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]n:ℕh:n + 1 < (true :: bs).length⊢ (2 * decodeBits bs + if true = true then 1 else 0) / 2 = decodeBits bs <;>falsebs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]n:ℕh:n + 1 < (false :: bs).length⊢ (2 * decodeBits bs + if false = true then 1 else 0) / 2 = decodeBits bstruebs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]n:ℕh:n + 1 < (true :: bs).length⊢ (2 * decodeBits bs + if true = true then 1 else 0) / 2 = decodeBits bs (simp only [Bool.false_eq_true, ite_false, ite_true]truebs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]n:ℕh:n + 1 < (true :: bs).length⊢ (2 * decodeBits bs + 1) / 2 = decodeBits bs; omegaAll goals completed! 🐙)succb:Boolbs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]n:ℕh:n + 1 < (b :: bs).lengthhd:(2 * decodeBits bs + if b = true then 1 else 0) / 2 = decodeBits bs⊢ ((2 * decodeBits bs + if b = true then 1 else 0) / 2).testBit n = (b :: bs)[n + 1]
        rw [hd,succb:Boolbs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]n:ℕh:n + 1 < (b :: bs).lengthhd:(2 * decodeBits bs + if b = true then 1 else 0) / 2 = decodeBits bs⊢ (decodeBits bs).testBit n = (b :: bs)[n + 1] ih n (byb:Boolbs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]n:ℕh:n + 1 < (b :: bs).lengthhd:(2 * decodeBits bs + if b = true then 1 else 0) / 2 = decodeBits bs⊢ n < bs.length simpa using hAll goals completed! 🐙)]succb:Boolbs:List Boolih:∀ (n : ℕ) (x : n < bs.length), (decodeBits bs).testBit n = bs[n]n:ℕh:n + 1 < (b :: bs).lengthhd:(2 * decodeBits bs + if b = true then 1 else 0) / 2 = decodeBits bs⊢ bs[n] = (b :: bs)[n + 1]
        simpAll goals completed! 🐙)

Every arity a block yields is at most the largest, arOf returning an arity only in the image of arity.

theorem le_maxArity_of_arOf_eq_some (R : RankedAlphabet) {v r : ℕ}
    (h : R.arOf v = some r) : r ≤ R.maxArity := byR:RankedAlphabetv:ℕr:ℕh:R.arOf v = some r⊢ r ≤ R.maxArity
  rw [arOfR:RankedAlphabetv:ℕr:ℕh:(if h : v < R.card then some (R.arity ⟨v, h⟩) else none) = some r⊢ r ≤ R.maxArity] at hR:RankedAlphabetv:ℕr:ℕh:(if h : v < R.card then some (R.arity ⟨v, h⟩) else none) = some r⊢ r ≤ R.maxArity
  split at hisTrueR:RankedAlphabetv:ℕr:ℕh✝:v < R.cardh:some (R.arity ⟨v, h✝⟩) = some r⊢ r ≤ R.maxArityisFalseR:RankedAlphabetv:ℕr:ℕh✝:¬v < R.cardh:none = some r⊢ r ≤ R.maxArity
  ·isTrueR:RankedAlphabetv:ℕr:ℕh✝:v < R.cardh:some (R.arity ⟨v, h✝⟩) = some r⊢ r ≤ R.maxArity rename_i hltisTrueR:RankedAlphabetv:ℕr:ℕhlt:v < R.cardh:some (R.arity ⟨v, h✝⟩) = some r⊢ r ≤ R.maxArity
    rw [← Option.some.inj hisTrueR:RankedAlphabetv:ℕr:ℕhlt:v < R.cardh:some (R.arity ⟨v, h✝⟩) = some r⊢ R.arity ⟨v, hlt⟩ ≤ R.maxArity]isTrueR:RankedAlphabetv:ℕr:ℕhlt:v < R.cardh:some (R.arity ⟨v, h✝⟩) = some r⊢ R.arity ⟨v, hlt⟩ ≤ R.maxArity
    exact arity_le_maxArity R ⟨v, hlt⟩All goals completed! 🐙
  ·isFalseR:RankedAlphabetv:ℕr:ℕh✝:¬v < R.cardh:none = some r⊢ r ≤ R.maxArity exact absurd h (byR:RankedAlphabetv:ℕr:ℕh✝:¬v < R.cardh:none = some r⊢ ¬none = some r nofunAll goals completed! 🐙)

endend RankedAlphabet