1. Geb
  2. Prototypes
  3. Computability
  4. CobhamFoldProto
  5. Layout
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.CobhamFoldProto.Fold public import Geb.Mathlib.Computability.Cobham.RankedTree

The fold scan's state as a bitstring

Cobham.stateWord lays RankedAlphabet.Scan out as a bitstring: the liveness flag, the incomplete block in a slot of the alphabet's width, then the pending count in unary. This module lays Geb.CobhamFold.FoldScan out the same way, with the unary count replaced by one block per stack entry.

Each entry occupies p + 1 bits: a true presence marker followed by the p bits of the carrier's encoding. The marker is what the unary count's true already was, so at p = 0 — the carrier Unit, whose encoding is empty — the layout is Cobham.stateWord and the dispatch window is Cobham.dispatchWidth, which Geb.CobhamFold.stateWordF_unit and Geb.CobhamFold.dispatchWidthF_zero state. The layout generalizes the recognizer's rather than sitting beside it.

The marker is not redundant at p > 0. Cobham.bits pads a window past the word's end with false, and a carrier value may encode to all-false, so without a marker the padding would be indistinguishable from a stack entry. The marker separates them: the run of markers gives the stack's height capped at the window, which is what decides whether a symbol's arity is available.

Main definitions

    Geb.CobhamFold.entryBits, Geb.CobhamFold.stackBits — one stack entry, and the stack, as bitstrings.

    Geb.CobhamFold.stateWordF — the fold scan's state as a bitstring.

    Geb.CobhamFold.dispatchWidthF — the number of state bits a step dispatches on.

    Geb.CobhamFold.decodeStack, Geb.CobhamFold.decodeStateAt, Geb.CobhamFold.decodeStateF — the inverse of the layout, at an arbitrary window and at the dispatch window.

    Geb.CobhamFold.dropCountF, Geb.CobhamFold.nextPrefixF — the bits a step drops and prepends.

Main statements

    Geb.CobhamFold.length_stackBits, Geb.CobhamFold.length_stateWordF_of_lt — the layout's lengths.

    Geb.CobhamFold.take_stackBits, Geb.CobhamFold.drop_stackBits, Geb.CobhamFold.drop_stackBits_mul — the stack's layout truncated, advanced by one entry, and advanced by several.

    Geb.CobhamFold.ofFn_bits_stateWordF — the state word truncated to a window and zero-padded.

    Geb.CobhamFold.decodeStateAt_stateWordF_of_lt, Geb.CobhamFold.decodeStateF_stateWordF_of_lt — the decoder inverts the layout up to truncating the stack at the window.

    Geb.CobhamFold.dropCountF_take_stack, Geb.CobhamFold.nextPrefixF_take_stack — truncating the stack at the window changes neither.

    Geb.CobhamFold.stateWordF_foldScanStep_of_lt — a step rewrites a bounded prefix and drops a bounded number of bits.

    Geb.CobhamFold.length_stateWordF_not_le_add — at the two-symbol alphabet, whose width is one, the additive bound Cobham.scan admits fails of this layout at every positive carrier width.

Implementation notes

dispatchWidthF reads R.maxArity + 1 entries. R.maxArity of them are what a symbol's algebra can consume; the extra one distinguishes a stack of exactly R.maxArity entries from a longer one, which is what decides r ≤ height for every arity r, RankedAlphabet.le_maxArity_of_arOf_eq_some bounding the arities. This is Cobham.dispatchWidth's R.maxArity + 1 window, one entry wide rather than one bit wide.

decodeStack recurses on a fuel argument by Nat.rec rather than on the word, so no def here calls itself.

decodeStateF reads the stack through List operations rather than by Fin arithmetic, for the reason Cobham.decodeState records: a branch family's domain is Fin (dispatchWidthF R p) → Bool at a symbolic width, and indexing it would carry a bound proof at every step, while DecidableEq (Fin n → Bool) depends on Classical.choice: it resolves through FinEnum.decidablePiFinEnum, which is choice-free, at mathlib's FinEnum.fin, which is not.

The retraction hypothesis ∀ a, dec (enc a) = a enters only at decodeStateF_stateWordF_of_lt; the lengths and the step lemma hold whatever dec does off the image of enc, as they do in Geb/Mathlib/Computability/Cobham/Fold.lean.

References

    [Cobham1965]

Tags

Cobham, ranked alphabet, preorder, fold, state layout, stack

@[expose] public sectionnamespace Geb.CobhamFoldopen Cobham RankedAlphabetuniverse uvariable {α : Type u} {p : ℕ}

One stack entry as a bitstring: a true presence marker followed by the carrier's encoding.

def entryBits (enc : α → Fin p → Bool) (a : α) : List Bool := true :: List.ofFn (enc a)

The stack as a bitstring: one marked block per entry, the top entry first. At p = 0 this is the run of true Cobham.stateWord spells the pending count with.

def stackBits (enc : α → Fin p → Bool) (st : List α) : List Bool := st.flatMap (entryBits enc)

The fold scan's state as a bitstring: the liveness flag, the block slot, then the stack.

def stateWordF (R : RankedAlphabet) (enc : α → Fin p → Bool) (s : FoldScan α) : List Bool := s.live :: bufBits R s.buf ++ stackBits enc s.stack

The number of state bits a step dispatches on: the flag, the slot, and R.maxArity + 1 stack entries.

def dispatchWidthF (R : RankedAlphabet) (p : ℕ) : ℕ := 1 + R.width + (p + 1) * (R.maxArity + 1)

An entry occupies the encoding's width plus its marker.

@[simp] theorem length_entryBits (enc : α → Fin p → Bool) (a : α) : (entryBits enc a).length = p + 1 := α:Type up:ℕenc:α → Fin p → Boola:α⊢ (entryBits enc a).length = p + 1 All goals completed! 🐙

The stack's layout is one entry's width per entry.

theorem length_stackBits (enc : α → Fin p → Bool) : ∀ st : List α, (stackBits enc st).length = (p + 1) * st.length := List.rec rfl fun a t ih ↦ α:Type up:ℕenc:α → Fin p → Boola:αt:List αih:(stackBits enc t).length = (p + 1) * t.length⊢ (stackBits enc (a :: t)).length = (p + 1) * (a :: t).length α:Type up:ℕenc:α → Fin p → Boola:αt:List αih:(stackBits enc t).length = (p + 1) * t.length⊢ p + 1 + (p + 1) * t.length = (p + 1) * t.length + (p + 1) All goals completed! 🐙

The empty stack's layout.

@[simp] theorem stackBits_nil (enc : α → Fin p → Bool) : stackBits enc ([] : List α) = [] := rfl

The stack's layout, one entry at a time.

@[simp] theorem stackBits_cons (enc : α → Fin p → Bool) (a : α) (st : List α) : stackBits enc (a :: st) = entryBits enc a ++ stackBits enc st := rfl

The state word's length: the flag, the slot, and the stack.

theorem length_stateWordF_of_lt (R : RankedAlphabet) (enc : α → Fin p → Bool) (s : FoldScan α) (h : s.buf.length < R.width) : (stateWordF R enc s).length = 1 + R.width + (p + 1) * s.stack.length := α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Bools:FoldScan αh:s.buf.length < R.width⊢ (stateWordF R enc s).length = 1 + R.width + (p + 1) * s.stack.length α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Bools:FoldScan αh:s.buf.length < R.width⊢ R.width + (p + 1) * s.stack.length + 1 = 1 + R.width + (p + 1) * s.stack.length All goals completed! 🐙

The stack's layout truncated to a whole number of entries is the layout of the truncated stack.

theorem take_stackBits (enc : α → Fin p → Bool) : ∀ (st : List α) (m : ℕ), (stackBits enc st).take ((p + 1) * m) = stackBits enc (st.take m) := List.rec (fun _ ↦ α:Type up:ℕenc:α → Fin p → Boolx✝:ℕ⊢ List.take ((p + 1) * x✝) (stackBits enc []) = stackBits enc (List.take x✝ []) All goals completed! 🐙) (fun a t ih m ↦ match m with α:Type up:ℕenc:α → Fin p → Boola:αt:List αih:∀ (m : ℕ), List.take ((p + 1) * m) (stackBits enc t) = stackBits enc (List.take m t)m:ℕ⊢ List.take ((p + 1) * 0) (stackBits enc (a :: t)) = stackBits enc (List.take 0 (a :: t)) α:Type up:ℕenc:α → Fin p → Boola:αt:List αih:∀ (m : ℕ), List.take ((p + 1) * m) (stackBits enc t) = stackBits enc (List.take m t)m:ℕ⊢ List.take ((p + 1) * 0) (stackBits enc (a :: t)) = stackBits enc (List.take 0 (a :: t)) All goals completed! 🐙 α:Type up:ℕenc:α → Fin p → Boola:αt:List αih:∀ (m : ℕ), List.take ((p + 1) * m) (stackBits enc t) = stackBits enc (List.take m t)m:ℕk:ℕ⊢ List.take ((p + 1) * (k + 1)) (stackBits enc (a :: t)) = stackBits enc (List.take (k + 1) (a :: t)) α:Type up:ℕenc:α → Fin p → Boola:αt:List αih:∀ (m : ℕ), List.take ((p + 1) * m) (stackBits enc t) = stackBits enc (List.take m t)m:ℕk:ℕ⊢ List.take ((p + 1) * (k + 1)) (stackBits enc (a :: t)) = stackBits enc (List.take (k + 1) (a :: t)) α:Type up:ℕenc:α → Fin p → Boola:αt:List αih:∀ (m : ℕ), List.take ((p + 1) * m) (stackBits enc t) = stackBits enc (List.take m t)m:ℕk:ℕhlen:(p + 1) * (k + 1) = (entryBits enc a).length + (p + 1) * k⊢ List.take ((p + 1) * (k + 1)) (stackBits enc (a :: t)) = stackBits enc (List.take (k + 1) (a :: t)) All goals completed! 🐙)

