def BitVec.iunfoldr {w : Nat} {α : Type u_1} (f : Fin w → α → α × Bool) (s : α) : α × BitVec w

iunfoldr is an iterative operation that applies a function f repeatedly.

It produces a sequence of state values [s_0, s_1 .. s_w] and a bitvector v where f i s_i = (s_{i+1}, b_i) and b_i is bit ith least-significant bit in v (e.g., getLsb v i = b_i).

Theorems involving iunfoldr can be eliminated using iunfoldr_replace below.

Equations

• One or more equations did not get rendered due to their size.

theorem BitVec.iunfoldr.fst_eq {w : Nat} {α : Type u_1} {f : Fin w → α → α × Bool} (state : Nat → α) (s : α) (init : s = state 0) (ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)) : (BitVec.iunfoldr f s).fst = state w

theorem BitVec.iunfoldr_replace {w : Nat} {α : Type u_1} {f : Fin w → α → α × Bool} (state : Nat → α) (value : BitVec w) (a : α) (init : state 0 = a) (step : ∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), BitVec.getLsb value ↑i)) : BitVec.iunfoldr f a = (state w, value)

Correctness theorem for iunfoldr.