fun O_1(n:UInt) {
  1
}

fun O_2n(n:UInt) {
  2 * n
}

fun O_2pow_n(n:UInt) {
  2 ^ n
}

fun O_log(n:UInt) {
  log(n)
}

fun O_n(n:UInt) {
  n
}

fun O_n2(n:UInt) {
  n * n
}

fun O_n3(n:UInt) {
  (n * n) * n
}

O_n_eq_O_2n: O_n ≈ O_2n

fun O_n_log_n(n:UInt) {
  n * log(n)
}

bigo_add: (all f:(fn UInt -> UInt). f + f ≲ f)

bigo_add_absorb: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt). (if g ≲ f then f + g ≲ f))

bigo_add_assoc: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt), h:(fn UInt -> UInt). (f + g) + h ≈ f + (g + h))

bigo_add_commute: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt). f + g ≈ g + f)

bigo_add_dominated_absorb_equiv: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt). (if g ≲ f then f + g ≈ f))

bigo_add_le_max: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt). f + g ≲ max(f, g))

bigo_add_mono: (all f1:(fn UInt -> UInt), f2:(fn UInt -> UInt), g1:(fn UInt -> UInt), g2:(fn UInt -> UInt). (if ((f1 ≲ g1) and (f2 ≲ g2)) then f1 + f2 ≲ g1 + g2))

bigo_add_zero: (all f:(fn UInt -> UInt). f + fun n:UInt { 0 } ≈ f)

bigo_const_func_le_O_1: (all c:UInt. fun n:UInt { c } ≲ O_1)

bigo_const_mult: (all f:(fn UInt -> UInt), k:UInt. k * f ≲ f)

bigo_const_mult_equiv: (all f:(fn UInt -> UInt), k:UInt. (if 0 < k then k * f ≈ f))

bigo_cubic_closure: (all a:UInt, b:UInt, c:UInt, d:UInt. (if 1 ≤ a then fun n:UInt { ((((a * n) * n) * n + (b * n) * n) + c * n) + d } ≈ fun n:UInt { (n * n) * n }))

bigo_cubic_le_2pow_n: O_n3 ≲ O_2pow_n

bigo_dist: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt), h:(fn UInt -> UInt). f * (g + h) ≈ f * g + f * h)

bigo_equiv_iff_theta: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt). ((f ≈ g) ⇔ ((f ≲ g) and bigo_omega(f, g))))

bigo_equiv_refl: (all f:(fn UInt -> UInt). f ≈ f)

bigo_equiv_sym: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt). (if f ≈ g then g ≈ f))

bigo_equiv_trans: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt), h:(fn UInt -> UInt). (if ((f ≈ g) and (g ≈ h)) then f ≈ h))

bigo_le_add_self: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt). g ≲ f + g)

bigo_le_const_mult: (all f:(fn UInt -> UInt), k:UInt. (if 1 ≤ k then f ≲ k * f))

bigo_linear_closure: (all a:UInt, b:UInt. (if 1 ≤ a then fun n:UInt { a * n + b } ≈ fun n:UInt { n }))

bigo_linear_le_2pow_n: O_n ≲ O_2pow_n

bigo_linear_le_n_log_n: O_n ≲ O_n_log_n

bigo_little_implies_big: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt). (if bigo_little_o(f, g) then f ≲ g))

bigo_little_irrefl: (all f:(fn UInt -> UInt). not bigo_little_o(f, f))

fun bigo_little_o(f:(fn UInt -> UInt), g:(fn UInt -> UInt)) {
  (all c:UInt. (if 0 < c then some n0:UInt. (all n:UInt. (if n0 ≤ n then c * f(n) < g(n)))))
}

fun bigo_little_omega(f:(fn UInt -> UInt), g:(fn UInt -> UInt)) {
  bigo_little_o(g, f)
}

bigo_little_omega_implies_big_omega: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt). (if bigo_little_omega(f, g) then bigo_omega(f, g)))

bigo_little_omega_irrefl: (all f:(fn UInt -> UInt). not bigo_little_omega(f, f))

bigo_little_omega_swap: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt). (if bigo_little_omega(f, g) then bigo_little_o(g, f)))

bigo_log_const: log(O_1) ≲ O_1

bigo_log_le_self: (all f:(fn UInt -> UInt). log(f) ≲ f)

bigo_log_log: log(O_log) ≲ O_log

bigo_log_pow: (all k:UInt. (if 1 ≤ k then log(fun n:UInt { n ^ k }) ≈ log(O_n)))

bigo_log_pow_le: (all k:UInt. (if 1 ≤ k then log(fun n:UInt { n ^ k }) ≲ log(O_n)))

bigo_max_le_add: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt). max(f, g) ≲ f + g)

