open Preamble

open Setoids

open Monad

open Option

open Extranat

open Vector

open Div_and_mod

open Jmeq

open Russell

open Types

open List

open Util

open FoldStuff

open Bool

open Hints_declaration

open Core_notation

open Pts

open Logic

open Relations

open Nat

open BitVector

open Exp

val addr16_of_addr11 : BitVector.word -> BitVector.word11 -> BitVector.word

val nat_of_bool : Bool.bool -> Nat.nat

val carry_of : Bool.bool -> Bool.bool -> Bool.bool -> Bool.bool

val add_with_carries :
  Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
  (BitVector.bitVector, BitVector.bitVector) Types.prod

val borrow_of : Bool.bool -> Bool.bool -> Bool.bool -> Bool.bool

val sub_with_borrows :
  Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
  (BitVector.bitVector, BitVector.bitVector) Types.prod

val add_n_with_carry :
  Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
  (BitVector.bitVector, BitVector.bitVector) Types.prod

val sub_n_with_carry :
  Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
  (BitVector.bitVector, BitVector.bitVector) Types.prod

val add_8_with_carry :
  BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
  (BitVector.bitVector, BitVector.bitVector) Types.prod

val add_16_with_carry :
  BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
  (BitVector.bitVector, BitVector.bitVector) Types.prod

val sub_7_with_carry :
  BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
  (BitVector.bitVector, BitVector.bitVector) Types.prod

val sub_8_with_carry :
  BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
  (BitVector.bitVector, BitVector.bitVector) Types.prod

val sub_16_with_carry :
  BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
  (BitVector.bitVector, BitVector.bitVector) Types.prod

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

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

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

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

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

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

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

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

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

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

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

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

type fbs_diff =
| Fbs_diff' of Nat.nat * Nat.nat

val fbs_diff_rect_Type4 :
  (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1

val fbs_diff_rect_Type5 :
  (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1

val fbs_diff_rect_Type3 :
  (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1

val fbs_diff_rect_Type2 :
  (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1

val fbs_diff_rect_Type1 :
  (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1

val fbs_diff_rect_Type0 :
  (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1

val fbs_diff_inv_rect_Type4 :
  Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1

val fbs_diff_inv_rect_Type3 :
  Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1

val fbs_diff_inv_rect_Type2 :
  Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1

val fbs_diff_inv_rect_Type1 :
  Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1

val fbs_diff_inv_rect_Type0 :
  Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1

val fbs_diff_discr : Nat.nat -> fbs_diff -> fbs_diff -> __

val fbs_diff_jmdiscr : Nat.nat -> fbs_diff -> fbs_diff -> __

val first_bit_set : Nat.nat -> BitVector.bitVector -> fbs_diff Types.option

val divmod_u_aux :
  Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
  (BitVector.bitVector, BitVector.bitVector) Types.prod

val divmod_u :
  Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
  (BitVector.bitVector, BitVector.bitVector) Types.prod Types.option

val division_u :
  Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
  BitVector.bitVector Types.option

val division_s :
  Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
  BitVector.bitVector Types.option

val modulus_u :
  Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
  BitVector.bitVector Types.option

val modulus_s :
  Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
  BitVector.bitVector Types.option

val lt_u :
  Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector -> Bool.bool

val gt_u :
  Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector -> Bool.bool

val lte_u :
  Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector -> Bool.bool

val gte_u :
  Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector -> Bool.bool

val lt_s : Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool

val gt_s : Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool

val lte_s :
  Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool

val gte_s :
  Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool

type ternary =
| Zero_carry
| One_carry
| Two_carry

val ternary_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1

val ternary_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1

val ternary_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1

val ternary_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1

val ternary_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1

val ternary_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1

val ternary_inv_rect_Type4 :
  ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val ternary_inv_rect_Type3 :
  ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val ternary_inv_rect_Type2 :
  ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val ternary_inv_rect_Type1 :
  ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val ternary_inv_rect_Type0 :
  ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val ternary_discr : ternary -> ternary -> __

val ternary_jmdiscr : ternary -> ternary -> __

val carry_0 : ternary -> (Bool.bool, ternary) Types.prod

val carry_1 : ternary -> (Bool.bool, ternary) Types.prod

val carry_2 : ternary -> (Bool.bool, ternary) Types.prod

val carry_3 : ternary -> (Bool.bool, ternary) Types.prod

val ternary_carry_of :
  Bool.bool -> Bool.bool -> Bool.bool -> ternary -> (Bool.bool, ternary)
  Types.prod

val canonical_add :
  Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
  BitVector.bitVector -> ternary -> (BitVector.bitVector, ternary) Types.prod

val carries_to_ternary : Bool.bool -> Bool.bool -> ternary

val max_u :
  Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector -> Bool.bool
  Vector.vector

val min_u :
  Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector -> Bool.bool
  Vector.vector

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

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

val bitvector_of_bool : Nat.nat -> Bool.bool -> BitVector.bitVector

val full_add :
  Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> BitVector.bit ->
  (BitVector.bit, BitVector.bitVector) Types.prod

val half_add :
  Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> (BitVector.bit,
  BitVector.bitVector) Types.prod

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

val sign_extension : BitVector.byte -> BitVector.word

val sign_bit : Nat.nat -> BitVector.bitVector -> Bool.bool

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

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

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