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 **)
let rec bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub x_14760 = function
| Leaf x_14762 -> h_Leaf x_14762
| Node (n, x_14764, x_14763) ->
  h_Node n x_14764 x_14763
    (bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub n x_14764)
    (bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub n x_14763)
| Stub n -> h_Stub n

(** val bitVectorTrie_rect_Type3 :
    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
let rec bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub x_14776 = function
| Leaf x_14778 -> h_Leaf x_14778
| Node (n, x_14780, x_14779) ->
  h_Node n x_14780 x_14779
    (bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub n x_14780)
    (bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub n x_14779)
| Stub n -> h_Stub n

(** val bitVectorTrie_rect_Type2 :
    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
let rec bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub x_14784 = function
| Leaf x_14786 -> h_Leaf x_14786
| Node (n, x_14788, x_14787) ->
  h_Node n x_14788 x_14787
    (bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub n x_14788)
    (bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub n x_14787)
| Stub n -> h_Stub n

(** val bitVectorTrie_rect_Type1 :
    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
let rec bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub x_14792 = function
| Leaf x_14794 -> h_Leaf x_14794
| Node (n, x_14796, x_14795) ->
  h_Node n x_14796 x_14795
    (bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub n x_14796)
    (bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub n x_14795)
| Stub n -> h_Stub n

(** val bitVectorTrie_rect_Type0 :
    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
let rec bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub x_14800 = function
| Leaf x_14802 -> h_Leaf x_14802
| Node (n, x_14804, x_14803) ->
  h_Node n x_14804 x_14803
    (bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub n x_14804)
    (bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub n x_14803)
| Stub n -> h_Stub n

(** val bitVectorTrie_inv_rect_Type4 :
    Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat ->
    'a1 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __
    -> 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2 **)
let bitVectorTrie_inv_rect_Type4 x2 hterm h1 h2 h3 =
  let hcut = bitVectorTrie_rect_Type4 h1 h2 h3 x2 hterm in hcut __ __

(** val bitVectorTrie_inv_rect_Type3 :
    Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat ->
    'a1 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __
    -> 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2 **)
let bitVectorTrie_inv_rect_Type3 x2 hterm h1 h2 h3 =
  let hcut = bitVectorTrie_rect_Type3 h1 h2 h3 x2 hterm in hcut __ __

(** val bitVectorTrie_inv_rect_Type2 :
    Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat ->
    'a1 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __
    -> 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2 **)
let bitVectorTrie_inv_rect_Type2 x2 hterm h1 h2 h3 =
  let hcut = bitVectorTrie_rect_Type2 h1 h2 h3 x2 hterm in hcut __ __

(** val bitVectorTrie_inv_rect_Type1 :
    Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat ->
    'a1 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __
    -> 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2 **)
let bitVectorTrie_inv_rect_Type1 x2 hterm h1 h2 h3 =
  let hcut = bitVectorTrie_rect_Type1 h1 h2 h3 x2 hterm in hcut __ __

(** val bitVectorTrie_inv_rect_Type0 :
    Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat ->
    'a1 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __
    -> 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2 **)
let bitVectorTrie_inv_rect_Type0 x2 hterm h1 h2 h3 =
  let hcut = bitVectorTrie_rect_Type0 h1 h2 h3 x2 hterm in hcut __ __

(** val bitVectorTrie_discr :
    Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __ **)
let bitVectorTrie_discr a2 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Leaf a0 -> Obj.magic (fun _ dH -> dH __)
     | Node (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Stub a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val bitVectorTrie_jmdiscr :
    Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __ **)
let bitVectorTrie_jmdiscr a2 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Leaf a0 -> Obj.magic (fun _ dH -> dH __)
     | Node (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Stub a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val fold :
    Nat.nat -> (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a1
    bitVectorTrie -> 'a2 -> 'a2 **)
let rec fold n f t b =
  (match t with
   | Leaf l -> (fun _ -> f (BitVector.zero n) l b)
   | Node (h, l, r) ->
     (fun _ ->
       fold h (fun x -> f (Vector.VCons (h, Bool.False, x))) l
         (fold h (fun x -> f (Vector.VCons (h, Bool.True, x))) r b))
   | Stub x -> (fun _ -> b)) __

(** val bvtfold_aux :
    (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a2 -> Nat.nat -> 'a1
    bitVectorTrie -> BitVector.bitVector -> 'a2 **)
let rec bvtfold_aux f seed n x x0 =
  (match n with
   | Nat.O ->
     (fun _ trie path ->
       (match trie with
        | Leaf l -> (fun _ -> f path l seed)
        | Node (n', l, r) -> (fun _ -> assert false (* absurd case *))
        | Stub s -> (fun _ -> seed)) __)
   | Nat.S n' ->
     (fun _ trie path ->
       (match trie with
        | Leaf l -> (fun _ -> assert false (* absurd case *))
        | Node (n'', l, r) ->
          (fun _ ->
            bvtfold_aux f
              (bvtfold_aux f seed n' l (Vector.VCons
                ((Nat.minus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                   (Nat.S Nat.O)))))))))))))))) (Nat.S n')), Bool.False,
                path))) n' r (Vector.VCons
              ((Nat.minus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                 (Nat.S Nat.O)))))))))))))))) (Nat.S n')), Bool.True, path)))
        | Stub s -> (fun _ -> seed)) __)) __ x x0

