open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Bool

open Relations

open Nat

type compare =
| LT
| EQ
| GT

(** val compare_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
let rec compare_rect_Type4 h_LT h_EQ h_GT = function
| LT -> h_LT
| EQ -> h_EQ
| GT -> h_GT

(** val compare_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
let rec compare_rect_Type5 h_LT h_EQ h_GT = function
| LT -> h_LT
| EQ -> h_EQ
| GT -> h_GT

(** val compare_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
let rec compare_rect_Type3 h_LT h_EQ h_GT = function
| LT -> h_LT
| EQ -> h_EQ
| GT -> h_GT

(** val compare_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
let rec compare_rect_Type2 h_LT h_EQ h_GT = function
| LT -> h_LT
| EQ -> h_EQ
| GT -> h_GT

(** val compare_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
let rec compare_rect_Type1 h_LT h_EQ h_GT = function
| LT -> h_LT
| EQ -> h_EQ
| GT -> h_GT

(** val compare_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
let rec compare_rect_Type0 h_LT h_EQ h_GT = function
| LT -> h_LT
| EQ -> h_EQ
| GT -> h_GT

(** val compare_inv_rect_Type4 :
    compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let compare_inv_rect_Type4 hterm h1 h2 h3 =
  let hcut = compare_rect_Type4 h1 h2 h3 hterm in hcut __

(** val compare_inv_rect_Type3 :
    compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let compare_inv_rect_Type3 hterm h1 h2 h3 =
  let hcut = compare_rect_Type3 h1 h2 h3 hterm in hcut __

(** val compare_inv_rect_Type2 :
    compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let compare_inv_rect_Type2 hterm h1 h2 h3 =
  let hcut = compare_rect_Type2 h1 h2 h3 hterm in hcut __

(** val compare_inv_rect_Type1 :
    compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let compare_inv_rect_Type1 hterm h1 h2 h3 =
  let hcut = compare_rect_Type1 h1 h2 h3 hterm in hcut __

(** val compare_inv_rect_Type0 :
    compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let compare_inv_rect_Type0 hterm h1 h2 h3 =
  let hcut = compare_rect_Type0 h1 h2 h3 hterm in hcut __

(** val compare_discr : compare -> compare -> __ **)
let compare_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | LT -> Obj.magic (fun _ dH -> dH)
     | EQ -> Obj.magic (fun _ dH -> dH)
     | GT -> Obj.magic (fun _ dH -> dH)) y

(** val compare_invert : compare -> compare **)
let compare_invert = function
| LT -> GT
| EQ -> EQ
| GT -> LT

type pos =
| One
| P1 of pos
| P0 of pos

(** val pos_rect_Type4 :
    'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
let rec pos_rect_Type4 h_one h_p1 h_p0 = function
| One -> h_one
| P1 x_1606 -> h_p1 x_1606 (pos_rect_Type4 h_one h_p1 h_p0 x_1606)
| P0 x_1607 -> h_p0 x_1607 (pos_rect_Type4 h_one h_p1 h_p0 x_1607)

(** val pos_rect_Type3 :
    'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
let rec pos_rect_Type3 h_one h_p1 h_p0 = function
| One -> h_one
| P1 x_1618 -> h_p1 x_1618 (pos_rect_Type3 h_one h_p1 h_p0 x_1618)
| P0 x_1619 -> h_p0 x_1619 (pos_rect_Type3 h_one h_p1 h_p0 x_1619)

(** val pos_rect_Type2 :
    'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
let rec pos_rect_Type2 h_one h_p1 h_p0 = function
| One -> h_one
| P1 x_1624 -> h_p1 x_1624 (pos_rect_Type2 h_one h_p1 h_p0 x_1624)
| P0 x_1625 -> h_p0 x_1625 (pos_rect_Type2 h_one h_p1 h_p0 x_1625)

(** val pos_rect_Type1 :
    'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
let rec pos_rect_Type1 h_one h_p1 h_p0 = function
| One -> h_one
| P1 x_1630 -> h_p1 x_1630 (pos_rect_Type1 h_one h_p1 h_p0 x_1630)
| P0 x_1631 -> h_p0 x_1631 (pos_rect_Type1 h_one h_p1 h_p0 x_1631)

(** val pos_rect_Type0 :
    'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
let rec pos_rect_Type0 h_one h_p1 h_p0 = function
| One -> h_one
| P1 x_1636 -> h_p1 x_1636 (pos_rect_Type0 h_one h_p1 h_p0 x_1636)
| P0 x_1637 -> h_p0 x_1637 (pos_rect_Type0 h_one h_p1 h_p0 x_1637)

(** val pos_inv_rect_Type4 :
    pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
    'a1) -> __ -> 'a1) -> 'a1 **)
let pos_inv_rect_Type4 hterm h1 h2 h3 =
  let hcut = pos_rect_Type4 h1 h2 h3 hterm in hcut __

(** val pos_inv_rect_Type3 :
    pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
    'a1) -> __ -> 'a1) -> 'a1 **)
let pos_inv_rect_Type3 hterm h1 h2 h3 =
  let hcut = pos_rect_Type3 h1 h2 h3 hterm in hcut __

(** val pos_inv_rect_Type2 :
    pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
    'a1) -> __ -> 'a1) -> 'a1 **)
let pos_inv_rect_Type2 hterm h1 h2 h3 =
  let hcut = pos_rect_Type2 h1 h2 h3 hterm in hcut __

(** val pos_inv_rect_Type1 :
    pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
    'a1) -> __ -> 'a1) -> 'a1 **)
let pos_inv_rect_Type1 hterm h1 h2 h3 =
  let hcut = pos_rect_Type1 h1 h2 h3 hterm in hcut __

(** val pos_inv_rect_Type0 :
    pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
    'a1) -> __ -> 'a1) -> 'a1 **)
let pos_inv_rect_Type0 hterm h1 h2 h3 =
  let hcut = pos_rect_Type0 h1 h2 h3 hterm in hcut __

(** val pos_discr : pos -> pos -> __ **)
let pos_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | One -> Obj.magic (fun _ dH -> dH)
     | P1 a0 -> Obj.magic (fun _ dH -> dH __)
     | P0 a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val pred : pos -> pos **)
let rec pred = function
| One -> One
| P1 ps -> P0 ps
| P0 ps ->
  (match ps with
   | One -> One
   | P1 x -> P1 (pred ps)
   | P0 x -> P1 (pred ps))

(** val succ : pos -> pos **)
let rec succ = function
| One -> P0 One
| P1 ps -> P0 (succ ps)
| P0 ps -> P1 ps

(** val nat_of_pos : pos -> Nat.nat **)
let rec nat_of_pos = function
| One -> Nat.S Nat.O
| P1 ps -> Nat.S (Nat.times (Nat.S (Nat.S Nat.O)) (nat_of_pos ps))
| P0 ps -> Nat.times (Nat.S (Nat.S Nat.O)) (nat_of_pos ps)

(** val succ_pos_of_nat : Nat.nat -> pos **)
let rec succ_pos_of_nat = function
| Nat.O -> One
| Nat.S n' -> succ (succ_pos_of_nat n')

(** val plus : pos -> pos -> pos **)
let rec plus n m =
  match n with
  | One -> succ m
  | P1 n' ->
    (match m with
     | One -> succ n
     | P1 m' -> P0 (succ (plus n' m'))
     | P0 m' -> P1 (plus n' m'))
  | P0 n' ->
    (match m with
     | One -> P1 n'
     | P1 m' -> P1 (plus n' m')
     | P0 m' -> P0 (plus n' m'))

(** val times : pos -> pos -> pos **)
let rec times n m =
  match n with
  | One -> m
  | P1 n' -> plus m (P0 (times n' m))
  | P0 n' -> P0 (times n' m)

type minusresult =
| MinusNeg
| MinusZero
| MinusPos of pos

(** val minusresult_rect_Type4 :
    'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
let rec minusresult_rect_Type4 h_MinusNeg h_MinusZero h_MinusPos = function
| MinusNeg -> h_MinusNeg
| MinusZero -> h_MinusZero
| MinusPos x_1813 -> h_MinusPos x_1813

(** val minusresult_rect_Type5 :
    'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
let rec minusresult_rect_Type5 h_MinusNeg h_MinusZero h_MinusPos = function
| MinusNeg -> h_MinusNeg
| MinusZero -> h_MinusZero
| MinusPos x_1818 -> h_MinusPos x_1818

(** val minusresult_rect_Type3 :
    'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
let rec minusresult_rect_Type3 h_MinusNeg h_MinusZero h_MinusPos = function
| MinusNeg -> h_MinusNeg
| MinusZero -> h_MinusZero
| MinusPos x_1823 -> h_MinusPos x_1823

(** val minusresult_rect_Type2 :
    'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
let rec minusresult_rect_Type2 h_MinusNeg h_MinusZero h_MinusPos = function
| MinusNeg -> h_MinusNeg
| MinusZero -> h_MinusZero
| MinusPos x_1828 -> h_MinusPos x_1828

(** val minusresult_rect_Type1 :
    'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
let rec minusresult_rect_Type1 h_MinusNeg h_MinusZero h_MinusPos = function
| MinusNeg -> h_MinusNeg
| MinusZero -> h_MinusZero
| MinusPos x_1833 -> h_MinusPos x_1833

(** val minusresult_rect_Type0 :
    'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
let rec minusresult_rect_Type0 h_MinusNeg h_MinusZero h_MinusPos = function
| MinusNeg -> h_MinusNeg
| MinusZero -> h_MinusZero
| MinusPos x_1838 -> h_MinusPos x_1838

(** val minusresult_inv_rect_Type4 :
    minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
let minusresult_inv_rect_Type4 hterm h1 h2 h3 =
  let hcut = minusresult_rect_Type4 h1 h2 h3 hterm in hcut __

(** val minusresult_inv_rect_Type3 :
    minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
let minusresult_inv_rect_Type3 hterm h1 h2 h3 =
  let hcut = minusresult_rect_Type3 h1 h2 h3 hterm in hcut __

(** val minusresult_inv_rect_Type2 :
    minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
let minusresult_inv_rect_Type2 hterm h1 h2 h3 =
  let hcut = minusresult_rect_Type2 h1 h2 h3 hterm in hcut __

(** val minusresult_inv_rect_Type1 :
    minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
let minusresult_inv_rect_Type1 hterm h1 h2 h3 =
  let hcut = minusresult_rect_Type1 h1 h2 h3 hterm in hcut __

(** val minusresult_inv_rect_Type0 :
    minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
let minusresult_inv_rect_Type0 hterm h1 h2 h3 =
  let hcut = minusresult_rect_Type0 h1 h2 h3 hterm in hcut __

(** val minusresult_discr : minusresult -> minusresult -> __ **)
let minusresult_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | MinusNeg -> Obj.magic (fun _ dH -> dH)
     | MinusZero -> Obj.magic (fun _ dH -> dH)
     | MinusPos a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val partial_minus : pos -> pos -> minusresult **)
let rec partial_minus n m =
  match n with
  | One ->
    (match m with
     | One -> MinusZero
     | P1 x -> MinusNeg
     | P0 x -> MinusNeg)
  | P1 n' ->
    (match m with
     | One -> MinusPos (P0 n')
     | P1 m' ->
       (match partial_minus n' m' with
        | MinusNeg -> MinusNeg
        | MinusZero -> MinusZero
        | MinusPos p -> MinusPos (P0 p))
     | P0 m' ->
       (match partial_minus n' m' with
        | MinusNeg -> MinusNeg
        | MinusZero -> MinusPos One
        | MinusPos p -> MinusPos (P1 p)))
  | P0 n' ->
    (match m with
     | One -> MinusPos (pred n)
     | P1 m' ->
       (match partial_minus n' m' with
        | MinusNeg -> MinusNeg
        | MinusZero -> MinusNeg
        | MinusPos p -> MinusPos (pred (P0 p)))
     | P0 m' ->
       (match partial_minus n' m' with
        | MinusNeg -> MinusNeg
        | MinusZero -> MinusZero
        | MinusPos p -> MinusPos (P0 p)))

(** val minus : pos -> pos -> pos **)
let minus n m =
  match partial_minus n m with
  | MinusNeg -> One
  | MinusZero -> One
  | MinusPos p -> p

(** val eqb : pos -> pos -> Bool.bool **)
let rec eqb n m =
  match n with
  | One ->
    (match m with
     | One -> Bool.True
     | P1 x -> Bool.False
     | P0 x -> Bool.False)
  | P1 p ->
    (match m with
     | One -> Bool.False
     | P1 q -> eqb p q
     | P0 x -> Bool.False)
  | P0 p ->
    (match m with
     | One -> Bool.False
     | P1 x -> Bool.False
     | P0 q -> eqb p q)

(** val eqb_elim : pos -> pos -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let eqb_elim n m x x0 =
  pos_rect_Type1 (fun m0 ->
    match m0 with
    | One -> (fun _ auto auto' -> auto __)
    | P1 m' -> (fun _ t f -> f __)
    | P0 m' -> (fun _ t f -> f __)) (fun n' iH m0 ->
    match m0 with
    | One -> (fun _ t f -> f __)
    | P1 m' -> (fun _ t f -> iH m' __ (fun _ -> t __) (fun _ -> f __))
    | P0 m' -> (fun _ t f -> f __)) (fun n' iH m0 ->
    match m0 with
    | One -> (fun _ t f -> f __)
    | P1 m' -> (fun _ t f -> f __)
    | P0 m' -> (fun _ t f -> iH m' __ (fun _ -> t __) (fun _ -> f __))) n m
    __ x x0

(** val leb : pos -> pos -> Bool.bool **)
let rec leb n m =
  match partial_minus n m with
  | MinusNeg -> Bool.True
  | MinusZero -> Bool.True
  | MinusPos x -> Bool.False

(** val pos_compare : pos -> pos -> compare **)
let pos_compare n m =
  match partial_minus n m with
  | MinusNeg -> LT
  | MinusZero -> EQ
  | MinusPos x -> GT

(** val two_power_nat : Nat.nat -> pos **)
let rec two_power_nat = function
| Nat.O -> One
| Nat.S n' -> P0 (two_power_nat n')

(** val two_power_pos : pos -> pos **)
let two_power_pos p =
  two_power_nat (nat_of_pos p)

(** val max : pos -> pos -> pos **)
let max n m =
  match leb n m with
  | Bool.True -> m
  | Bool.False -> n