fun Even(n:UInt) {
  some m:UInt. n = 2 * m
}

union Int {
  pos(UInt)
  negsuc(UInt)
}

fun Odd(n:UInt) {
  some m:UInt. n = 1 + 2 * m
}

view UInt {
  source Binary
  target UIntView
  into uint_view
  out uint_unview
  roundtrip uint_view_unview
}

fun abs(x:Int)

fun div2(b:UInt)

fun divides(a:UInt, b:UInt) {
  some k:UInt. a * k = b
}

fun fromNat(Nat) -> UInt

fromNat_add: (all x:Nat, y:Nat. fromNat(x + y) = fromNat(x) + fromNat(y))

fromNat_div: (all x:Nat, y:Nat. fromNat(x) / fromNat(y) = fromNat(x / y))

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

fromNat_injective: (all x:Nat, y:Nat. (if fromNat(x) = fromNat(y) then x = y))

fromNat_mod: (all x:Nat, y:Nat. fromNat(x) % fromNat(y) = fromNat(x % y))

fromNat_mult: (all x:Nat, y:Nat. fromNat(x * y) = fromNat(x) * fromNat(y))

recfun gcd(a:UInt, b:UInt) -> UInt
measure	b  {
  if b = 0 then
    a
  else
    gcd(b, a % b)
}

inc_add_one: (all n:UInt. inc(n) = 1 + n)

less_equal_fromNat: (all x:Nat, y:Nat. (if x ≤ y then fromNat(x) ≤ fromNat(y)))

less_equal_toNat: (all x:UInt, y:UInt. (if toNat(x) ≤ toNat(y) then x ≤ y))

less_fromNat: (all x:Nat, y:Nat. (if x < y then fromNat(x) < fromNat(y)))

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

less_toNat: (all x:UInt, y:UInt. (if toNat(x) < toNat(y) then x < y))

auto lit_add_fromNat

lit_add_fromNat: (all x:Nat, y:Nat. fromNat(lit(x)) + fromNat(lit(y)) = fromNat(lit(x) + lit(y)))

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_monus_fromNat

lit_monus_fromNat: (all x:Nat, y:Nat. fromNat(lit(x)) ∸ fromNat(lit(y)) = fromNat(lit(x) ∸ lit(y)))

auto lit_mult_fromNat

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

fun log(b:UInt)

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

fun max(x:UInt, y:UInt) {
  if x < y then
    y
  else
    x
}

fun max(x:Int, y:Int) {
  if x < y then
    y
  else
    x
}

fun min(x:UInt, y:UInt) {
  if x < y then
    x
  else
    y
}

fun min(x:Int, y:Int) {
  if x < y then
    x
  else
    y
}

fun operator %(n:UInt, m:UInt) {
  n ∸ (n / m) * m
}

fun operator *(UInt,UInt) -> UInt

fun operator *(x:Int, y:Int)

fun operator *(n:UInt, m:Int)

fun operator *(n:Int, m:UInt)

fun operator +(UInt,UInt) -> UInt

fun operator +(x:Int, m:Int)

fun operator +(n:UInt, m:Int)

fun operator +(n:Int, m:UInt)

fun operator -(x:Int)

fun operator -(n:UInt)

fun operator -(n:Int, m:Int) {
  n + - m
}

fun operator -(n:UInt, m:Int)

fun operator -(n:Int, m:UInt)

fun operator -(x:UInt, y:UInt)

recfun operator /(n:UInt, m:UInt) -> UInt
measure	n  {
  if n < m then
    0
  else
    if m = 0 then
      0
    else
      1 + (n ∸ m) / m
}

fun operator /(n:Int, m:Int)

fun operator /(n:Int, m:UInt)

fun operator <(UInt,UInt) -> bool

fun operator <(a:Int, y:Int)

fun operator >(x:UInt, y:UInt) {
  y < x
}

fun operator >(x:Int, y:Int) {
  y < x
}

fun operator ^(a:UInt, b:UInt)

fun operator ∸(UInt,UInt) -> UInt

fun operator ≤(x:UInt, y:UInt) {
  ((x < y) or (x = y))
}

fun operator ≤(a:Int, y:Int)

fun operator ≥(x:UInt, y:UInt) {
  y ≤ x
}

fun operator ≥(x:Int, y:Int) {
  y ≤ x
}