The stack's layout advanced past its first entry is the layout of the rest.

theorem drop_stackBits (enc : α → Fin p → Bool) (a : α) (st : List α) : (stackBits enc (a :: st)).drop (p + 1) = stackBits enc st := α:Type up:ℕenc:α → Fin p → Boola:αst:List α⊢ List.drop (p + 1) (stackBits enc (a :: st)) = stackBits enc st α:Type up:ℕenc:α → Fin p → Boola:αst:List α⊢ List.drop (p + 1) (entryBits enc a ++ stackBits enc st) = stackBits enc st All goals completed! 🐙

The stack's layout advanced past a whole number of entries is the layout of the stack advanced by that many.

theorem drop_stackBits_mul (enc : α → Fin p → Bool) : ∀ (n : ℕ) (st : List α), (stackBits enc st).drop ((p + 1) * n) = stackBits enc (st.drop n) := Nat.rec (fun st ↦ α:Type up:ℕenc:α → Fin p → Boolst:List α⊢ List.drop ((p + 1) * Nat.zero) (stackBits enc st) = stackBits enc (List.drop Nat.zero st) All goals completed! 🐙) (fun k ih st ↦ match st with α:Type up:ℕenc:α → Fin p → Boolk:ℕih:∀ (st : List α), List.drop ((p + 1) * k) (stackBits enc st) = stackBits enc (List.drop k st)st:List α⊢ List.drop ((p + 1) * k.succ) (stackBits enc []) = stackBits enc (List.drop k.succ []) α:Type up:ℕenc:α → Fin p → Boolk:ℕih:∀ (st : List α), List.drop ((p + 1) * k) (stackBits enc st) = stackBits enc (List.drop k st)st:List α⊢ List.drop ((p + 1) * k.succ) (stackBits enc []) = stackBits enc (List.drop k.succ []) All goals completed! 🐙 α:Type up:ℕenc:α → Fin p → Boolk:ℕih:∀ (st : List α), List.drop ((p + 1) * k) (stackBits enc st) = stackBits enc (List.drop k st)st:List αa:αt:List α⊢ List.drop ((p + 1) * k.succ) (stackBits enc (a :: t)) = stackBits enc (List.drop k.succ (a :: t)) α:Type up:ℕenc:α → Fin p → Boolk:ℕih:∀ (st : List α), List.drop ((p + 1) * k) (stackBits enc st) = stackBits enc (List.drop k st)st:List αa:αt:List α⊢ List.drop ((p + 1) * k.succ) (stackBits enc (a :: t)) = stackBits enc (List.drop k.succ (a :: t)) α:Type up:ℕenc:α → Fin p → Boolk:ℕih:∀ (st : List α), List.drop ((p + 1) * k) (stackBits enc st) = stackBits enc (List.drop k st)st:List αa:αt:List αhmul:(p + 1) * (k + 1) = p + 1 + (p + 1) * k⊢ List.drop ((p + 1) * k.succ) (stackBits enc (a :: t)) = stackBits enc (List.drop k.succ (a :: t)) All goals completed! 🐙)

The bits of a spelled-out family followed by anything are that family: the window reads only the family's own width.

theorem bits_ofFn_append (f : Fin p → Bool) (l : List Bool) : bits p (List.ofFn f ++ l) = f := p:ℕf:Fin p → Booll:List Bool⊢ bits p (List.ofFn f ++ l) = f p:ℕf:Fin p → Booll:List Boolj:Fin p⊢ bits p (List.ofFn f ++ l) j = f j p:ℕf:Fin p → Booll:List Boolj:Fin phj:↑j < (List.ofFn f).length⊢ bits p (List.ofFn f ++ l) j = f j p:ℕf:Fin p → Booll:List Boolj:Fin phj:↑j < (List.ofFn f).length⊢ (some (f ⟨↑j, ⋯⟩)).getD false = f j All goals completed! 🐙

The state word truncated to a window of whole entries past the slot, and zero-padded: the flag, the slot, the stack truncated at the window, and padding where the stack is shorter. Stated at an arbitrary window, the dispatch and the verdict reading different ones.

theorem ofFn_bits_stateWordF (R : RankedAlphabet) (enc : α → Fin p → Bool) (s : FoldScan α) (n m : ℕ) (hn : n = 1 + R.width + (p + 1) * m) (h : s.buf.length < R.width) : List.ofFn (bits n (stateWordF R enc s)) = s.live :: (bufBits R s.buf ++ (stackBits enc (s.stack.take m) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false)) := α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Bools:FoldScan αn:ℕm:ℕhn:n = 1 + R.width + (p + 1) * mh:s.buf.length < R.width⊢ List.ofFn (bits n (stateWordF R enc s)) = s.live :: (bufBits R s.buf ++ (stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false)) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Bools:FoldScan αm:ℕh:s.buf.length < R.width⊢ List.ofFn (bits (1 + R.width + (p + 1) * m) (stateWordF R enc s)) = s.live :: (bufBits R s.buf ++ (stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false)) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Bools:FoldScan αm:ℕh:s.buf.length < R.widthhbuf:(bufBits R s.buf).length = R.width⊢ List.ofFn (bits (1 + R.width + (p + 1) * m) (stateWordF R enc s)) = s.live :: (bufBits R s.buf ++ (stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false)) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Bools:FoldScan αm:ℕh:s.buf.length < R.widthhbuf:(bufBits R s.buf).length = R.widthhdw:1 + R.width + (p + 1) * m = (bufBits R s.buf).length + (p + 1) * m + 1⊢ List.ofFn (bits (1 + R.width + (p + 1) * m) (stateWordF R enc s)) = s.live :: (bufBits R s.buf ++ (stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false)) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Bools:FoldScan αm:ℕh:s.buf.length < R.widthhbuf:(bufBits R s.buf).length = R.widthhdw:1 + R.width + (p + 1) * m = (bufBits R s.buf).length + (p + 1) * m + 1hpad:1 + R.width + (p + 1) * m - (stateWordF R enc s).length = (p + 1) * m - (p + 1) * s.stack.length⊢ List.ofFn (bits (1 + R.width + (p + 1) * m) (stateWordF R enc s)) = s.live :: (bufBits R s.buf ++ (stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false)) All goals completed! 🐙

The validity scan of a word of leaves has one pending subterm per leaf. At the two-symbol alphabet a block is one bit and false spells the nullary symbol, so nothing is ever popped.

private theorem scanFinal_replicate_false : ∀ k : ℕ, Binary.binRanked.scanFinal (List.replicate k false) = ⟨[], k, true⟩ := Nat.rec (motive := fun k ↦ Binary.binRanked.scanFinal (List.replicate k false) = ⟨[], k, true⟩) rfl fun k ih ↦ k:ℕih:Binary.binRanked.scanFinal (List.replicate k false) = { buf := [], depth := k, live := true }⊢ Binary.binRanked.scanFinal (List.replicate k.succ false) = { buf := [], depth := k.succ, live := true } All goals completed! 🐙

At the two-symbol alphabet, whose width is one, the additive bound Cobham.scan admits fails of this layout at every positive carrier width, so the multiplicative bound Geb.CobhamFold.scanMul carries is not a convenience. A word of k leaves leaves k entries on the stack, giving a state of 2 + (q + 1) * k bits against an input of k; no fixed growth dominates that. The failure needs R.width < q + 1, and needs an alphabet whose symbols grow the stack: at R.width ≥ q + 1 the additive bound always suffices, and an alphabet with no nullary symbol keeps the stack empty whatever the carrier.

