define Even : (fn Int -> bool) = fun n:Int {
      some m:Int. n = +2 * m
    }

union Int {
  pos(UInt)
  negsuc(UInt)
}

define Odd : (fn Int -> bool) = fun n:Int {
      some m:Int. n = +1 + +2 * m
    }

opaque define abs : (fn Int -> UInt) = fun x:Int {
      switch x {
        case pos(n) {
          n
        }
        case negsuc(n) {
          1 + n
        }
      }
    }

auto abs_lit

abs_lit: (all x:Nat. abs(pos(fromNat(lit(x)))) = fromNat(lit(x)))

abs_neg: (all n:Int. abs(- n) = abs(n))

add_commute_uint_int: (all x:UInt, y:Int. x + y = y + x)

dist_neg_mult: (all x:Int, y:Int. - (x * y) = - x * y)

auto div_negsuc_negsuc

div_negsuc_negsuc: (all au:UInt, bu:UInt. negsuc(au) / negsuc(bu) = pos((1 + au) / (1 + bu)))

auto div_negsuc_pos

div_negsuc_pos: (all au:UInt, bu:UInt. negsuc(au) / pos(bu) = - pos((1 + au) / bu))

auto div_negsuc_uint

div_negsuc_uint: (all au:UInt, bu:UInt. negsuc(au) / bu = - pos((1 + au) / bu))

auto div_pos_negsuc

div_pos_negsuc: (all au:UInt, bu:UInt. pos(au) / negsuc(bu) = - pos(au / (1 + bu)))

auto div_pos_pos

div_pos_pos: (all au:UInt, bu:UInt. pos(au) / pos(bu) = pos(au / bu))

auto div_pos_uint

div_pos_uint: (all au:UInt, bu:UInt. pos(au) / bu = pos(au / bu))

define divides : (fn (Int, Int) -> bool) = fun a:Int, b:Int {
      some k:Int. a * k = b
    }

define gcd : (fn (Int, Int) -> Int) = fun a:Int, b:Int {
      pos(gcd(abs(a), abs(b)))
    }

int_Even_iff_abs_Even: (all x:Int. (Even(x) ⇔ Even(abs(x))))

int_Even_not_Odd: (all n:Int. (Even(n) ⇔ (not Odd(n))))

int_Even_or_Odd: (all n:Int. (Even(n) or Odd(n)))

int_Odd_iff_abs_Odd: (all x:Int. (Odd(x) ⇔ Odd(abs(x))))

int_abs_pow: (all n:Int, k:UInt. abs(n ^ k) = abs(n) ^ k)

int_add_assoc: (all x:Int, y:Int, z:Int. (x + y) + z = x + (y + z))

int_add_both_sides_of_equal: (all x:Int, y:Int, z:Int. (if x + y = x + z then y = z))

int_add_both_sides_of_equal_iff: (all x:Int, y:Int, z:Int. ((x + y = x + z) ⇔ (y = z)))

int_add_both_sides_of_equal_right: (all x:Int, y:Int, z:Int. (if y + x = z + x then y = z))

int_add_commute: (all x:Int, y:Int. x + y = y + x)

int_add_inverse: (all x:Int. x + - x = +0)

int_add_left_inverse: (all x:Int. - x + x = +0)

int_add_sub_cancel: (all x:Int, y:Int. (x + y) - y = x)

auto int_add_zero

int_add_zero: (all n:Int. n + +0 = n)

int_dist_mult_add: (all a:Int, x:Int, y:Int. a * (x + y) = a * x + a * y)

int_dist_mult_add_right: (all a:Int, x:Int, y:Int. (x + y) * a = x * a + y * a)

int_dist_mult_sub: (all a:Int, x:Int, y:Int. a * (x - y) = a * x - a * y)

int_divides_add: (all d:Int, m:Int, n:Int. (if (divides(d, m) and divides(d, n)) then divides(d, m + n)))

int_divides_iff_abs: (all a:Int, b:Int. (divides(a, b) ⇔ divides(abs(a), abs(b))))

