@[irreducible]

def lastPowerOfTwo_iter (m n : Nat) : Nat

Equations

• lastPowerOfTwo_iter m n = if m = 0 then 1 else if 2 ^ m < n then 2 ^ m else lastPowerOfTwo_iter (m - 1) n

def lastPowerOfTwo (n : Nat) : Nat

Returns the largest power of two strictly less than n.

If no such number exists, returns 1 instead.

Equations

• lastPowerOfTwo n = lastPowerOfTwo_iter ((n + 1) / 2) n

theorem sub_two_le {n : Nat} : n - 2 ≤ n

theorem le_two_pow {n : Nat} : n ≤ 2 ^ n