define O_1 : (fn UInt -> UInt) = fun n:UInt {
      1
    }

define O_2n : (fn UInt -> UInt) = fun n:UInt {
      2 * n
    }

define O_2pow_n : (fn UInt -> UInt) = fun n:UInt {
      2 ^ n
    }

define O_log : (fn UInt -> UInt) = fun n:UInt {
      log(n)
    }

define O_n : (fn UInt -> UInt) = fun n:UInt {
      n
    }

define O_n2 : (fn UInt -> UInt) = fun n:UInt {
      n * n
    }

define O_n3 : (fn UInt -> UInt) = fun n:UInt {
      (n * n) * n
    }

O_n_eq_O_2n: O_n ≈ O_2n

define O_n_log_n : (fn UInt -> UInt) = fun 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: (all f:(fn UInt -> UInt), g:(fn UInt -> UInt). (if f ≲ g then f + g ≈ g))

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

define bigo_little_o : (fn ((fn UInt -> UInt), (fn UInt -> UInt)) -> bool) = fun 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)))))
    }

define bigo_little_omega : (fn ((fn UInt -> UInt), (fn UInt -> UInt)) -> bool) = fun 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_add_dominated: (all f:(fn UInt -> UInt). log(f) + f ≈ 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_add_dominated: (all k:UInt. (if 1 ≤ k then log(O_n) + fun n:UInt { n ^ k } ≈ fun n:UInt { n ^ k }))

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

define bigo_omega : (fn ((fn UInt -> UInt), (fn UInt -> UInt)) -> bool) = fun 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_add_dominated: (all a:UInt, b:UInt. (if a ≤ b then fun n:UInt { n ^ a } + fun n:UInt { n ^ b } ≈ fun n:UInt { n ^ b }))

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_summation_const_one: fun x:UInt { uint_summation(x, 0, fun i:UInt { 1 }) } ≈ O_n

bigo_summation_id: fun x:UInt { uint_summation(x, 0, fun i:UInt { i }) } ≈ O_n2

bigo_summation_pow: (all a:UInt. (if 2 ≤ a then fun x:UInt { uint_summation(x, 0, fun i:UInt { a ^ i }) } ≈ fun x:UInt { a ^ x }))

bigo_summation_pow2: fun x:UInt { uint_summation(x, 0, fun i:UInt { 2 ^ i }) } ≈ O_2pow_n

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

define log : (fn (fn UInt -> UInt) -> (fn UInt -> UInt)) = fun 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)))

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

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

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

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

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

define operator ≲ : (fn ((fn UInt -> UInt), (fn UInt -> UInt)) -> bool) = fun 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)
}

define positive : (fn (fn UInt -> UInt) -> bool) = fun 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)
}