int_divides_mult_left: (all d:Int, n:Int, m:Int. (if divides(d, n) then divides(d, m * n)))

int_divides_mult_right: (all d:Int, n:Int, m:Int. (if divides(d, n) then divides(d, n * m)))

int_divides_neg_left: (all d:Int, n:Int. (if divides(d, n) then divides(- d, n)))

int_divides_neg_right: (all d:Int, n:Int. (if divides(d, n) then divides(d, - n)))

int_divides_refl: (all n:Int. divides(n, n))

int_divides_sub: (all d:Int, m:Int, n:Int. (if (divides(d, m) and divides(d, n)) then divides(d, m - n)))

int_divides_trans: (all a:Int, b:Int, c:Int. (if (divides(a, b) and divides(b, c)) then divides(a, c)))

int_divides_zero: (all n:Int. divides(n, +0))

int_even_add_even: (all x:Int, y:Int. (if (Even(x) and Even(y)) then Even(x + y)))

int_even_add_odd: (all x:Int, y:Int. (if (Even(x) and Odd(y)) then Odd(x + y)))

int_even_mult_left: (all x:Int, y:Int. (if Even(x) then Even(x * y)))

int_even_mult_right: (all x:Int, y:Int. (if Even(y) then Even(x * y)))

int_even_neg: (all x:Int. (Even(x) ⇔ Even(- x)))

int_even_one_odd: (all n:Int. (if Even(+1 + n) then Odd(n)))

int_gcd_divides_left: (all a:Int, b:Int. divides(gcd(a, b), a))

int_gcd_divides_right: (all a:Int, b:Int. divides(gcd(a, b), b))

int_gcd_greatest: (all d:Int, a:Int, b:Int. (if (divides(d, a) and divides(d, b)) then divides(d, gcd(a, b))))

int_lcm_zero_left: (all b:Int. lcm(+0, b) = +0)

int_lcm_zero_right: (all a:Int. lcm(a, +0) = +0)

int_less_iff_diff_pos: (all a:Int, b:Int. ((a < b) ⇔ (+0 < b - a)))

int_mult_assoc: (all x:Int, y:Int, z:Int. (x * y) * z = x * (y * z))

int_mult_commute: (all x:Int, y:Int. x * y = y * x)

auto int_mult_one

int_mult_one: (all x:Int. x * +1 = x)

auto int_mult_zero

int_mult_zero: (all x:Int. x * +0 = +0)

int_neg_injective: (all x:Int, y:Int. (if - x = - y then x = y))

int_neg_mult_left_cancel_le: (all n:Int, x:Int, y:Int. (if ((n < +0) and (n * x ≤ n * y)) then y ≤ x))

int_neg_mult_left_cancel_less: (all n:Int, x:Int, y:Int. (if ((n < +0) and (n * x < n * y)) then y < x))

int_neg_mult_mono_less_left: (all n:Int, x:Int, y:Int. (if ((n < +0) and (x < y)) then n * y < n * x))

int_neg_mult_mono_less_right: (all n:Int, x:Int, y:Int. (if ((n < +0) and (x < y)) then y * n < x * n))

int_neg_mult_right: (all x:Int, y:Int. x * - y = - (x * y))

int_neg_mult_right_cancel_le: (all n:Int, x:Int, y:Int. (if ((n < +0) and (x * n ≤ y * n)) then y ≤ x))

int_neg_mult_right_cancel_less: (all n:Int, x:Int, y:Int. (if ((n < +0) and (x * n < y * n)) then y < x))

int_neg_one_pow_even: (all k:UInt. (if Even(k) then - +1 ^ k = +1))

int_neg_one_pow_odd: (all k:UInt. (if Odd(k) then - +1 ^ k = - +1))

int_negsuc_eq_pos_false: (all x:UInt, y:UInt. negsuc(x) ≠ pos(y))

int_negsuc_injective: (all x:UInt, y:UInt. (if negsuc(x) = negsuc(y) then x = y))

