open Preamble

open Deqsets

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

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open BitVectorTrie

type bitVectorTrieSet = Types.unit0 BitVectorTrie.bitVectorTrie

(** val set_member :
    Nat.nat -> Bool.bool Vector.vector -> bitVectorTrieSet -> Bool.bool **)
let rec set_member n p b =
  (match p with
   | Vector.VEmpty ->
     (match b with
      | BitVectorTrie.Leaf x -> (fun _ -> Bool.True)
      | BitVectorTrie.Node (x, x0, x1) ->
        (fun _ -> Obj.magic Nat.nat_discr (Nat.S x) Nat.O __)
      | BitVectorTrie.Stub x -> (fun _ -> Bool.False))
   | Vector.VCons (o, hd, tl) ->
     (match b with
      | BitVectorTrie.Leaf x ->
        (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S o) __)
      | BitVectorTrie.Node (p0, l, r) ->
        (match hd with
         | Bool.True -> (fun _ -> set_member o tl r)
         | Bool.False -> (fun _ -> set_member o tl l))
      | BitVectorTrie.Stub x -> (fun _ -> Bool.False))) __

(** val set_union :
    Nat.nat -> bitVectorTrieSet -> bitVectorTrieSet -> bitVectorTrieSet **)
let rec set_union n = function
| BitVectorTrie.Leaf l -> (fun c -> BitVectorTrie.Leaf l)
| BitVectorTrie.Node (p, l, r) ->
  (fun c ->
    (match c with
     | BitVectorTrie.Leaf x ->
       (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S p) __)
     | BitVectorTrie.Node (p', l', r') ->
       (fun _ -> BitVectorTrie.Node (p, (set_union p l l'),
         (set_union p r r')))
     | BitVectorTrie.Stub x -> (fun _ -> BitVectorTrie.Node (p, l, r))) __)
| BitVectorTrie.Stub x -> (fun c -> c)

(** val set_eq :
    Nat.nat -> bitVectorTrieSet -> bitVectorTrieSet -> Bool.bool **)
let rec set_eq n b c =
  (match b with
   | BitVectorTrie.Leaf l ->
     (match c with
      | BitVectorTrie.Leaf l' -> (fun _ -> Bool.True)
      | BitVectorTrie.Node (x, x0, x1) -> (fun _ -> Bool.False)
      | BitVectorTrie.Stub x -> (fun _ -> Bool.False))
   | BitVectorTrie.Node (h, l, r) ->
     (match c with
      | BitVectorTrie.Leaf x -> (fun _ -> Bool.False)
      | BitVectorTrie.Node (h', l', r') ->
        (fun _ ->
          Bool.andb (set_eq h l r) (set_eq h r (Logic.eq_rect_Type0 h' r' h)))
      | BitVectorTrie.Stub x -> (fun _ -> Bool.False))
   | BitVectorTrie.Stub s ->
     (match c with
      | BitVectorTrie.Leaf x -> (fun _ -> Bool.False)
      | BitVectorTrie.Node (x, x0, x1) -> (fun _ -> Bool.False)
      | BitVectorTrie.Stub s' -> (fun _ -> Util.eq_nat s s'))) __

(** val set_insert :
    Nat.nat -> BitVector.bitVector -> bitVectorTrieSet -> Types.unit0
    BitVectorTrie.bitVectorTrie **)
let set_insert n b s =
  BitVectorTrie.insert n b Types.It s

(** val set_empty : Nat.nat -> Types.unit0 BitVectorTrie.bitVectorTrie **)
let set_empty n =
  BitVectorTrie.Stub n

(** val set_singleton :
    Nat.nat -> BitVector.bitVector -> Types.unit0 BitVectorTrie.bitVectorTrie **)
let set_singleton n b =
  BitVectorTrie.insert n b Types.It (set_empty n)