open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Setoids

open Monad

open Option

open Extranat

open Vector

open Div_and_mod

open Jmeq

open Russell

open List

open Util

open FoldStuff

open Bool

open Relations

open Nat

open BitVector

type 'a bitVectorTrie =
| Leaf of 'a
| Node of Nat.nat * 'a bitVectorTrie * 'a bitVectorTrie
| Stub of Nat.nat

val bitVectorTrie_rect_Type4 :
  ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
  -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2

val bitVectorTrie_rect_Type3 :
  ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
  -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2

val bitVectorTrie_rect_Type2 :
  ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
  -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2

val bitVectorTrie_rect_Type1 :
  ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
  -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2

val bitVectorTrie_rect_Type0 :
  ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
  -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2

val bitVectorTrie_inv_rect_Type4 :
  Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
  bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
  'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2

val bitVectorTrie_inv_rect_Type3 :
  Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
  bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
  'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2

val bitVectorTrie_inv_rect_Type2 :
  Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
  bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
  'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2

val bitVectorTrie_inv_rect_Type1 :
  Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
  bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
  'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2

val bitVectorTrie_inv_rect_Type0 :
  Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
  bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
  'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2

val bitVectorTrie_discr :
  Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __

val bitVectorTrie_jmdiscr :
  Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __

val fold :
  Nat.nat -> (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a1 bitVectorTrie
  -> 'a2 -> 'a2

val bvtfold_aux :
  (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a2 -> Nat.nat -> 'a1
  bitVectorTrie -> BitVector.bitVector -> 'a2

val lookup_opt :
  Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 Types.option

val member : Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> Bool.bool

val lookup :
  Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 -> 'a1

val prepare_trie_for_insertion :
  Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie

val insert :
  Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
  bitVectorTrie

val update :
  Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
  bitVectorTrie Types.option

val merge :
  Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie

open Deqsets

type strong_decidable = (__, __) Types.sum

val strong_decidable_in_codomain :
  Deqsets.deqSet -> Nat.nat -> __ bitVectorTrie -> __ -> strong_decidable