open Preamble

open Bool

open Hints_declaration

open Core_notation

open Pts

open Logic

open Relations

open Nat

open Jmeq

open Russell

open List

open Setoids

open Monad

open Option

open Types

open Extranat

open Vector

open Div_and_mod

open Util

open FoldStuff

open BitVector

open Exp

open Arithmetic

type comparison =
| Ceq
| Cne
| Clt
| Cle
| Cgt
| Cge

val comparison_rect_Type4 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1

val comparison_rect_Type5 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1

val comparison_rect_Type3 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1

val comparison_rect_Type2 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1

val comparison_rect_Type1 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1

val comparison_rect_Type0 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1

val comparison_inv_rect_Type4 :
  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
  (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val comparison_inv_rect_Type3 :
  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
  (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val comparison_inv_rect_Type2 :
  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
  (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val comparison_inv_rect_Type1 :
  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
  (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val comparison_inv_rect_Type0 :
  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
  (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val comparison_discr : comparison -> comparison -> __

val comparison_jmdiscr : comparison -> comparison -> __

val negate_comparison : comparison -> comparison

val swap_comparison : comparison -> comparison

val wordsize : Nat.nat

type int = BitVector.bitVector

val repr : Nat.nat -> int

val zero : int

val one : int

val mone : BitVector.bitVector

val iwordsize : int

val eq_dec : int -> int -> (__, __) Types.sum

val eq : int -> int -> Bool.bool

val lt : int -> int -> Bool.bool

val ltu : int -> int -> Bool.bool

val neg : int -> int

val mul :
  BitVector.bitVector -> BitVector.bitVector -> Bool.bool Vector.vector

val zero_ext_n :
  Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector

val zero_ext : Nat.nat -> int -> int

val sign_ext_n :
  Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector

val sign_ext : Nat.nat -> int -> int

val i_and : int -> int -> int

val or0 : int -> int -> int

val xor : int -> int -> int

val not : int -> int

val shl : int -> int -> int

val shru : int -> int -> int

val shr : int -> int -> int

val shrx : int -> int -> int

val shr_carry : int -> int -> BitVector.bitVector

val rol : int -> int -> int

val ror : int -> int -> int

val rolm : int -> int -> int -> int

val cmp : comparison -> int -> int -> Bool.bool

val cmpu : comparison -> int -> int -> Bool.bool

val notbool : int -> int