union Int {
pos(UInt)
negsuc(UInt)
}
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)
int_add_assoc: (all x:Int, y:Int, z:Int. (x + y) + z = x + (y + z))
int_add_commute: (all x:Int, y:Int. x + y = y + x)
int_add_inverse: (all x:Int. x + - x = +0)
auto int_add_zero
int_add_zero: (all n:Int. n + +0 = n)
int_less_equal_antisymmetric: (all x:Int, y:Int. (if (x ≤ y and y ≤ x) then x = y))
int_less_equal_refl: (all n:Int. n ≤ n)
int_less_equal_trans: (all m:Int, n:Int, o:Int. (if (m ≤ n and n ≤ o) then m ≤ o))
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)
auto int_one_mult
int_one_mult: (all x:Int. +1 * x = x)
int_sub_cancel: (all x:Int. x - x = +0)
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))))
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)
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)