fun Even(n:Int) {
  some m:Int. n = +2 * m
}

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

fun Odd(n:Int) {
  some m:Int. n = +1 + +2 * m
}

fun abs(x:Int)

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

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_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_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_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_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_negsuc_eq_pos_false: (all x:UInt, y:UInt. not (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)))

auto int_one_mult

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

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

int_pos_eq_negsuc_false: (all x:UInt, y:UInt. not (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_sub_add_cancel: (all x:Int, y:Int. (x - y) + y = x)

int_sub_cancel: (all x:Int. x - x = +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)

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

fun max(x:Int, y:Int) {
  if x < y then
    y
  else
    x
}

fun min(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

fun operator *(x:Int, y:Int)

fun operator *(n:UInt, m:Int)

fun operator *(n:Int, m:UInt)

fun operator +(x:Int, m:Int)

fun operator +(n:UInt, m:Int)

fun operator +(n:Int, m:UInt)

fun operator -(x:Int)

fun operator -(n:UInt)

fun operator -(n:Int, m:Int) {
  n + - m
}

fun operator -(n:UInt, m:Int)

fun operator -(n:Int, m:UInt)

fun operator -(x:UInt, y:UInt)

fun operator /(n:Int, m:Int)

fun operator /(n:Int, m:UInt)

fun operator <(a:Int, y:Int)

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

fun operator ≤(a:Int, y:Int)

fun operator ≥(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)