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

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

union UInt

fun div2(b:UInt)

fun fromNat(Nat) -> UInt

fun log(b:UInt) {
  cnt_dubs(pred(b))
}

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_one_odd: (all n:UInt. (if Even(1 + n) then Odd(n)))

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