fun sqr(a:UInt) {
  a * a
}

fun toNat(UInt) -> Nat

toNat_add: (all x:UInt, y:UInt. toNat(x + y) = toNat(x) + toNat(y))

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

toNat_less: (all x:UInt, y:UInt. (if x < y then toNat(x) < toNat(y)))

toNat_less_equal: (all x:UInt, y:UInt. (if x ≤ y then toNat(x) ≤ toNat(y)))

toNat_mod: (all x:UInt, y:UInt. toNat(x % y) = toNat(x) % toNat(y))

toNat_monus: (all x:UInt, y:UInt. toNat(x ∸ y) = toNat(x) ∸ toNat(y))

toNat_mult: (all x:UInt, y:UInt. toNat(x * y) = toNat(x) * toNat(y))

toNat_uint_summation: (all k:UInt, begin:UInt, f:(fn UInt -> UInt). toNat(uint_summation(k, begin, f)) = summation(toNat(k), toNat(begin), fun i { toNat(f(fromNat(i))) }))

uint_Even_not_Odd: (all n:UInt. (Even(n) ⇔ not Odd(n)))

uint_Even_or_Odd: (all n:UInt. (Even(n) or Odd(n)))

uint_add_assoc: (all x:UInt, y:UInt, z:UInt. (x + y) + z = x + (y + z))

uint_add_both_monus: (all z:UInt, y:UInt, x:UInt. (z + y) ∸ (z + x) = y ∸ x)

uint_add_both_sides_of_equal: (all x:UInt, y:UInt, z:UInt. ((x + y = x + z) ⇔ (y = z)))

auto uint_add_both_sides_of_le_equal

uint_add_both_sides_of_le_equal: (all x:UInt. (all y:UInt, z:UInt. (x + y ≤ x + z) = (y ≤ z)))

uint_add_both_sides_of_less: (all x:UInt, y:UInt, z:UInt. ((x + y < x + z) ⇔ (y < z)))

uint_add_both_sides_of_less_equal: (all x:UInt. (all y:UInt, z:UInt. ((x + y ≤ x + z) ⇔ (y ≤ z))))

uint_add_commute: (all x:UInt, y:UInt. x + y = y + x)

uint_add_div_one: (all n:UInt, m:UInt. (if 0 < m then (n + m) / m = 1 + n / m))

uint_add_mod: (all a:UInt, b:UInt, m:UInt. (if 0 < m then (a + b) % m = (a % m + b % m) % m))

uint_add_mono_less: (all a:UInt, b:UInt, c:UInt, d:UInt. (if ((a < c) and (b < d)) then a + b < c + d))

uint_add_mono_less_equal: (all a:UInt, b:UInt, c:UInt, d:UInt. (if ((a ≤ c) and (b ≤ d)) then a + b ≤ c + d))

auto uint_add_monus_identity

uint_add_monus_identity: (all m:UInt, n:UInt. (m + n) ∸ m = n)

uint_add_mult_div: (all n:UInt, k:UInt, m:UInt. (if 0 < m then (n + k * m) / m = k + n / m))

uint_add_mult_mod: (all n:UInt, k:UInt, m:UInt. (if 0 < m then (n + k * m) % m = n % m))

uint_add_one_le_double: (all x:UInt. (if 0 < x then 1 + x ≤ x + x))

uint_add_to_zero: (all n:UInt, m:UInt. (if n + m = 0 then ((n = 0) and (m = 0))))

auto uint_add_zero

uint_add_zero: (all x:UInt. x + 0 = x)

uint_dichotomy: (all x:UInt, y:UInt. ((x ≤ y) or (y < x)))

uint_dist_mult_add: (all a:UInt, x:UInt, y:UInt. a * (x + y) = a * x + a * y)

uint_dist_mult_add_right: (all x:UInt, y:UInt, a:UInt. (x + y) * a = x * a + y * a)

uint_dist_mult_monus: (all x:UInt. (all y:UInt, z:UInt. x * (y ∸ z) = x * y ∸ x * z))

uint_div_cancel: (all y:UInt. (if 0 < y then y / y = 1))

uint_div_less: (all n:UInt, m:UInt. (if ((0 < n) and (1 < m)) then n / m < n))

uint_div_less_equal: (all n:UInt, m:UInt. (if 0 < m then n / m ≤ n))

