open Preamble

open Bool

open Hints_declaration

open Core_notation

open Pts

open Logic

open Relations

open Nat

open Div_and_mod

open Jmeq

open Russell

open Types

open List

open Util

open FoldStuff

open Setoids

open Monad

open Option

open Extranat

open Vector

type bitVector = Bool.bool Vector.vector

type bit = Bool.bool

type nibble = bitVector

type byte7 = bitVector

type byte = bitVector

type word = bitVector

type word11 = bitVector

val zero : Nat.nat -> bitVector

val maximum : Nat.nat -> bitVector

val pad : Nat.nat -> Nat.nat -> bitVector -> Bool.bool Vector.vector

val conjunction_bv : Nat.nat -> bitVector -> bitVector -> bitVector

val inclusive_disjunction_bv :
  Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector

val exclusive_disjunction_bv :
  Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector

val negation_bv : Nat.nat -> bitVector -> Bool.bool Vector.vector

val eq_b : Bool.bool -> Bool.bool -> Bool.bool

val eq_bv : Nat.nat -> bitVector -> bitVector -> Bool.bool

val eq_bv_elim :
  Nat.nat -> bitVector -> bitVector -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1