theorem length_stateWordF_not_le_add {β : Type u} {q : ℕ} (hq : 0 < q) (enc : β → Fin q → Bool) (alg : (i : Fin Binary.binRanked.card) → (Fin (Binary.binRanked.arity i) → β) → β) (growth : ℕ) : ∃ w : List Bool, w.length + growth < (stateWordF Binary.binRanked enc (foldScanFinal Binary.binRanked alg w)).length := β:Type uq:ℕhq:0 < qenc:β → Fin q → Boolalg:(i : Fin Binary.binRanked.card) → (Fin (Binary.binRanked.arity i) → β) → βgrowth:ℕ⊢ ∃ w, w.length + growth < (stateWordF Binary.binRanked enc (foldScanFinal Binary.binRanked alg w)).length β:Type uq:ℕhq:0 < qenc:β → Fin q → Boolalg:(i : Fin Binary.binRanked.card) → (Fin (Binary.binRanked.arity i) → β) → βgrowth:ℕ⊢ (List.replicate growth false).length + growth < (stateWordF Binary.binRanked enc (foldScanFinal Binary.binRanked alg (List.replicate growth false))).length β:Type uq:ℕhq:0 < qenc:β → Fin q → Boolalg:(i : Fin Binary.binRanked.card) → (Fin (Binary.binRanked.arity i) → β) → βgrowth:ℕhproj:toScan (foldScanFinal Binary.binRanked alg (List.replicate growth false)) = Binary.binRanked.scanFinal (List.replicate growth false)⊢ (List.replicate growth false).length + growth < (stateWordF Binary.binRanked enc (foldScanFinal Binary.binRanked alg (List.replicate growth false))).length β:Type uq:ℕhq:0 < qenc:β → Fin q → Boolalg:(i : Fin Binary.binRanked.card) → (Fin (Binary.binRanked.arity i) → β) → βgrowth:ℕhproj:toScan (foldScanFinal Binary.binRanked alg (List.replicate growth false)) = { buf := [], depth := growth, live := true }⊢ (List.replicate growth false).length + growth < (stateWordF Binary.binRanked enc (foldScanFinal Binary.binRanked alg (List.replicate growth false))).length β:Type uq:ℕhq:0 < qenc:β → Fin q → Boolalg:(i : Fin Binary.binRanked.card) → (Fin (Binary.binRanked.arity i) → β) → βgrowth:ℕhproj:toScan (foldScanFinal Binary.binRanked alg (List.replicate growth false)) = { buf := [], depth := growth, live := true }hbuf:(foldScanFinal Binary.binRanked alg (List.replicate growth false)).buf = []⊢ (List.replicate growth false).length + growth < (stateWordF Binary.binRanked enc (foldScanFinal Binary.binRanked alg (List.replicate growth false))).length β:Type uq:ℕhq:0 < qenc:β → Fin q → Boolalg:(i : Fin Binary.binRanked.card) → (Fin (Binary.binRanked.arity i) → β) → βgrowth:ℕhproj:toScan (foldScanFinal Binary.binRanked alg (List.replicate growth false)) = { buf := [], depth := growth, live := true }hbuf:(foldScanFinal Binary.binRanked alg (List.replicate growth false)).buf = []hstack:(foldScanFinal Binary.binRanked alg (List.replicate growth false)).stack.length = growth⊢ (List.replicate growth false).length + growth < (stateWordF Binary.binRanked enc (foldScanFinal Binary.binRanked alg (List.replicate growth false))).length β:Type uq:ℕhq:0 < qenc:β → Fin q → Boolalg:(i : Fin Binary.binRanked.card) → (Fin (Binary.binRanked.arity i) → β) → βgrowth:ℕhproj:toScan (foldScanFinal Binary.binRanked alg (List.replicate growth false)) = { buf := [], depth := growth, live := true }hbuf:(foldScanFinal Binary.binRanked alg (List.replicate growth false)).buf = []hstack:(foldScanFinal Binary.binRanked alg (List.replicate growth false)).stack.length = growth⊢ growth + growth < 1 + Binary.binRanked.width + (q + 1) * growth β:Type uq:ℕhq:0 < qenc:β → Fin q → Boolalg:(i : Fin Binary.binRanked.card) → (Fin (Binary.binRanked.arity i) → β) → βgrowth:ℕhproj:toScan (foldScanFinal Binary.binRanked alg (List.replicate growth false)) = { buf := [], depth := growth, live := true }hbuf:(foldScanFinal Binary.binRanked alg (List.replicate growth false)).buf = []hstack:(foldScanFinal Binary.binRanked alg (List.replicate growth false)).stack.length = growthhw:Binary.binRanked.width = 1⊢ growth + growth < 1 + Binary.binRanked.width + (q + 1) * growth β:Type uq:ℕhq:0 < qenc:β → Fin q → Boolalg:(i : Fin Binary.binRanked.card) → (Fin (Binary.binRanked.arity i) → β) → βgrowth:ℕhproj:toScan (foldScanFinal Binary.binRanked alg (List.replicate growth false)) = { buf := [], depth := growth, live := true }hbuf:(foldScanFinal Binary.binRanked alg (List.replicate growth false)).buf = []hstack:(foldScanFinal Binary.binRanked alg (List.replicate growth false)).stack.length = growthhw:Binary.binRanked.width = 1⊢ growth + growth < 1 + 1 + (q * growth + growth) β:Type uq:ℕhq:0 < qenc:β → Fin q → Boolalg:(i : Fin Binary.binRanked.card) → (Fin (Binary.binRanked.arity i) → β) → βgrowth:ℕhproj:toScan (foldScanFinal Binary.binRanked alg (List.replicate growth false)) = { buf := [], depth := growth, live := true }hbuf:(foldScanFinal Binary.binRanked alg (List.replicate growth false)).buf = []hstack:(foldScanFinal Binary.binRanked alg (List.replicate growth false)).stack.length = growthhw:Binary.binRanked.width = 1hle:1 * growth ≤ q * growth⊢ growth + growth < 1 + 1 + (q * growth + growth) β:Type uq:ℕhq:0 < qenc:β → Fin q → Boolalg:(i : Fin Binary.binRanked.card) → (Fin (Binary.binRanked.arity i) → β) → βgrowth:ℕhproj:toScan (foldScanFinal Binary.binRanked alg (List.replicate growth false)) = { buf := [], depth := growth, live := true }hbuf:(foldScanFinal Binary.binRanked alg (List.replicate growth false)).buf = []hstack:(foldScanFinal Binary.binRanked alg (List.replicate growth false)).stack.length = growthhw:Binary.binRanked.width = 1hle:growth ≤ q * growth⊢ growth + growth < 1 + 1 + (q * growth + growth) All goals completed! 🐙

The inverse of the stack's layout, read off a bitstring with a fuel bound: each marked block contributes its decoded value, and the first unmarked block ends the stack.

def decodeStack (dec : (Fin p → Bool) → α) : ℕ → List Bool → List α := Nat.rec (motive := fun _ ↦ List Bool → List α) (fun _ ↦ []) fun _ ih l ↦ match l with | true :: rest => dec (bits p rest) :: ih (rest.drop p) | _ => []

The decoder at no fuel reads no entry.

@[simp] theorem decodeStack_zero (dec : (Fin p → Bool) → α) (l : List Bool) : decodeStack dec 0 l = [] := rfl

The decoder's computation rule at a marked block.

theorem decodeStack_succ_true (dec : (Fin p → Bool) → α) (k : ℕ) (rest : List Bool) : decodeStack dec (k + 1) (true :: rest) = dec (bits p rest) :: decodeStack dec k (rest.drop p) := rfl

The decoder inverts the stack's layout, up to truncating at the fuel. The retraction hypothesis is what identifies each decoded block with the value that spelled it; the trailing false padding stops the recursion.

theorem decodeStack_stackBits_append (dec : (Fin p → Bool) → α) (enc : α → Fin p → Bool) (hdec : ∀ a, dec (enc a) = a) : ∀ (k : ℕ) (st : List α) (j : ℕ), decodeStack dec k (stackBits enc st ++ List.replicate j false) = st.take k := Nat.rec (fun st _ ↦ α:Type up:ℕdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = ast:List αx✝:ℕ⊢ decodeStack dec Nat.zero (stackBits enc st ++ List.replicate x✝ false) = List.take Nat.zero st All goals completed! 🐙) (fun k ih st j ↦ match st with α:Type up:ℕdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = ak:ℕih:∀ (st : List α) (j : ℕ), decodeStack dec k (stackBits enc st ++ List.replicate j false) = List.take k stst:List αj:ℕ⊢ decodeStack dec k.succ (stackBits enc [] ++ List.replicate j false) = List.take k.succ [] α:Type up:ℕdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = ak:ℕih:∀ (st : List α) (j : ℕ), decodeStack dec k (stackBits enc st ++ List.replicate j false) = List.take k stst:List αj:ℕ⊢ decodeStack dec k.succ (stackBits enc [] ++ List.replicate j false) = List.take k.succ [] match j with α:Type up:ℕdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = ak:ℕih:∀ (st : List α) (j : ℕ), decodeStack dec k (stackBits enc st ++ List.replicate j false) = List.take k stst:List αj:ℕ⊢ decodeStack dec k.succ (stackBits enc [] ++ List.replicate 0 false) = List.take k.succ [] All goals completed! 🐙 α:Type up:ℕdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = ak:ℕih:∀ (st : List α) (j : ℕ), decodeStack dec k (stackBits enc st ++ List.replicate j false) = List.take k stst:List αj:ℕn✝:ℕ⊢ decodeStack dec k.succ (stackBits enc [] ++ List.replicate (n✝ + 1) false) = List.take k.succ [] All goals completed! 🐙 α:Type up:ℕdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = ak:ℕih:∀ (st : List α) (j : ℕ), decodeStack dec k (stackBits enc st ++ List.replicate j false) = List.take k stst:List αj:ℕa:αt:List α⊢ decodeStack dec k.succ (stackBits enc (a :: t) ++ List.replicate j false) = List.take k.succ (a :: t) α:Type up:ℕdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = ak:ℕih:∀ (st : List α) (j : ℕ), decodeStack dec k (stackBits enc st ++ List.replicate j false) = List.take k stst:List αj:ℕa:αt:List α⊢ decodeStack dec k.succ (stackBits enc (a :: t) ++ List.replicate j false) = List.take k.succ (a :: t) α:Type up:ℕdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = ak:ℕih:∀ (st : List α) (j : ℕ), decodeStack dec k (stackBits enc st ++ List.replicate j false) = List.take k stst:List αj:ℕa:αt:List α⊢ decodeStack dec k.succ (true :: List.ofFn (enc a) ++ stackBits enc t ++ List.replicate j false) = List.take k.succ (a :: t) α:Type up:ℕdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = ak:ℕih:∀ (st : List α) (j : ℕ), decodeStack dec k (stackBits enc st ++ List.replicate j false) = List.take k stst:List αj:ℕa:αt:List α⊢ decodeStack dec k.succ (true :: (List.ofFn (enc a) ++ (stackBits enc t ++ List.replicate j false))) = List.take k.succ (a :: t) All goals completed! 🐙)

