import Option

import Base

union Nat {
  zero
  suc(Nat)
}

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

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

recursive expt(Nat,Nat) -> Nat{
  expt(ℕ0, n) = ℕ1
  expt(suc(p), n) = n * expt(p, n)
}

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

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

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

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

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

recursive operator ≤(Nat,Nat) -> bool{
  operator ≤(ℕ0, m) = true
  operator ≤(suc(n'), m) = 
    switch m {
      case ℕ0 {
        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(ℕ0, begin, f) = ℕ0
  summation(suc(k), begin, f) = f(begin) + summation(k, suc(begin), f)
}

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

recursive pow2(Nat) -> Nat{
  pow2(ℕ0) = ℕ1
  pow2(suc(n')) = ℕ2 * pow2(n')
}

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

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

zero_add: (all n:Nat. ℕ0 + n = n)

add_zero: (all n:Nat. n + ℕ0 = n)

suc_add: (all m:Nat, n:Nat. suc(m) + n = suc(m + n))

suc_one_add: (all n:Nat. suc(n) = ℕ1 + n)

one_add_suc: (all n:Nat. ℕ1 + n = suc(n))

not_one_add_zero: (all n:Nat. not (ℕ1 + n = ℕ0))

add_suc: (all m:Nat. (all n:Nat. m + suc(n) = suc(m + n)))

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

one_add: (all m:Nat. ℕ1 + m = suc(m))

add_one: (all m:Nat. m + ℕ1 = suc(m))

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_to_zero: (all n:Nat. (all m:Nat. (if n + m = ℕ0 then (n = ℕ0 and m = ℕ0))))

zero_monus: (all x:Nat. ℕ0  x = ℕ0)

monus_cancel: (all n:Nat. n  n = ℕ0)

monus_zero: (all n:Nat. n  ℕ0 = n)

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

pred_one: pred(ℕ1) = ℕ0

pred_suc_n: (all n:Nat. pred(suc(n)) = n)

monus_one_pred: (all x:Nat. x  ℕ1 = pred(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)

zero_mult: (all n:Nat. ℕ0 * n = ℕ0)

mult_zero: (all n:Nat. n * ℕ0 = ℕ0)

suc_mult: (all m:Nat, n:Nat. suc(m) * n = n + m * n)

mult_suc: (all m:Nat. (all n:Nat. m * suc(n) = m + m * n))

mult_commute: (all m:Nat. (all n:Nat. m * n = n * m))

one_mult: (all n:Nat. ℕ1 * n = n)

mult_one: (all n:Nat. n * ℕ1 = n)

mult_to_zero: (all n:Nat, m:Nat. (if m * n = ℕ0 then (m = ℕ0 or n = ℕ0)))

one_mult_one: (all x:Nat, y:Nat. (if x * y = ℕ1 then (x = ℕ1 and y = ℕ1)))

two_mult: (all n:Nat. ℕ2 * n = n + n)

dist_mult_add: (all a:Nat, x:Nat, y:Nat. a * (x + y) = a * x + a * y)

dist_mult_add_right: (all x:Nat, y:Nat, a:Nat. (x + y) * a = x * a + y * a)

mult_assoc: (all m:Nat. (all n:Nat, o:Nat. (m * n) * o = m * (n * o)))

mult_right_cancel: (all m:Nat, n:Nat, o:Nat. (if m * suc(o) = n * suc(o) then m = n))

mult_left_cancel: (all m:Nat, a:Nat, b:Nat. (if suc(m) * a = suc(m) * b then a = b))

suc_less_equal_iff_less_equal_suc: (all x:Nat, y:Nat. ((x  y)  (suc(x)  suc(y))))

less_suc_iff_suc_less: (all x:Nat, y:Nat. ((x < y)  (suc(x) < suc(y))))

not_less_zero: (all x:Nat. not (x < ℕ0))

less_equal_implies_less_or_equal: (all x:Nat. (all y:Nat. (if x  y then (x < y or x = y))))

less_equal_not_equal_implies_less: (all x:Nat, y:Nat. (if (x  y and not (x = y)) then x < y))

less_implies_less_equal: (all x:Nat. (all y:Nat. (if x < y then x  y)))

less_equal_refl: (all n:Nat. n  n)

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

less_equal_antisymmetric: (all x:Nat. (all y:Nat. (if (x  y and y  x) then x = y)))

less_equal_trans: (all m:Nat. (all n:Nat, o:Nat. (if (m  n and n  o) then m  o)))

not_less_implies_less_equal: (all x:Nat. (all y:Nat. (if not (x < y) then y  x)))

less_irreflexive: (all x:Nat. not (x < x))

less_not_equal: (all x:Nat, y:Nat. (if x < y then not (x = y)))

greater_not_equal: (all x:Nat, y:Nat. (if x > y then not (x = y)))

trichotomy: (all x:Nat. (all y:Nat. (x < y or x = y or y < x)))

trichotomy2: (all y:Nat, x:Nat. (if (not (x = y) and not (x < y)) then y < x))

dichotomy: (all x:Nat, y:Nat. (x  y or y < x))

zero_or_positive: (all x:Nat. (x = ℕ0 or ℕ0 < x))

zero_le_zero: (all x:Nat. (if x  ℕ0 then x = ℕ0))

not_less_equal_iff_greater: (all x:Nat, y:Nat. (not (x  y)  (y < x)))

less_implies_not_greater: (all x:Nat. (all y:Nat. (if x < y then not (y < x))))

not_less_equal_less_equal: (all x:Nat, y:Nat. (if not (x  y) then y  x))

not_zero_suc: (all n:Nat. (if not (n = ℕ0) then some n':Nat. n = suc(n')))

positive_suc: (all n:Nat. (if ℕ0 < n then some n':Nat. n = suc(n')))

less_equal_add: (all x:Nat. (all y:Nat. x  x + y))

less_add_pos: (all x:Nat, y:Nat. (if ℕ0 < y then x < x + y))

less_equal_add_left: (all x:Nat, y:Nat. y  x + y)

less_equal_suc: (all n:Nat. n  suc(n))

less_suc: (all n:Nat. n < suc(n))

add_mono: (all a:Nat, b:Nat, c:Nat, d:Nat. (if (a  c and b  d) then a + b  c + d))

add_mono_less: (all a:Nat, b:Nat, c:Nat, d:Nat. (if (a < c and b < d) then a + b < c + d))

add_pos_nonneg: (all a:Nat, b:Nat. (if ℕ0 < a then ℕ0 < a + b))

zero_less_one_add: (all n:Nat. ℕ0 < ℕ1 + n)

add_both_sides_of_less_equal: (all x:Nat. (all y:Nat, z:Nat. ((x + y  x + z)  (y  z))))

add_both_sides_of_less: (all x:Nat, y:Nat, z:Nat. ((x + y < x + z)  (y < z)))

mult_mono_le_nonzero: (all x:Nat, y:Nat, n:Nat. (if x * suc(n)  y * suc(n) then x  y))

mult_nonzero_mono_le: (all n:Nat, x:Nat, y:Nat. (if suc(n) * x  suc(n) * y then x  y))

mono_nonzero_mult_le: (all n:Nat, x:Nat, y:Nat. (if x < y then suc(n) * x < suc(n) * y))

mult_mono_le: (all n:Nat. (all x:Nat, y:Nat. (if x  y then n * x  n * y)))

mult_mono_le_r: (all n:Nat. (all x:Nat, y:Nat. (if x  y then x * n  y * n)))

mult_cancel_right_less: (all x:Nat, y:Nat, z:Nat. (if y * x < z * x then y < z))

monus_add_assoc: (all n:Nat. (all l:Nat, m:Nat. (if m  n then l + (n  m) = (l + n)  m)))

monus_suc_identity: (all n:Nat. (if ℕ0 < n then suc(n  ℕ1) = n))

monus_add_identity: (all n:Nat. (all m:Nat. (if m  n then m + (n  m) = n)))

monus_right_cancel: (all x:Nat, y:Nat, a:Nat. (if (x  a = y  a and a  x and a  y) then x = y))

less_equal_add_monus: (all m:Nat. (all n:Nat, o:Nat. (if (n  m and m  n + o) then m  n  o)))

monus_zero_iff_less_eq: (all x:Nat, y:Nat. ((x  y)  (x  y = ℕ0)))

monus_pos_iff_less: (all x:Nat, y:Nat. ((y < x)  (ℕ0 < x  y)))

le_exists_monus: (all n:Nat, m:Nat. (if n  m then some x:Nat. m = n + x))

less_trans: (all m:Nat, n:Nat, o:Nat. (if (m < n and n < o) then m < o))

greater_any_zero: (all x:Nat, y:Nat. (if x < y then ℕ0 < y))

dist_mult_monus: (all x:Nat. (all y:Nat, z:Nat. x * (y  z) = x * y  x * z))

mult_pos_nonneg: (all a:Nat, b:Nat. (if (ℕ0 < a and ℕ0 < b) then ℕ0 < a * b))

mult_lt_mono_l: (all c:Nat, a:Nat, b:Nat. (if c > ℕ0 then (if a < b then a * c < b * c)))

mult_lt_mono_r: (all c:Nat, a:Nat, b:Nat. (if ℕ0 < c then (if a * c < b * c then a < b)))

max_greater_right: (all y:Nat, x:Nat. y  max(x, y))

max_greater_left: (all x:Nat, y:Nat. x  max(x, y))

max_is_left_or_right: (all x:Nat, y:Nat. (max(x, y) = x or max(x, y) = y))

zero_max: (all x:Nat. max(ℕ0, x) = x)

max_zero: (all x:Nat. max(x, ℕ0) = x)

max_symmetric: (all x:Nat, y:Nat. max(x, y) = max(y, x))

max_assoc: (all x:Nat, y:Nat, z:Nat. max(max(x, y), z) = max(x, max(y, z)))

max_equal_greater_right: (all x:Nat, y:Nat. (if x  y then max(x, y) = y))

max_equal_greater_left: (all x:Nat, y:Nat. (if y  x then max(x, y) = x))

max_less_equal: (all x:Nat, y:Nat, z:Nat. (if (x  z and y  z) then max(x, y)  z))

recursive parity(Nat,bool) -> bool{
  parity(ℕ0, b) = b
  parity(suc(n'), b) = parity(n', not b)
}

fun is_even(n:Nat) {
  parity(n, true)
}

fun is_odd(n:Nat) {
  parity(n, false)
}

fun EvenNat(n:Nat) {
  some m:Nat. n = ℕ2 * m
}

fun OddNat(n:Nat) {
  some m:Nat. n = suc(ℕ2 * m)
}

two_even: (all n:Nat. EvenNat(ℕ2 * n))

one_two_odd: (all n:Nat. OddNat(ℕ1 + ℕ2 * n))

even_or_odd: (all n:Nat. (is_even(n) or is_odd(n)))

addition_of_evens: (all x:Nat, y:Nat. (if (EvenNat(x) and EvenNat(y)) then EvenNat(x + y)))

is_even_odd: (all n:Nat. ((if is_even(n) then EvenNat(n)) and (if is_odd(n) then OddNat(n))))

Even_or_Odd: (all n:Nat. (EvenNat(n) or OddNat(n)))

odd_one_even: (all n:Nat. (if OddNat(ℕ1 + n) then EvenNat(n)))

even_one_odd: (all n:Nat. (if EvenNat(ℕ1 + n) then OddNat(n)))

Even_not_Odd: (all n:Nat. (EvenNat(n)  not OddNat(n)))

summation_cong: (all k:Nat. (all f:(fn Nat -> Nat), g:(fn Nat -> Nat), s:Nat, t:Nat. (if (all i:Nat. (if i < k then f(s + i) = g(t + i))) then summation(k, s, f) = summation(k, t, g))))

summation_suc: (all k:Nat. (all f:(fn Nat -> Nat), g:(fn Nat -> Nat), s:Nat. (if (all i:Nat. f(i) = g(suc(i))) then summation(k, s, f) = summation(k, suc(s), g))))

summation_add: (all a:Nat. (all b:Nat, s:Nat, t:Nat, f:(fn Nat -> Nat), g:(fn Nat -> Nat), h:(fn Nat -> Nat). (if ((all i:Nat. (if i < a then g(s + i) = f(s + i))) and (all i:Nat. (if i < b then h(t + i) = f((s + a) + i)))) then summation(a + b, s, f) = summation(a, s, g) + summation(b, t, h))))

summation_next: (all n:Nat, s:Nat, f:(fn Nat -> Nat). summation(ℕ1 + n, s, f) = summation(n, s, f) + f(s + n))

equal_refl: (all n:Nat. equal(n, n))

equal_complete_sound: (all m:Nat. (all n:Nat. ((m = n)  equal(m, n))))

not_equal_not_eq: (all m:Nat, n:Nat. (if not equal(m, n) then not (m = n)))

pow_positive: (all n:Nat. ℕ0 < pow2(n))

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

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

strong_induction: (all P:(fn Nat -> bool), n:Nat. (if (all j:Nat. (if (all i:Nat. (if i < j then P(i))) then P(j))) then P(n)))

div_mod: (all n:Nat, m:Nat. (if ℕ0 < m then (n / m) * m + n % m = n))

mod_less_divisor: (all n:Nat, m:Nat. (if ℕ0 < m then n % m < m))

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

divides_mod: (all d:Nat, m:Nat, n:Nat. (if (divides(d, n) and divides(d, m % n) and ℕ0 < n) then divides(d, m)))

div_cancel: (all y:Nat. (if ℕ0 < y then y / y = ℕ1))

mod_self_zero: (all y:Nat. y % y = ℕ0)

zero_mod: (all x:Nat. ℕ0 % x = ℕ0)

zero_div: (all x:Nat. (if ℕ0 < x then ℕ0 / x = ℕ0))

mod_one: (all n:Nat. n % ℕ1 = ℕ0)

div_one: (all n:Nat. n / ℕ1 = n)

add_div_one: (all n:Nat, m:Nat. (if ℕ0 < m then (n + m) / m = ℕ1 + n / m))

mult_div_inverse: (all n:Nat, m:Nat. (if ℕ0 < m then (n * m) / m = n))

expt_one: (all n:Nat. n ^ ℕ1 = n)

one_expt: (all n:Nat. ℕ1 ^ n = ℕ1)

pow_add_r: (all n:Nat, m:Nat, o:Nat. m ^ (n + o) = m ^ n * m ^ o)

pow_mul_l: (all o:Nat, m:Nat, n:Nat. (m * n) ^ o = m ^ o * n ^ o)

pow_mul_r: (all o:Nat, m:Nat, n:Nat. (m ^ n) ^ o = m ^ (n * o))

pow_pos_nonneg: (all b:Nat, a:Nat. (if ℕ0 < a then ℕ0 < a ^ b))

pow_zero_l: (all a:Nat. (if ℕ0 < a then ℕ0 ^ a = ℕ0))

pow_eq_zero: (all n:Nat, m:Nat. (if m ^ n = ℕ0 then m = ℕ0))

exp_one_implies_zero_or_one: (all m:Nat, n:Nat. (if m ^ n = ℕ1 then (n = ℕ0 or m = ℕ1)))

pow_lt_mono_l: (all c:Nat, a:Nat, b:Nat. (if ℕ0 < c then (if a < b then a ^ c < b ^ c)))

pow_gt_1: (all n:Nat, m:Nat. (if ℕ1 < n then ((ℕ0 < m)  (ℕ1 < n ^ m))))

pow_le_mono_l: (all c:Nat, a:Nat, b:Nat. (if a  b then a ^ c  b ^ c))

pow_lt_mono_r: (all c:Nat, a:Nat, b:Nat. (if ℕ1 < a then (if b < c then a ^ b < a ^ c)))

pow_inj_l: (all a:Nat, b:Nat, c:Nat. (if ℕ0 < c then (if a ^ c = b ^ c then a = b)))

pow_inj_r: (all a:Nat, b:Nat, c:Nat. (if ℕ1 < a then (if a ^ b = a ^ c then b = c)))

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

gcd_divides: (all b:Nat, a:Nat. (divides(gcd(a, b), a) and divides(gcd(a, b), b)))