uint_div_mod: (all n:UInt, m:UInt. (if 0 < m then (n / m) * m + n % m = n))

uint_div_one: (all n:UInt. n / 1 = n)

uint_div_zero: (all n:UInt. n / 0 = 0)

uint_divides_add: (all d:UInt, m:UInt, n:UInt. (if (divides(d, m) and divides(d, n)) then divides(d, m + n)))

uint_divides_antisymmetric: (all a:UInt, b:UInt. (if (divides(a, b) and divides(b, a)) then a = b))

uint_divides_less_equal: (all a:UInt, b:UInt. (if (divides(a, b) and (0 < b)) then a ≤ b))

uint_divides_mod: (all d:UInt, m:UInt, n:UInt. (if (divides(d, n) and divides(d, m % n) and (0 < n)) then divides(d, m)))

uint_divides_mod_of_divides: (all d:UInt, m:UInt, n:UInt. (if (divides(d, m) and divides(d, n)) then divides(d, m % n)))

uint_divides_monus: (all d:UInt, m:UInt, n:UInt. (if (divides(d, m) and divides(d, n)) then divides(d, m ∸ n)))

uint_divides_mult_left: (all d:UInt, n:UInt, m:UInt. (if divides(d, n) then divides(d, m * n)))

uint_divides_mult_right: (all d:UInt, n:UInt, m:UInt. (if divides(d, n) then divides(d, n * m)))

uint_divides_refl: (all n:UInt. divides(n, n))

uint_divides_trans: (all a:UInt, b:UInt, c:UInt. (if (divides(a, b) and divides(b, c)) then divides(a, c)))

uint_divides_zero: (all n:UInt. divides(n, 0))

auto uint_equal

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

uint_equal_implies_less_equal: (all x:UInt, y:UInt. (if x = y then x ≤ y))

uint_even_add_even: (all x:UInt, y:UInt. (if (Even(x) and Even(y)) then Even(x + y)))

uint_even_add_odd: (all x:UInt, y:UInt. (if (Even(x) and Odd(y)) then Odd(x + y)))

uint_even_mult_left: (all x:UInt, y:UInt. (if Even(x) then Even(x * y)))

uint_even_mult_right: (all x:UInt, y:UInt. (if Even(y) then Even(x * y)))

uint_even_one_odd: (all n:UInt. (if Even(1 + n) then Odd(n)))

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_fromNat_toNat: (all b:UInt. fromNat(toNat(b)) = b)

uint_gcd_divides: (all b:UInt, a:UInt. (divides(gcd(a, b), a) and divides(gcd(a, b), b)))

uint_gcd_divides_left: (all a:UInt, b:UInt. divides(gcd(a, b), a))

uint_gcd_divides_right: (all a:UInt, b:UInt. divides(gcd(a, b), b))

uint_gcd_greatest: (all d:UInt, a:UInt, b:UInt. (if (divides(d, a) and divides(d, b)) then divides(d, gcd(a, b))))

uint_greater_implies_not_equal: (all x:UInt, y:UInt. (if x > y then not (x = y)))

uint_induction: (all P:(fn UInt -> bool). (if (P(0) and (all m:UInt. (if P(m) then P(1 + m)))) then (all n:UInt. P(n))))

uint_k_induction: (all P:(fn UInt -> bool), k:UInt. (if (P(k) and (all m:UInt. (if ((k ≤ m) and P(m)) then P(1 + m)))) then (all n:UInt. (if k ≤ n then P(n)))))

uint_le_exists_monus: (all n:UInt, m:UInt. (if n ≤ m then some x:UInt. m = n + x))

uint_less_add_one_implies_less_equal: (all x:UInt, y:UInt. (if x < 1 + y then x ≤ y))

uint_less_equal_add: (all x:UInt, y:UInt. x ≤ x + y)

uint_less_equal_add_left: (all x:UInt, y:UInt. y ≤ x + y)

uint_less_equal_antisymmetric: (all x:UInt, y:UInt. (if ((x ≤ y) and (y ≤ x)) then x = y))

uint_less_equal_refl: (all n:UInt. n ≤ n)

auto uint_less_equal_refl_true

uint_less_equal_refl_true: (all n:UInt. (n ≤ n) = true)

uint_less_equal_trans: (all x:UInt, y:UInt, z:UInt. (if ((x ≤ y) and (y ≤ z)) then x ≤ z))