The inverse of the state layout at a window of n bits reading m stack entries: the flag is the head, the block is the slot past its padding and sentinel, and the stack is decoded from what follows the slot. Stated at an arbitrary window, the dispatch and the readout reading different ones.

def decodeStateAt (R : RankedAlphabet) (p : ℕ) (dec : (Fin p → Bool) → α) (n m : ℕ) (v : Fin n → Bool) : FoldScan α := ⟨(((List.ofFn v).tail.take R.width).dropWhile (fun b ↦ !b)).tail, decodeStack dec m ((List.ofFn v).tail.drop R.width), (List.ofFn v).headD false⟩

The decoder inverts the layout, up to truncating the stack at the window.

theorem decodeStateAt_stateWordF_of_lt (R : RankedAlphabet) (dec : (Fin p → Bool) → α) (enc : α → Fin p → Bool) (hdec : ∀ a, dec (enc a) = a) (s : FoldScan α) (n m : ℕ) (hn : n = 1 + R.width + (p + 1) * m) (h : s.buf.length < R.width) : decodeStateAt R p dec n m (bits n (stateWordF R enc s)) = { s with stack := s.stack.take m } := α:Type up:ℕR:RankedAlphabetdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = as:FoldScan αn:ℕm:ℕhn:n = 1 + R.width + (p + 1) * mh:s.buf.length < R.width⊢ decodeStateAt R p dec n m (bits n (stateWordF R enc s)) = { buf := s.buf, stack := List.take m s.stack, live := s.live } α:Type up:ℕR:RankedAlphabetdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = as:FoldScan αn:ℕm:ℕhn:n = 1 + R.width + (p + 1) * mh:s.buf.length < R.widthhbuf:(bufBits R s.buf).length = R.width⊢ decodeStateAt R p dec n m (bits n (stateWordF R enc s)) = { buf := s.buf, stack := List.take m s.stack, live := s.live } α:Type up:ℕR:RankedAlphabetdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = as:FoldScan αn:ℕm:ℕhn:n = 1 + R.width + (p + 1) * mh:s.buf.length < R.widthhbuf:(bufBits R s.buf).length = R.widthhword:List.ofFn (bits n (stateWordF R enc s)) = s.live :: (bufBits R s.buf ++ (stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false))⊢ decodeStateAt R p dec n m (bits n (stateWordF R enc s)) = { buf := s.buf, stack := List.take m s.stack, live := s.live } α:Type up:ℕR:RankedAlphabetdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = as:FoldScan αn:ℕm:ℕhn:n = 1 + R.width + (p + 1) * mh:s.buf.length < R.widthhbuf:(bufBits R s.buf).length = R.widthhword:List.ofFn (bits n (stateWordF R enc s)) = s.live :: (bufBits R s.buf ++ (stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false))hslot:List.take R.width (List.ofFn (bits n (stateWordF R enc s))).tail = bufBits R s.buf⊢ decodeStateAt R p dec n m (bits n (stateWordF R enc s)) = { buf := s.buf, stack := List.take m s.stack, live := s.live } α:Type up:ℕR:RankedAlphabetdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = as:FoldScan αn:ℕm:ℕhn:n = 1 + R.width + (p + 1) * mh:s.buf.length < R.widthhbuf:(bufBits R s.buf).length = R.widthhword:List.ofFn (bits n (stateWordF R enc s)) = s.live :: (bufBits R s.buf ++ (stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false))hslot:List.take R.width (List.ofFn (bits n (stateWordF R enc s))).tail = bufBits R s.bufhtail:List.drop R.width (List.ofFn (bits n (stateWordF R enc s))).tail = stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false⊢ decodeStateAt R p dec n m (bits n (stateWordF R enc s)) = { buf := s.buf, stack := List.take m s.stack, live := s.live } α:Type up:ℕR:RankedAlphabetdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = as:FoldScan αn:ℕm:ℕhn:n = 1 + R.width + (p + 1) * mh:s.buf.length < R.widthhbuf:(bufBits R s.buf).length = R.widthhword:List.ofFn (bits n (stateWordF R enc s)) = s.live :: (bufBits R s.buf ++ (stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false))hslot:List.take R.width (List.ofFn (bits n (stateWordF R enc s))).tail = bufBits R s.bufhtail:List.drop R.width (List.ofFn (bits n (stateWordF R enc s))).tail = stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false⊢ (decodeStateAt R p dec n m (bits n (stateWordF R enc s))).buf = { buf := s.buf, stack := List.take m s.stack, live := s.live }.bufα:Type up:ℕR:RankedAlphabetdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = as:FoldScan αn:ℕm:ℕhn:n = 1 + R.width + (p + 1) * mh:s.buf.length < R.widthhbuf:(bufBits R s.buf).length = R.widthhword:List.ofFn (bits n (stateWordF R enc s)) = s.live :: (bufBits R s.buf ++ (stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false))hslot:List.take R.width (List.ofFn (bits n (stateWordF R enc s))).tail = bufBits R s.bufhtail:List.drop R.width (List.ofFn (bits n (stateWordF R enc s))).tail = stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false⊢ (decodeStateAt R p dec n m (bits n (stateWordF R enc s))).stack = { buf := s.buf, stack := List.take m s.stack, live := s.live }.stackα:Type up:ℕR:RankedAlphabetdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = as:FoldScan αn:ℕm:ℕhn:n = 1 + R.width + (p + 1) * mh:s.buf.length < R.widthhbuf:(bufBits R s.buf).length = R.widthhword:List.ofFn (bits n (stateWordF R enc s)) = s.live :: (bufBits R s.buf ++ (stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false))hslot:List.take R.width (List.ofFn (bits n (stateWordF R enc s))).tail = bufBits R s.bufhtail:List.drop R.width (List.ofFn (bits n (stateWordF R enc s))).tail = stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false⊢ (decodeStateAt R p dec n m (bits n (stateWordF R enc s))).live = { buf := s.buf, stack := List.take m s.stack, live := s.live }.live α:Type up:ℕR:RankedAlphabetdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = as:FoldScan αn:ℕm:ℕhn:n = 1 + R.width + (p + 1) * mh:s.buf.length < R.widthhbuf:(bufBits R s.buf).length = R.widthhword:List.ofFn (bits n (stateWordF R enc s)) = s.live :: (bufBits R s.buf ++ (stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false))hslot:List.take R.width (List.ofFn (bits n (stateWordF R enc s))).tail = bufBits R s.bufhtail:List.drop R.width (List.ofFn (bits n (stateWordF R enc s))).tail = stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false⊢ (decodeStateAt R p dec n m (bits n (stateWordF R enc s))).buf = { buf := s.buf, stack := List.take m s.stack, live := s.live }.buf α:Type up:ℕR:RankedAlphabetdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = as:FoldScan αn:ℕm:ℕhn:n = 1 + R.width + (p + 1) * mh:s.buf.length < R.widthhbuf:(bufBits R s.buf).length = R.widthhword:List.ofFn (bits n (stateWordF R enc s)) = s.live :: (bufBits R s.buf ++ (stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false))hslot:List.take R.width (List.ofFn (bits n (stateWordF R enc s))).tail = bufBits R s.bufhtail:List.drop R.width (List.ofFn (bits n (stateWordF R enc s))).tail = stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false⊢ { buf := (true :: s.buf).tail, stack := decodeStack dec m (List.drop R.width (List.ofFn (bits n (stateWordF R enc s))).tail), live := (List.ofFn (bits n (stateWordF R enc s))).headD false }.buf = { buf := s.buf, stack := List.take m s.stack, live := s.live }.buf All goals completed! 🐙 α:Type up:ℕR:RankedAlphabetdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = as:FoldScan αn:ℕm:ℕhn:n = 1 + R.width + (p + 1) * mh:s.buf.length < R.widthhbuf:(bufBits R s.buf).length = R.widthhword:List.ofFn (bits n (stateWordF R enc s)) = s.live :: (bufBits R s.buf ++ (stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false))hslot:List.take R.width (List.ofFn (bits n (stateWordF R enc s))).tail = bufBits R s.bufhtail:List.drop R.width (List.ofFn (bits n (stateWordF R enc s))).tail = stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false⊢ (decodeStateAt R p dec n m (bits n (stateWordF R enc s))).stack = { buf := s.buf, stack := List.take m s.stack, live := s.live }.stack All goals completed! 🐙 α:Type up:ℕR:RankedAlphabetdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = as:FoldScan αn:ℕm:ℕhn:n = 1 + R.width + (p + 1) * mh:s.buf.length < R.widthhbuf:(bufBits R s.buf).length = R.widthhword:List.ofFn (bits n (stateWordF R enc s)) = s.live :: (bufBits R s.buf ++ (stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false))hslot:List.take R.width (List.ofFn (bits n (stateWordF R enc s))).tail = bufBits R s.bufhtail:List.drop R.width (List.ofFn (bits n (stateWordF R enc s))).tail = stackBits enc (List.take m s.stack) ++ List.replicate ((p + 1) * m - (p + 1) * s.stack.length) false⊢ (decodeStateAt R p dec n m (bits n (stateWordF R enc s))).live = { buf := s.buf, stack := List.take m s.stack, live := s.live }.live All goals completed! 🐙

