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)

auto zero_mult

nat_zero_mult: (all y:Nat. ℕ0 * lit(y) = ℕ0)

auto nat_zero_mult

auto mult_zero

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

auto lit_suc_mult

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

auto lit_mult_lit_suc

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

auto lit_mult_suc

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

auto one_mult

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

auto nat_one_mult

auto mult_one

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

auto nat_mult_one

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

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

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

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

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

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_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: (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))

mult_cancel_left_less: (all x:Nat, y:Nat, z:Nat. (if x * y < x * z 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_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)))

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

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

dist_mult_monus_one: (all x:Nat, y:Nat. x * (y ∸ suc(zero)) = x * y ∸ x)

n_le_nn: (all n:Nat. n ≤ n * n)

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

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

recfun operator /(n:Nat, m:Nat) -> Nat
measure	n  {
  if n < m then
    zero
  else
    if m = zero then
      zero
    else
      suc(zero) + (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)))

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

recfun div_alt(a:Nat, b:Nat, y:Nat) -> Pair<Nat,Nat>
measure	(a + b) + b  {
  if b = zero then
    pair(zero, a)
  else
    if (a = y and zero < a) then
      define f = div_alt(zero, b, y);
	pair(suc(first(f)), second(f))
    else
      div_alt(suc(a), b ∸ suc(zero), y)
}