uint_less_equal_zero: (all x:UInt. (if x ≤ 0 then x = 0))

uint_less_implies_less_equal: (all x:UInt, y:UInt. (if x < y then x ≤ y))

uint_less_implies_not_equal: (all x:UInt, y:UInt. (if x < y then not (x = y)))

uint_less_implies_not_greater: (all x:UInt, y:UInt. (if x < y then not (y < x)))

uint_less_irreflexive: (all x:UInt. not (x < x))

uint_less_is_less_equal: (all x:UInt, y:UInt. (x < y) = (1 + x ≤ y))

uint_less_plus1: (all n:UInt. n < 1 + n)

auto uint_less_plus1_true

uint_less_plus1_true: (all n:UInt. (n < 1 + n) = true)

auto uint_less_refl_false

uint_less_refl_false: (all x:UInt. (x < x) = false)

uint_less_trans: (all x:UInt, y:UInt, z:UInt. (if ((x < y) and (y < z)) then x < z))

auto uint_lit_div

uint_lit_div: (all x:Nat, y:Nat. fromNat(lit(x)) / fromNat(lit(y)) = fromNat(lit(x) / lit(y)))

auto uint_lit_less

uint_lit_less: (all x:Nat, y:Nat. (fromNat(lit(x)) < fromNat(lit(y))) = (lit(x) < lit(y)))

auto uint_lit_less_equal

uint_lit_less_equal: (all x:Nat, y:Nat. (fromNat(lit(x)) ≤ fromNat(lit(y))) = (lit(x) ≤ lit(y)))

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)

uint_max_assoc: (all x:UInt, y:UInt, z:UInt. max(max(x, y), z) = max(x, max(y, z)))

uint_max_equal_greater_left: (all x:UInt, y:UInt. (if y ≤ x then max(x, y) = x))

uint_max_equal_greater_right: (all x:UInt, y:UInt. (if x ≤ y then max(x, y) = y))

uint_max_greater_left: (all x:UInt, y:UInt. x ≤ max(x, y))

uint_max_greater_right: (all x:UInt, y:UInt. y ≤ max(x, y))

uint_max_idempotent: (all x:UInt. max(x, x) = x)

uint_max_is_left_or_right: (all x:UInt, y:UInt. ((max(x, y) = x) or (max(x, y) = y)))

uint_max_less_equal: (all x:UInt, y:UInt, z:UInt. (if ((x ≤ z) and (y ≤ z)) then max(x, y) ≤ z))

uint_max_min_absorb_left: (all x:UInt, y:UInt. max(x, min(x, y)) = x)

uint_max_min_absorb_right: (all x:UInt, y:UInt. max(min(x, y), x) = x)

uint_max_symmetric: (all x:UInt, y:UInt. max(x, y) = max(y, x))

auto uint_max_zero

uint_max_zero: (all x:UInt. max(x, 0) = x)

uint_min_equal_less_left: (all x:UInt, y:UInt. (if x ≤ y then min(x, y) = x))

uint_min_equal_less_right: (all x:UInt, y:UInt. (if y ≤ x then min(x, y) = y))

uint_min_greatest_less_equal: (all x:UInt, y:UInt, z:UInt. (if ((z ≤ x) and (z ≤ y)) then z ≤ min(x, y)))

uint_min_idempotent: (all x:UInt. min(x, x) = x)

uint_min_is_left_or_right: (all x:UInt, y:UInt. ((min(x, y) = x) or (min(x, y) = y)))

uint_min_less_equal_left: (all x:UInt, y:UInt. min(x, y) ≤ x)

uint_min_less_equal_right: (all x:UInt, y:UInt. min(x, y) ≤ y)

uint_min_max_absorb_left: (all x:UInt, y:UInt. min(x, max(x, y)) = x)

uint_min_max_absorb_right: (all x:UInt, y:UInt. min(max(x, y), x) = x)

uint_min_symmetric: (all x:UInt, y:UInt. min(x, y) = min(y, x))

uint_mod_less_divisor: (all n:UInt, m:UInt. (if 0 < m then n % m < m))

uint_mod_mod: (all n:UInt, m:UInt. (if 0 < m then (n % m) % m = n % m))

uint_mod_one: (all n:UInt. n % 1 = 0)