The decoder at the dispatch window.

def decodeStateF (R : RankedAlphabet) (p : ℕ) (dec : (Fin p → Bool) → α) (v : Fin (dispatchWidthF R p) → Bool) : FoldScan α := decodeStateAt R p dec (dispatchWidthF R p) (R.maxArity + 1) v

The decoder inverts the layout, up to truncating the stack at the dispatch window R.maxArity + 1.

theorem decodeStateF_stateWordF_of_lt (R : RankedAlphabet) (dec : (Fin p → Bool) → α) (enc : α → Fin p → Bool) (hdec : ∀ a, dec (enc a) = a) (s : FoldScan α) (h : s.buf.length < R.width) : decodeStateF R p dec (bits (dispatchWidthF R p) (stateWordF R enc s)) = { s with stack := s.stack.take (R.maxArity + 1) } := decodeStateAt_stateWordF_of_lt R dec enc hdec s (dispatchWidthF R p) (R.maxArity + 1) (α:Type up:ℕR:RankedAlphabetdec:(Fin p → Bool) → αenc:α → Fin p → Boolhdec:∀ (a : α), dec (enc a) = as:FoldScan αh:s.buf.length < R.width⊢ dispatchWidthF R p = 1 + R.width + (p + 1) * (R.maxArity + 1) All goals completed! 🐙) h

The bits a step drops from the state word: the flag and the slot, together with the entries the symbol of a completed block pops.

def dropCountF (R : RankedAlphabet) (p : ℕ) (b : Bool) (s : FoldScan α) : ℕ := match s.live with | false => 1 + R.width | true => if (b :: s.buf).length = R.width then match symOf R (decodeBits (b :: s.buf)) with | none => 1 + R.width | some i => if R.arity i ≤ s.stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width

The bits a step prepends to the state word: the rebuilt flag and slot, together with the entry the symbol of a completed block pushes.

