fromNat_expt: (all x:Nat, y:Nat. fromNat(x ^ y) = fromNat(x) ^ fromNat(y))

less_pow_log: (all n:UInt. (if 0 < n then n < 2 ^ (1 + log(n))))

auto lit_expt_fromNat

lit_expt_fromNat: (all x:Nat, y:Nat. fromNat(lit(x)) ^ fromNat(lit(y)) = fromNat(lit(x) ^ lit(y)))

auto lit_pow_mul_r

lit_pow_mul_r: (all m:Nat, n:Nat, o:UInt. fromNat(lit(m)) ^ (fromNat(lit(n)) * o) = (fromNat(lit(m)) ^ fromNat(lit(n))) ^ o)

log_pow: (all n:UInt. log(2 ^ n) = n)

toNat_expt: (all p:UInt, n:UInt. toNat(n ^ p) = toNat(n) ^ toNat(p))

uint_expt_log_less_equal: (all n:UInt. (if 0 < n then 2 ^ log(n) ≤ n))

uint_expt_one: (all n:UInt. n ^ 1 = n)

auto uint_expt_suc

uint_expt_suc: (all n:UInt, m:Nat. n ^ fromNat(lit(suc(m))) = n * n ^ fromNat(lit(m)))

uint_expt_two: (all n:UInt. n ^ 2 = n * n)

auto uint_expt_zero

uint_expt_zero: (all n:UInt. n ^ 0 = 1)

uint_log_add_le_log_mult: (all m:UInt, n:UInt. log(m) + log(n) ≤ log(m * n))

uint_log_greater_one: (all n:UInt. (if 2 ≤ n then 1 ≤ log(n)))

uint_log_mono: (all x:UInt, y:UInt. (if x ≤ y then log(x) ≤ log(y)))

uint_log_mult_le_log_add: (all m:UInt, n:UInt. log(m * n) ≤ (1 + log(m)) + log(n))

uint_log_pos: (all n:UInt. (if 1 < n then 0 < log(n)))

uint_logn_le_n: (all n:UInt. log(n) ≤ n)

uint_one_expt: (all n:UInt. 1 ^ n = 1)

uint_pow_add_r: (all m:UInt, n:UInt, o:UInt. m ^ (n + o) = m ^ n * m ^ o)

uint_pow_mul_l: (all m:UInt, n:UInt, o:UInt. (m * n) ^ o = m ^ o * n ^ o)

uint_pow_mul_r: (all m:UInt, n:UInt, o:UInt. (m ^ n) ^ o = m ^ (n * o))