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

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

view UInt {
  source Binary
  target UIntView
  into uint_view
  out uint_unview
  roundtrip uint_view_unview
}

fun div2(b:UInt)

fun fromNat(Nat) -> UInt

fun log(b:UInt)

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

fun min(x:UInt, y:UInt) {
  if x < y then
    x
  else
    y
}

fun operator *(UInt,UInt) -> UInt

fun operator +(UInt,UInt) -> UInt

fun operator <(UInt,UInt) -> bool

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

fun operator ^(a:UInt, b:UInt)

fun operator ∸(UInt,UInt) -> UInt

fun operator ≤(x:UInt, y:UInt) {
  ((x < y) or (x = y))
}

fun operator ≥(x:UInt, y:UInt) {
  y ≤ x
}

fun sqr(a:UInt) {
  a * a
}

fun toNat(UInt) -> Nat

uint_Even_not_Odd: (all n:UInt. (Even(n) ⇔ not Odd(n)))

uint_Even_or_Odd: (all n:UInt. (Even(n) or Odd(n)))

uint_even_add_even: (all x:UInt, y:UInt. (if (Even(x) and Even(y)) then Even(x + y)))

uint_even_add_odd: (all x:UInt, y:UInt. (if (Even(x) and Odd(y)) then Odd(x + y)))

uint_even_mult_left: (all x:UInt, y:UInt. (if Even(x) then Even(x * y)))

uint_even_mult_right: (all x:UInt, y:UInt. (if Even(y) then Even(x * y)))

uint_even_one_odd: (all n:UInt. (if Even(1 + n) then Odd(n)))

uint_odd_add_even: (all x:UInt, y:UInt. (if (Odd(x) and Even(y)) then Odd(x + y)))

uint_odd_add_odd: (all x:UInt, y:UInt. (if (Odd(x) and Odd(y)) then Even(x + y)))

uint_odd_mult_odd: (all x:UInt, y:UInt. (if (Odd(x) and Odd(y)) then Odd(x * y)))

uint_odd_one_even: (all n:UInt. (if Odd(1 + n) then Even(n)))

uint_one_two_odd: (all n:UInt. Odd(1 + 2 * n))

uint_two_even: (all n:UInt. Even(2 * n))