int_nonneg_mult_mono_le_left: (all n:Int, x:Int, y:Int. (if ((+0 ≤ n) and (x ≤ y)) then n * x ≤ n * y))

int_nonneg_mult_mono_le_right: (all n:Int, x:Int, y:Int. (if ((+0 ≤ n) and (x ≤ y)) then x * n ≤ y * n))

int_nonpos_mult_mono_le_left: (all n:Int, x:Int, y:Int. (if ((n ≤ +0) and (x ≤ y)) then n * y ≤ n * x))

int_nonpos_mult_mono_le_right: (all n:Int, x:Int, y:Int. (if ((n ≤ +0) and (x ≤ y)) then y * n ≤ x * n))

int_odd_add_even: (all x:Int, y:Int. (if (Odd(x) and Even(y)) then Odd(x + y)))

int_odd_add_odd: (all x:Int, y:Int. (if (Odd(x) and Odd(y)) then Even(x + y)))

int_odd_mult_odd: (all x:Int, y:Int. (if (Odd(x) and Odd(y)) then Odd(x * y)))

int_odd_neg: (all x:Int. (Odd(x) ⇔ Odd(- x)))

int_odd_one_even: (all n:Int. (if Odd(+1 + n) then Even(n)))

int_one_divides: (all n:Int. divides(+1, n))

auto int_one_mult

int_one_mult: (all x:Int. +1 * x = x)

auto int_one_pow

int_one_pow: (all k:UInt. +1 ^ k = +1)

int_one_two_odd: (all n:Int. Odd(+1 + +2 * n))

int_pos_eq_negsuc_false: (all x:UInt, y:UInt. pos(x) ≠ negsuc(y))

int_pos_injective: (all x:UInt, y:UInt. (if pos(x) = pos(y) then x = y))

int_pos_mult_left_cancel_le: (all n:Int, x:Int, y:Int. (if ((+0 < n) and (n * x ≤ n * y)) then x ≤ y))

int_pos_mult_left_cancel_less: (all n:Int, x:Int, y:Int. (if ((+0 < n) and (n * x < n * y)) then x < y))

int_pos_mult_mono_less_left: (all n:Int, x:Int, y:Int. (if ((+0 < n) and (x < y)) then n * x < n * y))

int_pos_mult_mono_less_right: (all n:Int, x:Int, y:Int. (if ((+0 < n) and (x < y)) then x * n < y * n))

int_pos_mult_right_cancel_le: (all n:Int, x:Int, y:Int. (if ((+0 < n) and (x * n ≤ y * n)) then x ≤ y))

int_pos_mult_right_cancel_less: (all n:Int, x:Int, y:Int. (if ((+0 < n) and (x * n < y * n)) then x < y))

int_pow_add: (all n:Int, j:UInt, k:UInt. n ^ (j + k) = n ^ j * n ^ k)

int_pow_eq_zero: (all n:Int, k:UInt. (if n ^ k = +0 then n = +0))

int_pow_mul_base: (all k:UInt, a:Int, b:Int. (a * b) ^ k = a ^ k * b ^ k)

int_pow_mul_exp: (all n:Int, j:UInt, k:UInt. n ^ (j * k) = (n ^ k) ^ j)

int_pow_neg_base_even: (all m:UInt, n:Int. - n ^ (2 * m) = n ^ (2 * m))

int_pow_neg_base_odd: (all m:UInt, n:Int. - n ^ (1 + 2 * m) = - (n ^ (1 + 2 * m)))

int_pow_neg_base_when_even: (all n:Int, k:UInt. (if Even(k) then - n ^ k = n ^ k))

int_pow_neg_base_when_odd: (all n:Int, k:UInt. (if Odd(k) then - n ^ k = - (n ^ k)))

int_pow_nonneg: (all n:Int, k:UInt. (if +0 ≤ n then +0 ≤ n ^ k))

int_pow_nonzero: (all n:Int, k:UInt. (if n ≠ +0 then n ^ k ≠ +0))

auto int_pow_one

int_pow_one: (all n:Int. n ^ 1 = n)