def nextPrefixF (R : RankedAlphabet) (enc : α → Fin p → Bool) (alg : (i : Fin R.card) → (Fin (R.arity i) → α) → α) (b : Bool) (s : FoldScan α) : List Bool := match s.live with | false => false :: bufBits R s.buf | true => if (b :: s.buf).length = R.width then match symOf R (decodeBits (b :: s.buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ s.stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ s.stack[d.val]'(Nat.lt_of_lt_of_le d.isLt h)) else false :: bufBits R [] else true :: bufBits R (b :: s.buf)

Truncating the stack at the dispatch window leaves the bits dropped unchanged: the only test reading the stack's height compares it with an arity, which RankedAlphabet.arity_le_maxArity bounds by R.maxArity.

theorem dropCountF_take_stack (R : RankedAlphabet) (p : ℕ) (b : Bool) (s : FoldScan α) : dropCountF R p b { s with stack := s.stack.take (R.maxArity + 1) } = dropCountF R p b s := α:Type uR:RankedAlphabetp:ℕb:Bools:FoldScan α⊢ dropCountF R p b { buf := s.buf, stack := List.take (R.maxArity + 1) s.stack, live := s.live } = dropCountF R p b s α:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List αlive:Bool⊢ dropCountF R p b { buf := { buf := buf, stack := stack, live := live }.buf, stack := List.take (R.maxArity + 1) { buf := buf, stack := stack, live := live }.stack, live := { buf := buf, stack := stack, live := live }.live } = dropCountF R p b { buf := buf, stack := stack, live := live } α:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List αlive:Bool⊢ (match { buf := { buf := buf, stack := stack, live := live }.buf, stack := List.take (R.maxArity + 1) { buf := buf, stack := stack, live := live }.stack, live := { buf := buf, stack := stack, live := live }.live }.live with | false => 1 + R.width | true => if (b :: { buf := { buf := buf, stack := stack, live := live }.buf, stack := List.take (R.maxArity + 1) { buf := buf, stack := stack, live := live }.stack, live := { buf := buf, stack := stack, live := live }.live }.buf).length = R.width then match symOf R (decodeBits (b :: { buf := { buf := buf, stack := stack, live := live }.buf, stack := List.take (R.maxArity + 1) { buf := buf, stack := stack, live := live }.stack, live := { buf := buf, stack := stack, live := live }.live }.buf)) with | none => 1 + R.width | some i => if R.arity i ≤ { buf := { buf := buf, stack := stack, live := live }.buf, stack := List.take (R.maxArity + 1) { buf := buf, stack := stack, live := live }.stack, live := { buf := buf, stack := stack, live := live }.live }.stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) = match { buf := buf, stack := stack, live := live }.live with | false => 1 + R.width | true => if (b :: { buf := buf, stack := stack, live := live }.buf).length = R.width then match symOf R (decodeBits (b :: { buf := buf, stack := stack, live := live }.buf)) with | none => 1 + R.width | some i => if R.arity i ≤ { buf := buf, stack := stack, live := live }.stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width α:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List αlive:Bool⊢ (match live with | false => 1 + R.width | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ (List.take (R.maxArity + 1) stack).length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) = match live with | false => 1 + R.width | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width α:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List α⊢ (match false with | false => 1 + R.width | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ (List.take (R.maxArity + 1) stack).length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) = match false with | false => 1 + R.width | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.widthα:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List α⊢ (match true with | false => 1 + R.width | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ (List.take (R.maxArity + 1) stack).length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) = match true with | false => 1 + R.width | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width α:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List α⊢ (match false with | false => 1 + R.width | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ (List.take (R.maxArity + 1) stack).length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) = match false with | false => 1 + R.width | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width All goals completed! 🐙 α:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List α⊢ (match true with | false => 1 + R.width | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ (List.take (R.maxArity + 1) stack).length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) = match true with | false => 1 + R.width | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width α:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List α⊢ (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ (List.take (R.maxArity + 1) stack).length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) = if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width α:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.width⊢ (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ (List.take (R.maxArity + 1) stack).length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) = if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.widthα:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List αhlen:¬(b :: buf).length = R.width⊢ (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ (List.take (R.maxArity + 1) stack).length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) = if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width α:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.width⊢ (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ (List.take (R.maxArity + 1) stack).length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) = if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width α:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.width⊢ (match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ (List.take (R.maxArity + 1) stack).length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width) = match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width match hsym : symOf R (decodeBits (b :: buf)) with α:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.widthhsym:symOf R (decodeBits (b :: buf)) = none⊢ (match none with | none => 1 + R.width | some i => if R.arity i ≤ (List.take (R.maxArity + 1) stack).length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width) = match none with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width All goals completed! 🐙 α:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some i⊢ (match some i with | none => 1 + R.width | some i => if R.arity i ≤ (List.take (R.maxArity + 1) stack).length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width) = match some i with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width α:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some i⊢ (if R.arity i ≤ (List.take (R.maxArity + 1) stack).length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width) = if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width α:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:R.arity i ≤ R.maxArity⊢ (if R.arity i ≤ (List.take (R.maxArity + 1) stack).length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width) = if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width α:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:R.arity i ≤ R.maxArityhmin:(List.take (R.maxArity + 1) stack).length = min (R.maxArity + 1) stack.length⊢ (if R.arity i ≤ (List.take (R.maxArity + 1) stack).length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width) = if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width α:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:R.arity i ≤ R.maxArityhmin:(List.take (R.maxArity + 1) stack).length = min (R.maxArity + 1) stack.lengthhst:R.arity i ≤ stack.length⊢ (if R.arity i ≤ (List.take (R.maxArity + 1) stack).length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width) = if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.widthα:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:R.arity i ≤ R.maxArityhmin:(List.take (R.maxArity + 1) stack).length = min (R.maxArity + 1) stack.lengthhst:¬R.arity i ≤ stack.length⊢ (if R.arity i ≤ (List.take (R.maxArity + 1) stack).length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width) = if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width α:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:R.arity i ≤ R.maxArityhmin:(List.take (R.maxArity + 1) stack).length = min (R.maxArity + 1) stack.lengthhst:R.arity i ≤ stack.length⊢ (if R.arity i ≤ (List.take (R.maxArity + 1) stack).length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width) = if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width All goals completed! 🐙 α:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:R.arity i ≤ R.maxArityhmin:(List.take (R.maxArity + 1) stack).length = min (R.maxArity + 1) stack.lengthhst:¬R.arity i ≤ stack.length⊢ (if R.arity i ≤ (List.take (R.maxArity + 1) stack).length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width) = if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width All goals completed! 🐙 α:Type uR:RankedAlphabetp:ℕb:Boolbuf:List Boolstack:List αhlen:¬(b :: buf).length = R.width⊢ (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ (List.take (R.maxArity + 1) stack).length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) = if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width All goals completed! 🐙

Truncating the stack at the dispatch window leaves the bits prepended unchanged: the entries the algebra reads are the first R.arity i, and the window holds R.maxArity + 1 of them.

theorem nextPrefixF_take_stack (R : RankedAlphabet) (enc : α → Fin p → Bool) (alg : (i : Fin R.card) → (Fin (R.arity i) → α) → α) (b : Bool) (s : FoldScan α) : nextPrefixF R enc alg b { s with stack := s.stack.take (R.maxArity + 1) } = nextPrefixF R enc alg b s := α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Bools:FoldScan α⊢ nextPrefixF R enc alg b { buf := s.buf, stack := List.take (R.maxArity + 1) s.stack, live := s.live } = nextPrefixF R enc alg b s α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αlive:Bool⊢ nextPrefixF R enc alg b { buf := { buf := buf, stack := stack, live := live }.buf, stack := List.take (R.maxArity + 1) { buf := buf, stack := stack, live := live }.stack, live := { buf := buf, stack := stack, live := live }.live } = nextPrefixF R enc alg b { buf := buf, stack := stack, live := live } α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αlive:Bool⊢ (match { buf := { buf := buf, stack := stack, live := live }.buf, stack := List.take (R.maxArity + 1) { buf := buf, stack := stack, live := live }.stack, live := { buf := buf, stack := stack, live := live }.live }.live with | false => false :: bufBits R { buf := { buf := buf, stack := stack, live := live }.buf, stack := List.take (R.maxArity + 1) { buf := buf, stack := stack, live := live }.stack, live := { buf := buf, stack := stack, live := live }.live }.buf | true => if (b :: { buf := { buf := buf, stack := stack, live := live }.buf, stack := List.take (R.maxArity + 1) { buf := buf, stack := stack, live := live }.stack, live := { buf := buf, stack := stack, live := live }.live }.buf).length = R.width then match symOf R (decodeBits (b :: { buf := { buf := buf, stack := stack, live := live }.buf, stack := List.take (R.maxArity + 1) { buf := buf, stack := stack, live := live }.stack, live := { buf := buf, stack := stack, live := live }.live }.buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ { buf := { buf := buf, stack := stack, live := live }.buf, stack := List.take (R.maxArity + 1) { buf := buf, stack := stack, live := live }.stack, live := { buf := buf, stack := stack, live := live }.live }.stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ { buf := { buf := buf, stack := stack, live := live }.buf, stack := List.take (R.maxArity + 1) { buf := buf, stack := stack, live := live }.stack, live := { buf := buf, stack := stack, live := live }.live }.stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: { buf := { buf := buf, stack := stack, live := live }.buf, stack := List.take (R.maxArity + 1) { buf := buf, stack := stack, live := live }.stack, live := { buf := buf, stack := stack, live := live }.live }.buf)) = match { buf := buf, stack := stack, live := live }.live with | false => false :: bufBits R { buf := buf, stack := stack, live := live }.buf | true => if (b :: { buf := buf, stack := stack, live := live }.buf).length = R.width then match symOf R (decodeBits (b :: { buf := buf, stack := stack, live := live }.buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ { buf := buf, stack := stack, live := live }.stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ { buf := buf, stack := stack, live := live }.stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: { buf := buf, stack := stack, live := live }.buf) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αlive:Bool⊢ (match live with | false => false :: bufBits R buf | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ (List.take (R.maxArity + 1) stack).length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ (List.take (R.maxArity + 1) stack)[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)) = match live with | false => false :: bufBits R buf | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List α⊢ (match false with | false => false :: bufBits R buf | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ (List.take (R.maxArity + 1) stack).length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ (List.take (R.maxArity + 1) stack)[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)) = match false with | false => false :: bufBits R buf | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List α⊢ (match true with | false => false :: bufBits R buf | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ (List.take (R.maxArity + 1) stack).length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ (List.take (R.maxArity + 1) stack)[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)) = match true with | false => false :: bufBits R buf | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List α⊢ (match false with | false => false :: bufBits R buf | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ (List.take (R.maxArity + 1) stack).length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ (List.take (R.maxArity + 1) stack)[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)) = match false with | false => false :: bufBits R buf | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf) All goals completed! 🐙 α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List α⊢ (match true with | false => false :: bufBits R buf | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ (List.take (R.maxArity + 1) stack).length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ (List.take (R.maxArity + 1) stack)[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)) = match true with | false => false :: bufBits R buf | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List α⊢ (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ (List.take (R.maxArity + 1) stack).length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ (List.take (R.maxArity + 1) stack)[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)) = if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.width⊢ (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ (List.take (R.maxArity + 1) stack).length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ (List.take (R.maxArity + 1) stack)[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)) = if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αhlen:¬(b :: buf).length = R.width⊢ (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ (List.take (R.maxArity + 1) stack).length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ (List.take (R.maxArity + 1) stack)[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)) = if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.width⊢ (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ (List.take (R.maxArity + 1) stack).length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ (List.take (R.maxArity + 1) stack)[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)) = if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.width⊢ (match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ (List.take (R.maxArity + 1) stack).length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ (List.take (R.maxArity + 1) stack)[↑d]) else false :: bufBits R []) = match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] match hsym : symOf R (decodeBits (b :: buf)) with α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.widthhsym:symOf R (decodeBits (b :: buf)) = none⊢ (match none with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ (List.take (R.maxArity + 1) stack).length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ (List.take (R.maxArity + 1) stack)[↑d]) else false :: bufBits R []) = match none with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] All goals completed! 🐙 α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some i⊢ (match some i with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ (List.take (R.maxArity + 1) stack).length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ (List.take (R.maxArity + 1) stack)[↑d]) else false :: bufBits R []) = match some i with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some i⊢ (if h : R.arity i ≤ (List.take (R.maxArity + 1) stack).length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ (List.take (R.maxArity + 1) stack)[↑d]) else false :: bufBits R []) = if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:R.arity i ≤ R.maxArity⊢ (if h : R.arity i ≤ (List.take (R.maxArity + 1) stack).length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ (List.take (R.maxArity + 1) stack)[↑d]) else false :: bufBits R []) = if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:R.arity i ≤ R.maxArityhmin:(List.take (R.maxArity + 1) stack).length = min (R.maxArity + 1) stack.length⊢ (if h : R.arity i ≤ (List.take (R.maxArity + 1) stack).length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ (List.take (R.maxArity + 1) stack)[↑d]) else false :: bufBits R []) = if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:R.arity i ≤ R.maxArityhmin:(List.take (R.maxArity + 1) stack).length = min (R.maxArity + 1) stack.lengthhst:R.arity i ≤ stack.length⊢ (if h : R.arity i ≤ (List.take (R.maxArity + 1) stack).length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ (List.take (R.maxArity + 1) stack)[↑d]) else false :: bufBits R []) = if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R []α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:R.arity i ≤ R.maxArityhmin:(List.take (R.maxArity + 1) stack).length = min (R.maxArity + 1) stack.lengthhst:¬R.arity i ≤ stack.length⊢ (if h : R.arity i ≤ (List.take (R.maxArity + 1) stack).length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ (List.take (R.maxArity + 1) stack)[↑d]) else false :: bufBits R []) = if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:R.arity i ≤ R.maxArityhmin:(List.take (R.maxArity + 1) stack).length = min (R.maxArity + 1) stack.lengthhst:R.arity i ≤ stack.length⊢ (if h : R.arity i ≤ (List.take (R.maxArity + 1) stack).length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ (List.take (R.maxArity + 1) stack)[↑d]) else false :: bufBits R []) = if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:R.arity i ≤ R.maxArityhmin:(List.take (R.maxArity + 1) stack).length = min (R.maxArity + 1) stack.lengthhst:R.arity i ≤ stack.length⊢ true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ (List.take (R.maxArity + 1) stack)[↑d]) = true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:R.arity i ≤ R.maxArityhmin:(List.take (R.maxArity + 1) stack).length = min (R.maxArity + 1) stack.lengthhst:R.arity i ≤ stack.lengthd:Fin (R.arity i)⊢ (List.take (R.maxArity + 1) stack)[↑d] = stack[↑d] All goals completed! 🐙 α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αhlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:R.arity i ≤ R.maxArityhmin:(List.take (R.maxArity + 1) stack).length = min (R.maxArity + 1) stack.lengthhst:¬R.arity i ≤ stack.length⊢ (if h : R.arity i ≤ (List.take (R.maxArity + 1) stack).length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ (List.take (R.maxArity + 1) stack)[↑d]) else false :: bufBits R []) = if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] All goals completed! 🐙 α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αhlen:¬(b :: buf).length = R.width⊢ (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ (List.take (R.maxArity + 1) stack).length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ (List.take (R.maxArity + 1) stack)[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)) = if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf) All goals completed! 🐙

A step of the fold scan rewrites a bounded prefix of the state word and drops a bounded number of its bits: the flag and the slot are rebuilt, and the stack in the tail is popped by the arity of a completed block's symbol and pushed with the algebra's value.

