define Even : (fn UInt -> bool) = fun n:UInt {
      some m:UInt. n = 2 * m
    }

define Odd : (fn UInt -> bool) = fun 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
  inverse uint_unview_view
}

opaque define div2 : (fn UInt -> UInt)

opaque recursive fromNat(Nat) -> UInt

opaque define log : (fn UInt -> UInt)

define max : (fn (UInt, UInt) -> UInt) = fun x:UInt, y:UInt {
      if x < y then
        y
      else
        x
    }

define min : (fn (UInt, UInt) -> UInt) = fun x:UInt, y:UInt {
      if x < y then
        x
      else
        y
    }

opaque recursive operator *(UInt,UInt) -> UInt

opaque recursive operator +(UInt,UInt) -> UInt

opaque recursive operator <(UInt,UInt) -> bool

define operator > : (fn (UInt, UInt) -> bool) = fun x:UInt, y:UInt {
      y < x
    }

opaque define operator ^ : (fn (UInt, UInt) -> UInt)

opaque recursive operator ∸(UInt,UInt) -> UInt

define operator ≤ : (fn (UInt, UInt) -> bool) = fun x:UInt, y:UInt {
      ((x < y) or (x = y))
    }

define operator ≥ : (fn (UInt, UInt) -> bool) = fun x:UInt, y:UInt {
      y ≤ x
    }

define sqr : (fn UInt -> UInt) = fun a:UInt {
      a * a
    }

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