(** val lookup_opt :
    Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 Types.option **)
let rec lookup_opt n b t =
  (match t with
   | Leaf l -> (fun x -> Types.Some l)
   | Node (h, l, r) ->
     (fun b0 ->
       lookup_opt h (Vector.tail h b0)
         (match Vector.head' h b0 with
          | Bool.True -> r
          | Bool.False -> l))
   | Stub x -> (fun x0 -> Types.None)) b

(** val member :
    Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> Bool.bool **)
let member n b t =
  match lookup_opt n b t with
  | Types.None -> Bool.False
  | Types.Some x -> Bool.True

(** val lookup :
    Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 -> 'a1 **)
let rec lookup n b t a =
  (match b with
   | Vector.VEmpty ->
     (match t with
      | Leaf l -> (fun _ -> l)
      | Node (h, l, r) -> (fun _ -> assert false (* absurd case *))
      | Stub s -> (fun _ -> a))
   | Vector.VCons (o, hd, tl) ->
     (match t with
      | Leaf l -> (fun _ -> assert false (* absurd case *))
      | Node (h, l, r) ->
        (match hd with
         | Bool.True -> (fun _ -> lookup h tl r a)
         | Bool.False -> (fun _ -> lookup h tl l a))
      | Stub s -> (fun _ -> a))) __

(** val prepare_trie_for_insertion :
    Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie **)
let rec prepare_trie_for_insertion n b a =
  match b with
  | Vector.VEmpty -> Leaf a
  | Vector.VCons (o, hd, tl) ->
    (match hd with
     | Bool.True -> Node (o, (Stub o), (prepare_trie_for_insertion o tl a))
     | Bool.False -> Node (o, (prepare_trie_for_insertion o tl a), (Stub o)))

(** val insert :
    Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
    bitVectorTrie **)
let rec insert n b a =
  match b with
  | Vector.VEmpty -> (fun x -> Leaf a)
  | Vector.VCons (o, hd, tl) ->
    (fun t ->
      (match t with
       | Leaf l -> (fun _ -> assert false (* absurd case *))
       | Node (p, l, r) ->
         (fun _ ->
           match hd with
           | Bool.True -> Node (o, l, (insert o tl a r))
           | Bool.False -> Node (o, (insert o tl a l), r))
       | Stub p ->
         (fun _ ->
           prepare_trie_for_insertion (Nat.S o) (Vector.VCons (o, hd, tl)) a))
        __)

(** val update :
    Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
    bitVectorTrie Types.option **)
let rec update n b a =
  match b with
  | Vector.VEmpty ->
    (fun t ->
      (match t with
       | Leaf x -> (fun _ -> Types.Some (Leaf a))
       | Node (x, x0, x1) -> (fun _ -> assert false (* absurd case *))
       | Stub x -> (fun _ -> Types.None)) __)
  | Vector.VCons (o, hd, tl) ->
    (fun t ->
      (match t with
       | Leaf l -> (fun _ -> assert false (* absurd case *))
       | Node (p, l, r) ->
         (fun _ ->
           match hd with
           | Bool.True ->
             Types.option_map (fun v -> Node (o, l, v)) (update o tl a r)
           | Bool.False ->
             Types.option_map (fun v -> Node (o, v, r)) (update o tl a l))
       | Stub p -> (fun _ -> Types.None)) __)

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

open Deqsets

type strong_decidable = (__, __) Types.sum

(** val strong_decidable_in_codomain :
    Deqsets.deqSet -> Nat.nat -> __ bitVectorTrie -> __ -> strong_decidable **)
let strong_decidable_in_codomain a n m =
  bitVectorTrie_rect_Type0 (fun a' a0 ->
    Bool.bool_inv_rect_Type0 (Deqsets.eqb a a' a0) (fun _ -> Types.Inl __)
      (fun _ -> Types.Inr __)) (fun n0 l r hl hr a0 ->
    match hl a0 with
    | Types.Inl _ -> Types.Inl __
    | Types.Inr _ ->
      (match hr a0 with
       | Types.Inl _ -> Types.Inl __
       | Types.Inr _ -> Types.Inr __)) (fun n0 a0 -> Types.Inr __) n m