uint_mod_self_zero: (all y:UInt. y % y = 0)

uint_mod_small: (all n:UInt, m:UInt. (if n < m then n % m = n))

uint_monus_add_assoc: (all n:UInt, l:UInt, m:UInt. (if m ≤ n then l + (n ∸ m) = (l + n) ∸ m))

uint_monus_add_identity: (all n:UInt. (all m:UInt. (if m ≤ n then m + (n ∸ m) = n)))

auto uint_monus_cancel

uint_monus_cancel: (all n:UInt. n ∸ n = 0)

uint_monus_monus_eq_monus_add: (all x:UInt, y:UInt, z:UInt. (x ∸ y) ∸ z = x ∸ (y + z))

uint_monus_one_less: (all n:UInt. (if not (n = 0) then n ∸ 1 < n))

uint_monus_order: (all x:UInt, y:UInt, z:UInt. (x ∸ y) ∸ z = (x ∸ z) ∸ y)

auto uint_monus_zero

uint_monus_zero: (all n:UInt. n ∸ 0 = n)

uint_monus_zero_iff_less_eq: (all x:UInt, y:UInt. ((x ≤ y) ⇔ (x ∸ y = 0)))

uint_mult_add_div: (all k:UInt, n:UInt, m:UInt. (if 0 < m then (k * m + n) / m = k + n / m))

uint_mult_add_mod: (all k:UInt, n:UInt, m:UInt. (if 0 < m then (k * m + n) % m = n % m))

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

uint_mult_commute: (all m:UInt, n:UInt. m * n = n * m)

uint_mult_div_inverse: (all n:UInt, m:UInt. (if 0 < m then (n * m) / m = n))

uint_mult_div_left_inverse: (all n:UInt, m:UInt. (if 0 < m then (m * n) / m = n))

uint_mult_mod: (all a:UInt, b:UInt, m:UInt. (if 0 < m then (a * b) % m = ((a % m) * (b % m)) % m))

uint_mult_mod_left_zero: (all n:UInt, m:UInt. (if 0 < m then (m * n) % m = 0))

uint_mult_mod_right_zero: (all n:UInt, m:UInt. (if 0 < m then (n * m) % m = 0))

uint_mult_mono_le: (all n:UInt, x:UInt, y:UInt. (if x ≤ y then n * x ≤ n * y))

uint_mult_mono_le2: (all n:UInt, x:UInt, m:UInt, y:UInt. (if ((n ≤ m) and (x ≤ y)) then n * x ≤ m * y))

auto uint_mult_one

uint_mult_one: (all n:UInt. n * 1 = n)

uint_mult_to_zero: (all n:UInt, m:UInt. (if n * m = 0 then ((n = 0) or (m = 0))))

auto uint_mult_zero

uint_mult_zero: (all n:UInt. n * 0 = 0)

uint_not_less_equal_iff_greater: (all x:UInt, y:UInt. (not (x ≤ y) ⇔ (y < x)))

uint_not_less_implies_less_equal: (all x:UInt, y:UInt. (if not (x < y) then y ≤ x))

uint_not_less_zero: (all x:UInt. not (x < 0))

uint_not_one_add_le_zero: (all n:UInt. not (1 + n ≤ 0))

uint_not_one_add_zero: (all n:UInt. not (1 + n = 0))

uint_not_zero_pos: (all n:UInt. (if not (n = 0) then 0 < n))

uint_odd_add_even: (all x:UInt, y:UInt. (if (Odd(x) and Even(y)) then Odd(x + y)))

uint_odd_add_odd: (all x:UInt, y:UInt. (if (Odd(x) and Odd(y)) then Even(x + y)))

uint_odd_mult_odd: (all x:UInt, y:UInt. (if (Odd(x) and Odd(y)) then Odd(x * y)))

uint_odd_one_even: (all n:UInt. (if Odd(1 + n) then Even(n)))

auto uint_one_add_zero_false

uint_one_add_zero_false: (all n:UInt. (1 + n = 0) = false)

auto uint_one_expt

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

auto uint_one_mult

uint_one_mult: (all n:UInt. 1 * n = n)

uint_one_two_odd: (all n:UInt. Odd(1 + 2 * n))

uint_pos_implies_one_le: (all n:UInt. (if 0 < n then 1 ≤ n))