int_pow_one_add: (all n:Int, k:UInt. n ^ (1 + k) = n * n ^ k)

auto int_pow_pos

int_pow_pos: (all m:UInt, k:UInt. pos(m) ^ k = pos(m ^ k))

int_pow_pos_of_pos: (all n:Int, k:UInt. (if +0 < n then +0 < n ^ k))

int_pow_two: (all n:Int. n ^ 2 = n * n)

auto int_pow_zero

int_pow_zero: (all n:Int. n ^ 0 = +1)

int_sub_add_cancel: (all x:Int, y:Int. (x - y) + y = x)

int_sub_cancel: (all x:Int. x - x = +0)

define int_summation : (fn (UInt, UInt, (fn UInt -> Int)) -> Int) = fun k:UInt, begin:UInt, f:(fn UInt -> Int) {
      int_summation_nat(toNat(k), toNat(begin), f)
    }

int_summation_add: (all a:UInt. (all b:UInt, s:UInt, t:UInt, f:(fn UInt -> Int), g:(fn UInt -> Int), h:(fn UInt -> Int). (if ((all i:Nat. (if i < toNat(a) then g(s + fromNat(i)) = f(s + fromNat(i)))) and (all i:Nat. (if i < toNat(b) then h(t + fromNat(i)) = f((s + a) + fromNat(i))))) then int_summation(a + b, s, f) = int_summation(a, s, g) + int_summation(b, t, h))))

int_summation_add_pointwise: (all k:UInt, s:UInt, f:(fn UInt -> Int), g:(fn UInt -> Int). int_summation(k, s, fun i:UInt { f(i) + g(i) }) = int_summation(k, s, f) + int_summation(k, s, g))

int_summation_cong: (all k:UInt. (all f:(fn UInt -> Int), g:(fn UInt -> Int), s:UInt, t:UInt. (if (all i:Nat. (if i < toNat(k) then f(s + fromNat(i)) = g(t + fromNat(i)))) then int_summation(k, s, f) = int_summation(k, t, g))))

int_summation_const_zero: (all k:UInt, s:UInt. int_summation(k, s, fun i:UInt { +0 }) = +0)

recursive int_summation_nat(Nat,Nat,(fn UInt -> Int)) -> Int{
  int_summation_nat(zero, begin, f) = +0
  int_summation_nat(suc(k), begin, f) = f(fromNat(begin)) + int_summation_nat(k, suc(begin), f)
}

int_summation_neg: (all k:UInt, s:UInt, f:(fn UInt -> Int). int_summation(k, s, fun i:UInt { - f(i) }) = - int_summation(k, s, f))

int_summation_next: (all n:UInt, s:UInt, f:(fn UInt -> Int). int_summation(1 + n, s, f) = int_summation(n, s, f) + f(s + n))

int_summation_sub: (all k:UInt, s:UInt, f:(fn UInt -> Int), g:(fn UInt -> Int). int_summation(k, s, fun i:UInt { f(i) - g(i) }) = int_summation(k, s, f) - int_summation(k, s, g))

int_summation_zero: (all begin:UInt, f:(fn UInt -> Int). int_summation(0, begin, f) = +0)

int_two_even: (all n:Int. Even(+2 * n))

auto int_zero_add

int_zero_add: (all n:Int. +0 + n = n)

auto int_zero_mult

int_zero_mult: (all x:Int. +0 * x = +0)

int_zero_pow: (all k:UInt. (if 0 < k then +0 ^ k = +0))

define lcm : (fn (Int, Int) -> Int) = fun a:Int, b:Int {
      pos(lcm(abs(a), abs(b)))
    }

auto lit_add_lit_pos

lit_add_lit_pos: (all x:Nat, y:Nat. fromNat(lit(x)) + pos(fromNat(lit(y))) = pos(fromNat(lit(x) + lit(y))))

auto lit_add_negsuc_pos_suc

