open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Bool

open Relations

open Nat

open Positive

open Div_and_mod

open Jmeq

open Russell

open List

open Util

open Setoids

open Monad

open Option

type 'a positive_map =
| Pm_leaf
| Pm_node of 'a Types.option * 'a positive_map * 'a positive_map

val positive_map_rect_Type4 :
  'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
  'a2 -> 'a2) -> 'a1 positive_map -> 'a2

val positive_map_rect_Type3 :
  'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
  'a2 -> 'a2) -> 'a1 positive_map -> 'a2

val positive_map_rect_Type2 :
  'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
  'a2 -> 'a2) -> 'a1 positive_map -> 'a2

val positive_map_rect_Type1 :
  'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
  'a2 -> 'a2) -> 'a1 positive_map -> 'a2

val positive_map_rect_Type0 :
  'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
  'a2 -> 'a2) -> 'a1 positive_map -> 'a2

val positive_map_inv_rect_Type4 :
  'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
  'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2

val positive_map_inv_rect_Type3 :
  'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
  'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2

val positive_map_inv_rect_Type2 :
  'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
  'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2

val positive_map_inv_rect_Type1 :
  'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
  'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2

val positive_map_inv_rect_Type0 :
  'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
  'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2

val positive_map_discr : 'a1 positive_map -> 'a1 positive_map -> __

val positive_map_jmdiscr : 'a1 positive_map -> 'a1 positive_map -> __

val lookup_opt : Positive.pos -> 'a1 positive_map -> 'a1 Types.option

val lookup : Positive.pos -> 'a1 positive_map -> 'a1 -> 'a1

val pm_set :
  Positive.pos -> 'a1 Types.option -> 'a1 positive_map -> 'a1 positive_map

val insert : Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map

val update :
  Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map Types.option

val fold :
  (Positive.pos -> 'a1 -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 -> 'a2

val domain_of_pm : 'a1 positive_map -> Types.unit0 positive_map

val is_none : 'a1 Types.option -> Bool.bool

val is_pm_leaf : 'a1 positive_map -> Bool.bool

val map_opt :
  ('a1 -> 'a2 Types.option) -> 'a1 positive_map -> 'a2 positive_map

val map : ('a1 -> 'a2) -> 'a1 positive_map -> 'a2 positive_map

val merge :
  ('a1 Types.option -> 'a2 Types.option -> 'a3 Types.option) -> 'a1
  positive_map -> 'a2 positive_map -> 'a3 positive_map

val domain_size : 'a1 positive_map -> Nat.nat

val pm_all_aux :
  'a1 positive_map -> 'a1 positive_map -> (Positive.pos -> Positive.pos) ->
  (Positive.pos -> 'a1 -> __ -> Bool.bool) -> Bool.bool

val pm_all :
  'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> Bool.bool) -> Bool.bool

val pm_choose :
  'a1 positive_map -> ((Positive.pos, 'a1) Types.prod, 'a1 positive_map)
  Types.prod Types.option

val pm_try_remove :
  Positive.pos -> 'a1 positive_map -> ('a1, 'a1 positive_map) Types.prod
  Types.option

val pm_fold_inf_aux :
  'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a1
  positive_map -> (Positive.pos -> Positive.pos) -> 'a2 -> 'a2

val pm_fold_inf :
  'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a2

val pm_find_aux :
  (Positive.pos -> Positive.pos) -> 'a1 positive_map -> (Positive.pos -> 'a1
  -> Bool.bool) -> (Positive.pos, 'a1) Types.prod Types.option

val pm_find :
  'a1 positive_map -> (Positive.pos -> 'a1 -> Bool.bool) -> (Positive.pos,
  'a1) Types.prod Types.option