fun O_1(n:UInt) {
  1
}

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

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

fun O_n(n:UInt) {
  n
}

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

O_n_eq_O_2n: O_n ≈ O_2n

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

bigo_const_mult: (all f:(fn UInt -> UInt), k:UInt. k * f ≲ 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_refl: (all f:(fn UInt -> UInt). f ≲ f)

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). log(f) + log(g) ≲ log(f * g))

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

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