Ordered folds over fixed-width bitstrings

The first count strings are enumerated by their little-endian numeric value. The complete fold visits all 2 ^ width strings, including the single empty string when width = 0. The update need not be associative or commutative.

def Complexity.bitstringFoldPrefix (update : List Bool → List Bool → List Bool) (seed : List Bool) (width : ℕ) : ℕ → List Bool

Fold over the first count fixed-width bitstrings in little-endian numeric order. Prefixes past 2 ^ width repeat candidates; the space theorem only bounds and uses prefixes up to that endpoint.

Equations

• Complexity.bitstringFoldPrefix update seed width 0 = seed
• Complexity.bitstringFoldPrefix update seed width count.succ = update (width.toBitsLE count) (Complexity.bitstringFoldPrefix update seed width count)

@[simp]

theorem Complexity.bitstringFoldPrefix_zero (update : List Bool → List Bool → List Bool) (seed : List Bool) (width : ℕ) : bitstringFoldPrefix update seed width 0 = seed

@[simp]

theorem Complexity.bitstringFoldPrefix_succ (update : List Bool → List Bool → List Bool) (seed : List Bool) (width count : ℕ) : bitstringFoldPrefix update seed width (count + 1) = update (width.toBitsLE count) (bitstringFoldPrefix update seed width count)

def Complexity.bitstringFold (update : List Bool → List Bool → List Bool) (seed : List Bool) (width : ℕ) : List Bool

Fold over every string of exactly width bits, in little-endian numeric order.

Equations

• Complexity.bitstringFold update seed width = Complexity.bitstringFoldPrefix update seed width (2 ^ width)

@[simp]

theorem Complexity.bitstringFold_zero (update : List Bool → List Bool → List Bool) (seed : List Bool) : bitstringFold update seed 0 = update [] seed

A zero-width fold still performs one update, with the empty candidate.