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. (if ((0 < m) and (0 < n)) then log(m) + log(n) ≤ log(m * n)))

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

uint_log_lt: (all n:UInt, m:UInt. (if 0 < n then ((log(n) < m) ⇔ (n < 2 ^ m))))

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))

auto uint_log_one

uint_log_one: log(1) = 0

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

uint_log_two: log(2) = 1

auto uint_log_zero

uint_log_zero: log(0) = 0

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

auto uint_one_expt

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_eq_one: (all m:UInt, n:UInt. (if m ^ n = 1 then ((n = 0) or (m = 1))))

uint_pow_eq_zero: (all m:UInt, n:UInt. (if m ^ n = 0 then m = 0))

uint_pow_gt_one: (all n:UInt, m:UInt. (if 1 < n then ((0 < m) ⇔ (1 < n ^ m))))

uint_pow_inj_l: (all a:UInt, b:UInt, c:UInt. (if 0 < c then (if a ^ c = b ^ c then a = b)))

uint_pow_inj_r: (all a:UInt, b:UInt, c:UInt. (if 1 < a then (if a ^ b = a ^ c then b = c)))

uint_pow_le_mono_l: (all c:UInt, a:UInt, b:UInt. (if a ≤ b then a ^ c ≤ b ^ c))

uint_pow_le_mono_r: (all c:UInt, a:UInt, b:UInt. (if 1 ≤ a then (if b ≤ c then a ^ b ≤ a ^ c)))

uint_pow_lt_implies_lt: (all c:UInt, a:UInt, b:UInt. (if 0 < c then (if a ^ c < b ^ c then a < b)))

uint_pow_lt_mono_l: (all c:UInt, a:UInt, b:UInt. (if 0 < c then (if a < b then a ^ c < b ^ c)))

uint_pow_lt_mono_r: (all c:UInt, a:UInt, b:UInt. (if 1 < a then (if b < c then a ^ b < a ^ c)))

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))

uint_pow_pos: (all a:UInt, b:UInt. (if 0 < a then 0 < a ^ b))

uint_zero_pow: (all a:UInt. (if 0 < a then 0 ^ a = 0))