union Option<T> {
  none
  just(T)
}

fun after<T, U>(o:Option<T>, f:(fn T -> U)) {
  switch o {
    case none {
      @none<U>
    }
    case just(x) {
      just(f(x))
    }
  }
}

fun default<T>(o:Option<T>, y:T) {
  switch o {
    case none {
      y
    }
    case just(x) {
      x
    }
  }
}

or_not: (all P:bool, Q:bool. (if ((P or Q) and not P) then Q))

ex_mid: (all b:bool. (b or not b))

or_sym: (all P:bool, Q:bool. (P or Q) = (Q or P))

and_sym: (all P:bool, Q:bool. (P and Q) = (Q and P))

eq_true: (all P:bool. (P ⇔ (P = true)))

eq_false: (all P:bool. (not P ⇔ (P = false)))

iff_equal: (all P:bool, Q:bool. (if (P ⇔ Q) then P = Q))

iff_symm: (all P:bool, Q:bool. (if (P ⇔ Q) then (Q ⇔ P)))

iff_trans: (all P:bool, Q:bool, R:bool. (if ((P ⇔ Q) and (Q ⇔ R)) then (P ⇔ R)))

contrapositive: (all P:bool, Q:bool. (if ((if P then Q) and not Q) then not P))

double_neg: (all P:bool. not not P = P)

fun xor(x:bool, y:bool) {
  if x then
    not y
  else
    y
}

xor_true: (all b:bool. xor(true, b) = not b)

xor_false: (all b:bool. xor(false, b) = b)

xor_commute: (all a:bool, b:bool. xor(a, b) = xor(b, a))

union Nat {
  zero
  suc(Nat)
}

recursive operator +(Nat,Nat) -> Nat{
  operator +(zero, m) = m
  operator +(suc(n), m) = suc(n + m)
}

recursive operator *(Nat,Nat) -> Nat{
  operator *(zero, m) = zero
  operator *(suc(n), m) = m + n * m
}

recursive expt(Nat,Nat) -> Nat{
  expt(zero, n) = suc(zero)
  expt(suc(p), n) = n * expt(p, n)
}

fun operator ^(a:Nat, b:Nat) {
  expt(b, a)
}

recursive max(Nat,Nat) -> Nat{
  max(zero, n) = n
  max(suc(m'), n) = 
    switch n {
      case zero {
        suc(m')
      }
      case suc(n') {
        suc(max(m', n'))
      }
    }
}

recursive min(Nat,Nat) -> Nat{
  min(zero, n) = zero
  min(suc(m'), n) = 
    switch n {
      case zero {
        zero
      }
      case suc(n') {
        suc(min(m', n'))
      }
    }
}

fun pred(n:Nat) {
  switch n {
    case zero {
      zero
    }
    case suc(n') {
      n'
    }
  }
}

recursive operator ∸(Nat,Nat) -> Nat{
  operator ∸(zero, m) = zero
  operator ∸(suc(n), m) = 
    switch m {
      case zero {
        suc(n)
      }
      case suc(m') {
        n ∸ m'
      }
    }
}

recursive operator ≤(Nat,Nat) -> bool{
  operator ≤(zero, m) = true
  operator ≤(suc(n'), m) = 
    switch m {
      case zero {
        false
      }
      case suc(m') {
        n' ≤ m'
      }
    }
}

fun operator <(x:Nat, y:Nat) {
  suc(x) ≤ y
}

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

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

recursive summation(Nat,Nat,(fn Nat -> Nat)) -> Nat{
  summation(zero, begin, f) = zero
  summation(suc(k), begin, f) = f(begin) + summation(k, suc(begin), f)
}

recursive iterate<T>(Nat,T,(fn T -> T)) -> T{
  iterate(zero, init, f) = init
  iterate(suc(n), init, f) = f(@iterate<T>(n, init, f))
}

recursive pow2(Nat) -> Nat{
  pow2(zero) = suc(zero)
  pow2(suc(n')) = suc(suc(zero)) * pow2(n')
}

recursive equal(Nat,Nat) -> bool{
  equal(zero, n) = 
    switch n {
      case zero {
        true
      }
      case suc(n') {
        false
      }
    }
  equal(suc(m'), n) = 
    switch n {
      case zero {
        false
      }
      case suc(n') {
        equal(m', n')
      }
    }
}

recursive dist(Nat,Nat) -> Nat{
  dist(zero, n) = n
  dist(suc(m), n) = 
    switch n {
      case zero {
        suc(m)
      }
      case suc(n') {
        dist(m, n')
      }
    }
}

fun log(n) {
  find_log(n, zero, zero)
}

fun lit(a:Nat) {
  a
}

lit_idem: (all x:Nat. lit(lit(x)) = lit(x))

auto lit_idem

suc_lit: (all n:Nat. suc(lit(n)) = lit(suc(n)))

auto suc_lit

auto zero_add

nat_zero_add: (all y:Nat. ℕ0 + y = y)

auto nat_zero_add

auto add_zero

nat_add_zero: (all x:Nat. x + ℕ0 = x)

auto nat_add_zero

lit_suc_add: (all x:Nat, y:Nat. lit(suc(x)) + lit(y) = lit(suc(lit(x) + lit(y))))

auto lit_suc_add

add_commute: (all n:Nat. (all m:Nat. n + m = m + n))

add_assoc: (all m:Nat, n:Nat, o:Nat. (m + n) + o = m + (n + o))

assoc_add: (all m:Nat, n:Nat, o:Nat. m + (n + o) = (m + n) + o)

add_both_sides_of_equal: (all x:Nat. (all y:Nat, z:Nat. ((x + y = x + z) ⇔ (y = z))))

left_cancel: (all x:Nat. (all y:Nat, z:Nat. (if x + y = x + z then y = z)))

add_both_monus: (all z:Nat, y:Nat, x:Nat. (z + y) ∸ (z + x) = y ∸ x)

add_monus_identity: (all m:Nat. (all n:Nat. (m + n) ∸ m = n))

monus_monus_eq_monus_add: (all x:Nat. (all y:Nat. (all z:Nat. (x ∸ y) ∸ z = x ∸ (y + z))))

monus_order: (all x:Nat, y:Nat, z:Nat. (x ∸ y) ∸ z = (x ∸ z) ∸ y)