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) = fun b:UInt {
      switch b {
        case bzero {
          0
        }
        case dub_inc(x) {
          inc(x)
        }
        case inc_dub(x) {
          x
        }
      }
    }

opaque recursive fromNat(Nat) -> UInt{
  fromNat(zero) = 0
  fromNat(suc(n)) = inc(fromNat(n))
}

opaque define log : (fn UInt -> UInt) = fun b:UInt {
      cnt_dubs(pred(b))
    }

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{
  operator *(bzero, y) = 0
  operator *(dub_inc(x), y) = 
    switch y {
      case bzero {
        0
      }
      case dub_inc(y') {
        dub(dub_inc((x + y') + x * y'))
      }
      case inc_dub(y') {
        dub_inc(x + dub(y' + x * y'))
      }
    }
  operator *(inc_dub(x), y) = 
    switch y {
      case bzero {
        0
      }
      case dub_inc(y') {
        dub_inc((dub(x) + y') + dub(x * y'))
      }
      case inc_dub(y') {
        inc_dub((x + y') + dub(x * y'))
      }
    }
}

opaque recursive operator +(UInt,UInt) -> UInt{
  operator +(bzero, y) = y
  operator +(dub_inc(x), y) = 
    switch y {
      case bzero {
        dub_inc(x)
      }
      case dub_inc(y') {
        dub_inc(inc(x + y'))
      }
      case inc_dub(y') {
        inc(dub_inc(x + y'))
      }
    }
  operator +(inc_dub(x), y) = 
    switch y {
      case bzero {
        inc_dub(x)
      }
      case dub_inc(y') {
        inc(dub_inc(x + y'))
      }
      case inc_dub(y') {
        inc(inc_dub(x + y'))
      }
    }
}

opaque recursive operator <(UInt,UInt) -> bool{
  operator <(bzero, y) = 
    switch y {
      case bzero {
        false
      }
      case dub_inc(y') {
        true
      }
      case inc_dub(y') {
        true
      }
    }
  operator <(dub_inc(x'), y) = 
    switch y {
      case bzero {
        false
      }
      case dub_inc(y') {
        x' < y'
      }
      case inc_dub(y') {
        x' < y'
      }
    }
  operator <(inc_dub(x'), y) = 
    switch y {
      case bzero {
        false
      }
      case dub_inc(y') {
        ((x' < y') or (x' = y'))
      }
      case inc_dub(y') {
        x' < y'
      }
    }
}

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

opaque define operator ^ : (fn (UInt, UInt) -> UInt) = fun a:UInt, b:UInt {
      expt(b, a)
    }

opaque recursive operator ∸(UInt,UInt) -> UInt{
  operator ∸(bzero, y) = 0
  operator ∸(dub_inc(x), y) = 
    switch y {
      case bzero {
        dub_inc(x)
      }
      case dub_inc(y') {
        dub(x ∸ y')
      }
      case inc_dub(y') {
        (if x < y' then 0 else inc_dub(x ∸ y'))
      }
    }
  operator ∸(inc_dub(x), y) = 
    switch y {
      case bzero {
        inc_dub(x)
      }
      case dub_inc(y') {
        (if x < y' then 0 else pred(dub(x ∸ y')))
      }
      case inc_dub(y') {
        dub(x ∸ y')
      }
    }
}

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{
  toNat(bzero) = ℕ0
  toNat(dub_inc(x)) = ℕ2 * suc(toNat(x))
  toNat(inc_dub(x)) = suc(ℕ2 * toNat(x))
}

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