uint_pos_mult_both_sides_of_less: (all n:UInt, x:UInt, y:UInt. (if ((0 < n) and (x < y)) then n * x < n * y))

uint_pos_mult_left_cancel: (all n:UInt, x:UInt, y:UInt. (if ((0 < n) and (n * x = n * y)) then x = y))

uint_pos_mult_left_cancel_less: (all n:UInt, x:UInt, y:UInt. (if ((0 < n) and (n * x < n * y)) then x < y))

uint_pos_mult_left_cancel_less_equal: (all n:UInt, x:UInt, y:UInt. (if ((0 < n) and (n * x ≤ n * y)) then x ≤ y))

uint_pos_mult_right_cancel: (all n:UInt, x:UInt, y:UInt. (if ((0 < n) and (x * n = y * n)) then x = y))

uint_pos_mult_right_cancel_less: (all n:UInt, x:UInt, y:UInt. (if ((0 < n) and (x * n < y * n)) then x < y))

uint_pos_mult_right_cancel_less_equal: (all n:UInt, x:UInt, y:UInt. (if ((0 < n) and (x * n ≤ y * n)) then x ≤ y))

uint_pos_not_zero: (all n:UInt. (if 0 < n then not (n = 0)))

uint_positive_add_one: (all n:UInt. (if 0 < n then some n':UInt. n = 1 + n'))

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_strong_induction: (all P:(fn UInt -> bool), n:UInt. (if (all j:UInt. (if (all i:UInt. (if i < j then P(i))) then P(j))) then P(n)))

fun uint_summation(k:UInt, begin:UInt, f:(fn UInt -> UInt)) {
  fromNat(summation(toNat(k), toNat(begin), fun i { toNat(f(fromNat(i))) }))
}

uint_summation_add: (all a:UInt. (all b:UInt, s:UInt, t:UInt, f:(fn UInt -> UInt), g:(fn UInt -> UInt), h:(fn UInt -> UInt). (if ((all i:Nat. (if i < toNat(a) then g(s + fromNat(i)) = f(s + fromNat(i)))) and (all i:Nat. (if i < toNat(b) then h(t + fromNat(i)) = f((s + a) + fromNat(i))))) then uint_summation(a + b, s, f) = uint_summation(a, s, g) + uint_summation(b, t, h))))

uint_summation_cong: (all k:UInt. (all f:(fn UInt -> UInt), g:(fn UInt -> UInt), s:UInt, t:UInt. (if (all i:Nat. (if i < toNat(k) then f(s + fromNat(i)) = g(t + fromNat(i)))) then uint_summation(k, s, f) = uint_summation(k, t, g))))

uint_summation_next: (all n:UInt, s:UInt, f:(fn UInt -> UInt). uint_summation(1 + n, s, f) = uint_summation(n, s, f) + f(s + n))

uint_toNat_fromNat: (all x:Nat. toNat(fromNat(x)) = x)

uint_toNat_injective: (all x:UInt, y:UInt. (if toNat(x) = toNat(y) then x = y))

uint_trichotomy: (all x:UInt, y:UInt. ((x < y) or (x = y) or (y < x)))

uint_two_even: (all n:UInt. Even(2 * n))

uint_two_mult: (all n:UInt. 2 * n = n + n)

auto uint_zero_add

uint_zero_add: (all x:UInt. 0 + x = x)

uint_zero_div: (all x:UInt. (if 0 < x then 0 / x = 0))

uint_zero_le: (all x:UInt. 0 ≤ x)

uint_zero_le_zero: (all x:UInt. (if x ≤ 0 then x = 0))

auto uint_zero_less_equal_true

uint_zero_less_equal_true: (all x:UInt. (0 ≤ x) = true)

uint_zero_less_one_add: (all n:UInt. 0 < 1 + n)

auto uint_zero_less_one_add_true

uint_zero_less_one_add_true: (all n:UInt. (0 < 1 + n) = true)

auto uint_zero_max

uint_zero_max: (all x:UInt. max(0, x) = x)

uint_zero_mod: (all x:UInt. 0 % x = 0)

auto uint_zero_mult

uint_zero_mult: (all n:UInt. 0 * n = 0)

uint_zero_or_add_one: (all x:UInt. ((x = 0) or some x':UInt. x = 1 + x'))

uint_zero_or_positive: (all x:UInt. ((x = 0) or (0 < x)))

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