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

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

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_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_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_two_odd: (all n:Int. Odd(+1 + +2 * n))

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