bigo_mult_assoc: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt), h:(fn UInt -> UInt). (f * g) * h ≈ f * (g * h))

bigo_mult_commute: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt). f * g ≈ g * f)

bigo_mult_mono: (all f1:(fn UInt -> UInt), f2:(fn UInt -> UInt), g1:(fn UInt -> UInt), g2:(fn UInt -> UInt). (if ((f1 ≲ g1) and (f2 ≲ g2)) then f1 * f2 ≲ g1 * g2))

bigo_mult_one_func: (all f:(fn UInt -> UInt). f * fun n:UInt { 1 } ≈ f)

bigo_n_log_n_le_quadratic: O_n_log_n ≲ O_n2

fun bigo_omega(f:(fn UInt -> UInt), g:(fn UInt -> UInt)) {
  g ≲ f
}

bigo_omega_refl: (all f:(fn UInt -> UInt). bigo_omega(f, f))

bigo_omega_trans: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt), h:(fn UInt -> UInt). (if (bigo_omega(f, g) and bigo_omega(g, h)) then bigo_omega(f, h)))

bigo_pointwise_eq: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt). (if (all n:UInt. f(n) = g(n)) then f ≈ g))

bigo_pointwise_le: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt). (if (all n:UInt. f(n) ≤ g(n)) then f ≲ g))

bigo_poly_closure: (all pre:List<UInt>, a:UInt. (if 1 ≤ a then fun n:UInt { poly_eval(pre ++ [a], n) } ≈ fun n:UInt { n ^ length(pre) }))

bigo_pow_mono: (all a:UInt, b:UInt. (if a ≤ b then fun n:UInt { n ^ a } ≲ fun n:UInt { n ^ b }))

bigo_pow_strict_mono: (all a:UInt, b:UInt. (if a < b then bigo_little_o(fun n:UInt { n ^ a }, fun n:UInt { n ^ b })))

bigo_quadratic_closure: (all a:UInt, b:UInt, c:UInt. (if 1 ≤ a then fun n:UInt { ((a * n) * n + b * n) + c } ≈ fun n:UInt { n * n }))

bigo_quadratic_le_2pow_n: O_n2 ≲ O_2pow_n

bigo_quadratic_le_cubic: O_n2 ≲ O_n3

bigo_refl: (all f:(fn UInt -> UInt). f ≲ f)

bigo_self_le_add: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt). f ≲ f + g)

bigo_trans: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt), h:(fn UInt -> UInt). (if ((f ≲ g) and (g ≲ h)) then f ≲ h))

constant_le_log: O_1 ≲ O_log

linear_le_quadratic: O_n ≲ O_n2

fun log(f:(fn UInt -> UInt)) {
  fun x:UInt {
    log(f(x))
  }
}

log_le_linear: O_log ≲ O_n

log_product_equiv_sum: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt). (if ((all n:UInt. 1 < f(n)) and (all n:UInt. 1 < g(n))) then log(f * g) ≈ log(f) + log(g)))

log_product_less_equal_sum: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt). (if ((all n:UInt. 1 < f(n)) and (all n:UInt. 1 < g(n))) then log(f * g) ≲ log(f) + log(g)))

log_sum_less_equal_product: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt). (if ((all n:UInt. 0 < f(n)) and (all n:UInt. 0 < g(n))) then log(f) + log(g) ≲ log(f * g)))

fun max(f:(fn UInt -> UInt), g:(fn UInt -> UInt)) {
  fun n:UInt {
    max(f(n), g(n))
  }
}

fun operator *(f:(fn UInt -> UInt), g:(fn UInt -> UInt)) {
  fun x:UInt {
    f(x) * g(x)
  }
}

fun operator *(k:UInt, g:(fn UInt -> UInt)) {
  fun x:UInt {
    k * g(x)
  }
}

fun operator +(f:(fn UInt -> UInt), g:(fn UInt -> UInt)) {
  fun x:UInt {
    f(x) + g(x)
  }
}

fun operator ≈(f:(fn UInt -> UInt), g:(fn UInt -> UInt)) {
  ((f ≲ g) and (g ≲ f))
}

fun operator ≲(f:(fn UInt -> UInt), g:(fn UInt -> UInt)) {
  some n0:UInt,c:UInt. (all n:UInt. (if n0 ≤ n then f(n) ≤ c * g(n)))
}

recursive poly_eval(List<UInt>,UInt) -> UInt{
  poly_eval([], n) = 0
  poly_eval(node(a, rest), n) = a + n * poly_eval(rest, n)
}

fun positive(f:(fn UInt -> UInt)) {
  (all n:UInt. 0 < f(n))
}

recursive sum_coeffs(List<UInt>) -> UInt{
  sum_coeffs([]) = 0
  sum_coeffs(node(a, rest)) = a + sum_coeffs(rest)
}