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 **)
let zero n =
  Vector.replicate n Bool.False

(** val maximum : Nat.nat -> bitVector **)
let maximum n =
  Vector.replicate n Bool.True

(** val pad : Nat.nat -> Nat.nat -> bitVector -> Bool.bool Vector.vector **)
let pad m n b =
  Vector.pad_vector Bool.False m n b

(** val conjunction_bv : Nat.nat -> bitVector -> bitVector -> bitVector **)
let conjunction_bv n b c =
  Vector.zip_with n Bool.andb b c

(** val inclusive_disjunction_bv :
    Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector **)
let inclusive_disjunction_bv n b c =
  Vector.zip_with n Bool.orb b c

(** val exclusive_disjunction_bv :
    Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector **)
let exclusive_disjunction_bv n b c =
  Vector.zip_with n Bool.xorb b c

(** val negation_bv : Nat.nat -> bitVector -> Bool.bool Vector.vector **)
let negation_bv n b =
  Vector.map n Bool.notb b

(** val eq_b : Bool.bool -> Bool.bool -> Bool.bool **)
let eq_b b c =
  match b with
  | Bool.True -> c
  | Bool.False -> Bool.notb c

(** val eq_bv : Nat.nat -> bitVector -> bitVector -> Bool.bool **)
let eq_bv n b c =
  Vector.eq_v n eq_b b c

(** val eq_bv_elim :
    Nat.nat -> bitVector -> bitVector -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let eq_bv_elim n x y ht hf =
  Vector.eq_v_elim eq_b (fun _ clearme ->
    match clearme with
    | Bool.True ->
      (fun clearme0 ->
        match clearme0 with
        | Bool.True -> (fun auto auto' -> auto __)
        | Bool.False -> (fun auto auto' -> auto' __))
    | Bool.False ->
      (fun clearme0 ->
        match clearme0 with
        | Bool.True -> (fun auto auto' -> auto' __)
        | Bool.False -> (fun auto auto' -> auto __))) n x y ht hf