lit_add_negsuc_pos_suc: (all x:Nat, y:Nat. negsuc(fromNat(lit(suc(x)))) + pos(fromNat(lit(suc(y)))) = negsuc(fromNat(lit(x))) + pos(fromNat(lit(y))))

auto lit_add_negsuc_zero_pos_suc

lit_add_negsuc_zero_pos_suc: (all x:Nat, y:Nat. -1 + pos(fromNat(lit(suc(y)))) = pos(fromNat(lit(y))))

auto lit_add_pos_lit

lit_add_pos_lit: (all x:Nat, y:Nat. pos(fromNat(lit(x))) + fromNat(lit(y)) = pos(fromNat(lit(x) + lit(y))))

auto lit_add_pos_negsuc_suc

lit_add_pos_negsuc_suc: (all x:Nat, y:Nat. pos(fromNat(lit(suc(y)))) + negsuc(fromNat(lit(suc(x)))) = pos(fromNat(lit(y))) + negsuc(fromNat(lit(x))))

auto lit_add_pos_pos

lit_add_pos_pos: (all x:Nat, y:Nat. pos(fromNat(lit(x))) + pos(fromNat(lit(y))) = pos(fromNat(lit(x) + lit(y))))

auto lit_add_pos_suc_negsuc_zero

lit_add_pos_suc_negsuc_zero: (all x:Nat, y:Nat. pos(fromNat(lit(suc(y)))) + -1 = pos(fromNat(lit(y))))

define max : (fn (Int, Int) -> Int) = fun x:Int, y:Int {
      if x < y then
        y
      else
        x
    }

define min : (fn (Int, Int) -> Int) = fun x:Int, y:Int {
      if x < y then
        x
      else
        y
    }

auto mult_lit_neg_lit

mult_lit_neg_lit: (all x:Nat, y:Nat. fromNat(lit(x)) * negsuc(fromNat(lit(y))) = - pos(fromNat(lit(x)) + fromNat(lit(x)) * fromNat(lit(y))))

auto mult_lit_pos_lit

mult_lit_pos_lit: (all x:Nat, y:Nat. fromNat(lit(x)) * pos(fromNat(lit(y))) = pos(fromNat(lit(x) * lit(y))))

auto mult_neg_lit_lit

mult_neg_lit_lit: (all x:Nat, y:Nat. negsuc(fromNat(lit(x))) * fromNat(lit(y)) = - pos(fromNat(lit(y)) + fromNat(lit(y)) * fromNat(lit(x))))

auto mult_neg_lit_pos

mult_neg_lit_pos: (all x:Nat, y:Nat. negsuc(fromNat(lit(x))) * pos(fromNat(lit(y))) = - pos(fromNat(lit(y)) + fromNat(lit(y)) * fromNat(lit(x))))

auto mult_pos_lit_lit

mult_pos_lit_lit: (all x:Nat, y:Nat. pos(fromNat(lit(x))) * fromNat(lit(y)) = pos(fromNat(lit(x) * lit(y))))

auto mult_pos_lit_neg_lit

mult_pos_lit_neg_lit: (all x:Nat, y:Nat. pos(fromNat(lit(x))) * negsuc(fromNat(lit(y))) = - pos(fromNat(lit(x)) + fromNat(lit(x)) * fromNat(lit(y))))

auto mult_pos_lit_pos_lit

mult_pos_lit_pos_lit: (all x:Nat, y:Nat. pos(fromNat(lit(x))) * pos(fromNat(lit(y))) = pos(fromNat(lit(x) * lit(y))))

neg_distr_add: (all x:Int, y:Int. - (x + y) = - x + - y)

neg_involutive: (all n:Int. - (- n) = n)

auto neg_lit_suc

neg_lit_suc: (all x:Nat. - fromNat(lit(suc(x))) = negsuc(fromNat(lit(x))))

auto neg_lit_zero

neg_lit_zero: - +0 = +0

auto neg_negsuc_lit

neg_negsuc_lit: (all x:Nat. - negsuc(fromNat(lit(x))) = pos(fromNat(lit(suc(x)))))

auto neg_pos_lit_suc