theorem stateWordF_foldScanStep_of_lt (R : RankedAlphabet) (enc : α → Fin p → Bool) (alg : (i : Fin R.card) → (Fin (R.arity i) → α) → α) (b : Bool) (s : FoldScan α) (h : s.buf.length < R.width) : stateWordF R enc (foldScanStep R alg b s) = nextPrefixF R enc alg b s ++ (stateWordF R enc s).drop (dropCountF R p b s) := α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Bools:FoldScan αh:s.buf.length < R.width⊢ stateWordF R enc (foldScanStep R alg b s) = nextPrefixF R enc alg b s ++ List.drop (dropCountF R p b s) (stateWordF R enc s) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Bools:FoldScan αh:s.buf.length < R.widthhpre:(s.live :: bufBits R s.buf).length = 1 + R.width⊢ stateWordF R enc (foldScanStep R alg b s) = nextPrefixF R enc alg b s ++ List.drop (dropCountF R p b s) (stateWordF R enc s) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Bools:FoldScan αh:s.buf.length < R.widthhpre:(s.live :: bufBits R s.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc s) = stackBits enc s.stack⊢ stateWordF R enc (foldScanStep R alg b s) = nextPrefixF R enc alg b s ++ List.drop (dropCountF R p b s) (stateWordF R enc s) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Bools:FoldScan αh:s.buf.length < R.widthhpre:(s.live :: bufBits R s.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc s) = stackBits enc s.stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc s) = stackBits enc (List.drop n s.stack)⊢ stateWordF R enc (foldScanStep R alg b s) = nextPrefixF R enc alg b s ++ List.drop (dropCountF R p b s) (stateWordF R enc s) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αlive:Boolh:{ buf := buf, stack := stack, live := live }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := live }.live :: bufBits R { buf := buf, stack := stack, live := live }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := live }) = stackBits enc { buf := buf, stack := stack, live := live }.stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := live }) = stackBits enc (List.drop n { buf := buf, stack := stack, live := live }.stack)⊢ stateWordF R enc (foldScanStep R alg b { buf := buf, stack := stack, live := live }) = nextPrefixF R enc alg b { buf := buf, stack := stack, live := live } ++ List.drop (dropCountF R p b { buf := buf, stack := stack, live := live }) (stateWordF R enc { buf := buf, stack := stack, live := live }) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αlive:Boolh:{ buf := buf, stack := stack, live := live }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := live }.live :: bufBits R { buf := buf, stack := stack, live := live }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := live }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := live }) = stackBits enc (List.drop n stack)⊢ stateWordF R enc (foldScanStep R alg b { buf := buf, stack := stack, live := live }) = nextPrefixF R enc alg b { buf := buf, stack := stack, live := live } ++ List.drop (dropCountF R p b { buf := buf, stack := stack, live := live }) (stateWordF R enc { buf := buf, stack := stack, live := live }) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αlive:Boolh:{ buf := buf, stack := stack, live := live }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := live }.live :: bufBits R { buf := buf, stack := stack, live := live }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := live }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := live }) = stackBits enc (List.drop n stack)⊢ stateWordF R enc (match { buf := buf, stack := stack, live := live }.live with | false => { buf := buf, stack := stack, live := live } | true => if (b :: { buf := buf, stack := stack, live := live }.buf).length = R.width then match symOf R (decodeBits (b :: { buf := buf, stack := stack, live := live }.buf)) with | none => { buf := [], stack := { buf := buf, stack := stack, live := live }.stack, live := false } | some i => if h : R.arity i ≤ { buf := buf, stack := stack, live := live }.stack.length then { buf := [], stack := (alg i fun d ↦ { buf := buf, stack := stack, live := live }.stack[↑d]) :: List.drop (R.arity i) { buf := buf, stack := stack, live := live }.stack, live := true } else { buf := [], stack := { buf := buf, stack := stack, live := live }.stack, live := false } else { buf := b :: { buf := buf, stack := stack, live := live }.buf, stack := { buf := buf, stack := stack, live := live }.stack, live := true }) = (match { buf := buf, stack := stack, live := live }.live with | false => false :: bufBits R { buf := buf, stack := stack, live := live }.buf | true => if (b :: { buf := buf, stack := stack, live := live }.buf).length = R.width then match symOf R (decodeBits (b :: { buf := buf, stack := stack, live := live }.buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ { buf := buf, stack := stack, live := live }.stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ { buf := buf, stack := stack, live := live }.stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: { buf := buf, stack := stack, live := live }.buf)) ++ List.drop (match { buf := buf, stack := stack, live := live }.live with | false => 1 + R.width | true => if (b :: { buf := buf, stack := stack, live := live }.buf).length = R.width then match symOf R (decodeBits (b :: { buf := buf, stack := stack, live := live }.buf)) with | none => 1 + R.width | some i => if R.arity i ≤ { buf := buf, stack := stack, live := live }.stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := live }) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αlive:Boolh:{ buf := buf, stack := stack, live := live }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := live }.live :: bufBits R { buf := buf, stack := stack, live := live }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := live }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := live }) = stackBits enc (List.drop n stack)⊢ stateWordF R enc (match live with | false => { buf := buf, stack := stack, live := live } | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => { buf := [], stack := stack, live := false } | some i => if h : R.arity i ≤ stack.length then { buf := [], stack := (alg i fun d ↦ stack[↑d]) :: List.drop (R.arity i) stack, live := true } else { buf := [], stack := stack, live := false } else { buf := b :: buf, stack := stack, live := true }) = (match live with | false => false :: bufBits R buf | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)) ++ List.drop (match live with | false => 1 + R.width | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := live }) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := false }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := false }.live :: bufBits R { buf := buf, stack := stack, live := false }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := false }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := false }) = stackBits enc (List.drop n stack)⊢ stateWordF R enc (match false with | false => { buf := buf, stack := stack, live := false } | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => { buf := [], stack := stack, live := false } | some i => if h : R.arity i ≤ stack.length then { buf := [], stack := (alg i fun d ↦ stack[↑d]) :: List.drop (R.arity i) stack, live := true } else { buf := [], stack := stack, live := false } else { buf := b :: buf, stack := stack, live := true }) = (match false with | false => false :: bufBits R buf | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)) ++ List.drop (match false with | false => 1 + R.width | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := false })α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := true }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := true }.live :: bufBits R { buf := buf, stack := stack, live := true }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc (List.drop n stack)⊢ stateWordF R enc (match true with | false => { buf := buf, stack := stack, live := true } | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => { buf := [], stack := stack, live := false } | some i => if h : R.arity i ≤ stack.length then { buf := [], stack := (alg i fun d ↦ stack[↑d]) :: List.drop (R.arity i) stack, live := true } else { buf := [], stack := stack, live := false } else { buf := b :: buf, stack := stack, live := true }) = (match true with | false => false :: bufBits R buf | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)) ++ List.drop (match true with | false => 1 + R.width | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := false }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := false }.live :: bufBits R { buf := buf, stack := stack, live := false }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := false }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := false }) = stackBits enc (List.drop n stack)⊢ stateWordF R enc (match false with | false => { buf := buf, stack := stack, live := false } | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => { buf := [], stack := stack, live := false } | some i => if h : R.arity i ≤ stack.length then { buf := [], stack := (alg i fun d ↦ stack[↑d]) :: List.drop (R.arity i) stack, live := true } else { buf := [], stack := stack, live := false } else { buf := b :: buf, stack := stack, live := true }) = (match false with | false => false :: bufBits R buf | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)) ++ List.drop (match false with | false => 1 + R.width | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := false }) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := false }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := false }.live :: bufBits R { buf := buf, stack := stack, live := false }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := false }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := false }) = stackBits enc (List.drop n stack)⊢ stateWordF R enc { buf := buf, stack := stack, live := false } = false :: bufBits R buf ++ List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := false }) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := false }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := false }.live :: bufBits R { buf := buf, stack := stack, live := false }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := false }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := false }) = stackBits enc (List.drop n stack)⊢ stateWordF R enc { buf := buf, stack := stack, live := false } = false :: bufBits R buf ++ stackBits enc stack All goals completed! 🐙 α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := true }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := true }.live :: bufBits R { buf := buf, stack := stack, live := true }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc (List.drop n stack)⊢ stateWordF R enc (match true with | false => { buf := buf, stack := stack, live := true } | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => { buf := [], stack := stack, live := false } | some i => if h : R.arity i ≤ stack.length then { buf := [], stack := (alg i fun d ↦ stack[↑d]) :: List.drop (R.arity i) stack, live := true } else { buf := [], stack := stack, live := false } else { buf := b :: buf, stack := stack, live := true }) = (match true with | false => false :: bufBits R buf | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)) ++ List.drop (match true with | false => 1 + R.width | true => if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := true }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := true }.live :: bufBits R { buf := buf, stack := stack, live := true }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc (List.drop n stack)⊢ stateWordF R enc (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => { buf := [], stack := stack, live := false } | some i => if h : R.arity i ≤ stack.length then { buf := [], stack := (alg i fun d ↦ stack[↑d]) :: List.drop (R.arity i) stack, live := true } else { buf := [], stack := stack, live := false } else { buf := b :: buf, stack := stack, live := true }) = (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)) ++ List.drop (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := true }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := true }.live :: bufBits R { buf := buf, stack := stack, live := true }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc (List.drop n stack)hlen:(b :: buf).length = R.width⊢ stateWordF R enc (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => { buf := [], stack := stack, live := false } | some i => if h : R.arity i ≤ stack.length then { buf := [], stack := (alg i fun d ↦ stack[↑d]) :: List.drop (R.arity i) stack, live := true } else { buf := [], stack := stack, live := false } else { buf := b :: buf, stack := stack, live := true }) = (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)) ++ List.drop (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true })α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := true }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := true }.live :: bufBits R { buf := buf, stack := stack, live := true }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc (List.drop n stack)hlen:¬(b :: buf).length = R.width⊢ stateWordF R enc (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => { buf := [], stack := stack, live := false } | some i => if h : R.arity i ≤ stack.length then { buf := [], stack := (alg i fun d ↦ stack[↑d]) :: List.drop (R.arity i) stack, live := true } else { buf := [], stack := stack, live := false } else { buf := b :: buf, stack := stack, live := true }) = (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)) ++ List.drop (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := true }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := true }.live :: bufBits R { buf := buf, stack := stack, live := true }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc (List.drop n stack)hlen:(b :: buf).length = R.width⊢ stateWordF R enc (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => { buf := [], stack := stack, live := false } | some i => if h : R.arity i ≤ stack.length then { buf := [], stack := (alg i fun d ↦ stack[↑d]) :: List.drop (R.arity i) stack, live := true } else { buf := [], stack := stack, live := false } else { buf := b :: buf, stack := stack, live := true }) = (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)) ++ List.drop (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := true }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := true }.live :: bufBits R { buf := buf, stack := stack, live := true }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc (List.drop n stack)hlen:(b :: buf).length = R.width⊢ stateWordF R enc (match symOf R (decodeBits (b :: buf)) with | none => { buf := [], stack := stack, live := false } | some i => if h : R.arity i ≤ stack.length then { buf := [], stack := (alg i fun d ↦ stack[↑d]) :: List.drop (R.arity i) stack, live := true } else { buf := [], stack := stack, live := false }) = (match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R []) ++ List.drop (match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) match hsym : symOf R (decodeBits (b :: buf)) with α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := true }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := true }.live :: bufBits R { buf := buf, stack := stack, live := true }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc (List.drop n stack)hlen:(b :: buf).length = R.widthhsym:symOf R (decodeBits (b :: buf)) = none⊢ stateWordF R enc (match none with | none => { buf := [], stack := stack, live := false } | some i => if h : R.arity i ≤ stack.length then { buf := [], stack := (alg i fun d ↦ stack[↑d]) :: List.drop (R.arity i) stack, live := true } else { buf := [], stack := stack, live := false }) = (match none with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R []) ++ List.drop (match none with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := true }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := true }.live :: bufBits R { buf := buf, stack := stack, live := true }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc (List.drop n stack)hlen:(b :: buf).length = R.widthhsym:symOf R (decodeBits (b :: buf)) = none⊢ stateWordF R enc { buf := [], stack := stack, live := false } = false :: bufBits R [] ++ List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := true }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := true }.live :: bufBits R { buf := buf, stack := stack, live := true }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc (List.drop n stack)hlen:(b :: buf).length = R.widthhsym:symOf R (decodeBits (b :: buf)) = none⊢ stateWordF R enc { buf := [], stack := stack, live := false } = false :: bufBits R [] ++ stackBits enc stack All goals completed! 🐙 α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := true }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := true }.live :: bufBits R { buf := buf, stack := stack, live := true }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc (List.drop n stack)hlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some i⊢ stateWordF R enc (match some i with | none => { buf := [], stack := stack, live := false } | some i => if h : R.arity i ≤ stack.length then { buf := [], stack := (alg i fun d ↦ stack[↑d]) :: List.drop (R.arity i) stack, live := true } else { buf := [], stack := stack, live := false }) = (match some i with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R []) ++ List.drop (match some i with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := true }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := true }.live :: bufBits R { buf := buf, stack := stack, live := true }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc (List.drop n stack)hlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some i⊢ stateWordF R enc (if h : R.arity i ≤ stack.length then { buf := [], stack := (alg i fun d ↦ stack[↑d]) :: List.drop (R.arity i) stack, live := true } else { buf := [], stack := stack, live := false }) = (if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R []) ++ List.drop (if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := true }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := true }.live :: bufBits R { buf := buf, stack := stack, live := true }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc (List.drop n stack)hlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihst:R.arity i ≤ stack.length⊢ stateWordF R enc (if h : R.arity i ≤ stack.length then { buf := [], stack := (alg i fun d ↦ stack[↑d]) :: List.drop (R.arity i) stack, live := true } else { buf := [], stack := stack, live := false }) = (if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R []) ++ List.drop (if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true })α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := true }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := true }.live :: bufBits R { buf := buf, stack := stack, live := true }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc (List.drop n stack)hlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihst:¬R.arity i ≤ stack.length⊢ stateWordF R enc (if h : R.arity i ≤ stack.length then { buf := [], stack := (alg i fun d ↦ stack[↑d]) :: List.drop (R.arity i) stack, live := true } else { buf := [], stack := stack, live := false }) = (if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R []) ++ List.drop (if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := true }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := true }.live :: bufBits R { buf := buf, stack := stack, live := true }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc (List.drop n stack)hlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihst:R.arity i ≤ stack.length⊢ stateWordF R enc (if h : R.arity i ≤ stack.length then { buf := [], stack := (alg i fun d ↦ stack[↑d]) :: List.drop (R.arity i) stack, live := true } else { buf := [], stack := stack, live := false }) = (if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R []) ++ List.drop (if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := true }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := true }.live :: bufBits R { buf := buf, stack := stack, live := true }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc (List.drop n stack)hlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihst:R.arity i ≤ stack.length⊢ { buf := [], stack := (alg i fun d ↦ stack[↑d]) :: List.drop (R.arity i) stack, live := true }.live :: (bufBits R { buf := [], stack := (alg i fun d ↦ stack[↑d]) :: List.drop (R.arity i) stack, live := true }.buf ++ stackBits enc { buf := [], stack := (alg i fun d ↦ stack[↑d]) :: List.drop (R.arity i) stack, live := true }.stack) = true :: bufBits R [] ++ (entryBits enc (alg i fun d ↦ stack[↑d]) ++ stackBits enc (List.drop (R.arity i) stack)) All goals completed! 🐙 α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := true }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := true }.live :: bufBits R { buf := buf, stack := stack, live := true }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc (List.drop n stack)hlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihst:¬R.arity i ≤ stack.length⊢ stateWordF R enc (if h : R.arity i ≤ stack.length then { buf := [], stack := (alg i fun d ↦ stack[↑d]) :: List.drop (R.arity i) stack, live := true } else { buf := [], stack := stack, live := false }) = (if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R []) ++ List.drop (if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := true }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := true }.live :: bufBits R { buf := buf, stack := stack, live := true }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc (List.drop n stack)hlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihst:¬R.arity i ≤ stack.length⊢ stateWordF R enc { buf := [], stack := stack, live := false } = false :: bufBits R [] ++ stackBits enc stack All goals completed! 🐙 α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := true }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := true }.live :: bufBits R { buf := buf, stack := stack, live := true }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc (List.drop n stack)hlen:¬(b :: buf).length = R.width⊢ stateWordF R enc (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => { buf := [], stack := stack, live := false } | some i => if h : R.arity i ≤ stack.length then { buf := [], stack := (alg i fun d ↦ stack[↑d]) :: List.drop (R.arity i) stack, live := true } else { buf := [], stack := stack, live := false } else { buf := b :: buf, stack := stack, live := true }) = (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => false :: bufBits R [] | some i => if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits enc (alg i fun d ↦ stack[↑d]) else false :: bufBits R [] else true :: bufBits R (b :: buf)) ++ List.drop (if (b :: buf).length = R.width then match symOf R (decodeBits (b :: buf)) with | none => 1 + R.width | some i => if R.arity i ≤ stack.length then 1 + R.width + (p + 1) * R.arity i else 1 + R.width else 1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) α:Type up:ℕR:RankedAlphabetenc:α → Fin p → Boolalg:(i : Fin R.card) → (Fin (R.arity i) → α) → αb:Boolbuf:List Boolstack:List αh:{ buf := buf, stack := stack, live := true }.buf.length < R.widthhpre:({ buf := buf, stack := stack, live := true }.live :: bufBits R { buf := buf, stack := stack, live := true }.buf).length = 1 + R.widthhdrop:List.drop (1 + R.width) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc stackhdropr:∀ (n : ℕ), List.drop (1 + R.width + (p + 1) * n) (stateWordF R enc { buf := buf, stack := stack, live := true }) = stackBits enc (List.drop n stack)hlen:¬(b :: buf).length = R.width⊢ stateWordF R enc { buf := b :: buf, stack := stack, live := true } = true :: bufBits R (b :: buf) ++ stackBits enc stack All goals completed! 🐙
end Geb.CobhamFoldend