neg_pos_lit_suc: (all x:Nat. - pos(fromNat(lit(suc(x)))) = negsuc(fromNat(lit(x))))

auto neg_uint_zero

neg_uint_zero: - 0 = +0

neg_zero: - +0 = +0

opaque define operator * : (fn (Int, Int) -> Int) = fun x:Int, y:Int {
      (sign(x) * sign(y)) * (abs(x) * abs(y))
    }

opaque define operator * : (fn (UInt, Int) -> Int) = fun n:UInt, m:Int {
      pos(n) * m
    }

opaque define operator * : (fn (Int, UInt) -> Int) = fun n:Int, m:UInt {
      n * pos(m)
    }

opaque define operator + : (fn (Int, Int) -> Int) = fun x:Int, m:Int {
      switch x {
        case pos(n) {
          switch m { case pos(n') { pos(n + n') } case negsuc(n') { n ⊝ (1 + n') } }
        }
        case negsuc(n) {
          switch m { case pos(n') { n' ⊝ (1 + n) } case negsuc(n') { negsuc((1 + n) + n') } }
        }
      }
    }

opaque define operator + : (fn (UInt, Int) -> Int) = fun n:UInt, m:Int {
      pos(n) + m
    }

opaque define operator + : (fn (Int, UInt) -> Int) = fun n:Int, m:UInt {
      n + pos(m)
    }

opaque define operator - : (fn Int -> Int) = fun x:Int {
      switch x {
        case pos(n) {
          (if n = 0 then +0 else negsuc(n ∸ 1))
        }
        case negsuc(n) {
          pos(1 + n)
        }
      }
    }

opaque define operator - : (fn UInt -> Int) = fun n:UInt {
      - pos(n)
    }

define operator - : (fn (Int, Int) -> Int) = fun n:Int, m:Int {
      n + - m
    }

opaque define operator - : (fn (UInt, Int) -> Int) = fun n:UInt, m:Int {
      pos(n) - m
    }

opaque define operator - : (fn (Int, UInt) -> Int) = fun n:Int, m:UInt {
      n - pos(m)
    }

opaque define operator - : (fn (UInt, UInt) -> Int) = fun x:UInt, y:UInt {
      pos(x) - pos(y)
    }

opaque define operator / : (fn (Int, Int) -> Int) = fun n:Int, m:Int {
      (sign(n) * sign(m)) * (abs(n) / abs(m))
    }

opaque define operator / : (fn (Int, UInt) -> Int) = fun n:Int, m:UInt {
      sign(n) * (abs(n) / m)
    }

opaque define operator < : (fn (Int, Int) -> bool) = fun a:Int, y:Int {
      switch a {
        case pos(x) {
          switch y { case pos(y') { x < y' } case negsuc(y') { false } }
        }
        case negsuc(x) {
          switch y { case pos(y') { true } case negsuc(y') { y' < x } }
        }
      }
    }

define operator > : (fn (Int, Int) -> bool) = fun x:Int, y:Int {
      y < x
    }

opaque define operator ^ : (fn (Int, UInt) -> Int) = fun a:Int, b:UInt {
      expt_nat(toNat(b), a)
    }

opaque define operator ≤ : (fn (Int, Int) -> bool) = fun a:Int, y:Int {
      switch a {
        case pos(x) {
          switch y { case pos(y') { x ≤ y' } case negsuc(y') { false } }
        }
        case negsuc(x) {
          switch y { case pos(y') { true } case negsuc(y') { y' ≤ x } }
        }
      }
    }

define operator ≥ : (fn (Int, Int) -> bool) = fun x:Int, y:Int {
      y ≤ x
    }

auto sign_neg_lit

sign_neg_lit: (all x:Nat. sign(negsuc(fromNat(lit(x)))) = negative)

auto sign_pos_lit

sign_pos_lit: (all x:Nat. sign(pos(fromNat(lit(x)))) = positive)

suc_uint_monuso: (all x:UInt, y:UInt. (1 + x) ⊝ (1 + y) = x ⊝ y)