open Preamble

open Exp

open Arithmetic

open Integers

open AST

open Proper

open PositiveMap

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Positive

open Identifiers

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 BitVectorTrie

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Graphs

type property_lattice = { l_bottom : __; l_equal : (__ -> __ -> Bool.bool);
                          l_included : (__ -> __ -> Bool.bool);
                          l_is_maximal : (__ -> Bool.bool) }

(** val property_lattice_rect_Type4 :
    (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
    Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
let rec property_lattice_rect_Type4 h_mk_property_lattice x_18885 =
  let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
    l_is_maximal = l_is_maximal0 } = x_18885
  in
  h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0

(** val property_lattice_rect_Type5 :
    (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
    Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
let rec property_lattice_rect_Type5 h_mk_property_lattice x_18887 =
  let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
    l_is_maximal = l_is_maximal0 } = x_18887
  in
  h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0

(** val property_lattice_rect_Type3 :
    (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
    Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
let rec property_lattice_rect_Type3 h_mk_property_lattice x_18889 =
  let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
    l_is_maximal = l_is_maximal0 } = x_18889
  in
  h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0

(** val property_lattice_rect_Type2 :
    (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
    Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
let rec property_lattice_rect_Type2 h_mk_property_lattice x_18891 =
  let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
    l_is_maximal = l_is_maximal0 } = x_18891
  in
  h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0

(** val property_lattice_rect_Type1 :
    (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
    Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
let rec property_lattice_rect_Type1 h_mk_property_lattice x_18893 =
  let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
    l_is_maximal = l_is_maximal0 } = x_18893
  in
  h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0

(** val property_lattice_rect_Type0 :
    (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
    Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
let rec property_lattice_rect_Type0 h_mk_property_lattice x_18895 =
  let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
    l_is_maximal = l_is_maximal0 } = x_18895
  in
  h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0

type l_property = __

(** val l_bottom : property_lattice -> __ **)
let rec l_bottom xxx =
  xxx.l_bottom

(** val l_equal : property_lattice -> __ -> __ -> Bool.bool **)
let rec l_equal xxx =
  xxx.l_equal

(** val l_included : property_lattice -> __ -> __ -> Bool.bool **)
let rec l_included xxx =
  xxx.l_included

(** val l_is_maximal : property_lattice -> __ -> Bool.bool **)
let rec l_is_maximal xxx =
  xxx.l_is_maximal

(** val property_lattice_inv_rect_Type4 :
    property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
    Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1 **)
let property_lattice_inv_rect_Type4 hterm h1 =
  let hcut = property_lattice_rect_Type4 h1 hterm in hcut __

(** val property_lattice_inv_rect_Type3 :
    property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
    Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1 **)
let property_lattice_inv_rect_Type3 hterm h1 =
  let hcut = property_lattice_rect_Type3 h1 hterm in hcut __

(** val property_lattice_inv_rect_Type2 :
    property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
    Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1 **)
let property_lattice_inv_rect_Type2 hterm h1 =
  let hcut = property_lattice_rect_Type2 h1 hterm in hcut __

(** val property_lattice_inv_rect_Type1 :
    property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
    Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1 **)
let property_lattice_inv_rect_Type1 hterm h1 =
  let hcut = property_lattice_rect_Type1 h1 hterm in hcut __

(** val property_lattice_inv_rect_Type0 :
    property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
    Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1 **)
let property_lattice_inv_rect_Type0 hterm h1 =
  let hcut = property_lattice_rect_Type0 h1 hterm in hcut __

(** val property_lattice_jmdiscr :
    property_lattice -> property_lattice -> __ **)
let property_lattice_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { l_bottom = a1; l_equal = a2; l_included = a3; l_is_maximal =
       a4 } = x
     in
    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y

type valuation = Graphs.label -> __

type rhs = valuation -> __

type equations = Graphs.label -> rhs

type fixpoint =
  valuation
  (* singleton inductive, whose constructor was mk_fixpoint *)

(** val fixpoint_rect_Type4 :
    property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
    'a1 **)
let rec fixpoint_rect_Type4 latt eqs h_mk_fixpoint x_18916 =
  let fix_lfp = x_18916 in h_mk_fixpoint fix_lfp __

(** val fixpoint_rect_Type5 :
    property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
    'a1 **)
let rec fixpoint_rect_Type5 latt eqs h_mk_fixpoint x_18918 =
  let fix_lfp = x_18918 in h_mk_fixpoint fix_lfp __

(** val fixpoint_rect_Type3 :
    property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
    'a1 **)
let rec fixpoint_rect_Type3 latt eqs h_mk_fixpoint x_18920 =
  let fix_lfp = x_18920 in h_mk_fixpoint fix_lfp __

(** val fixpoint_rect_Type2 :
    property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
    'a1 **)
let rec fixpoint_rect_Type2 latt eqs h_mk_fixpoint x_18922 =
  let fix_lfp = x_18922 in h_mk_fixpoint fix_lfp __

(** val fixpoint_rect_Type1 :
    property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
    'a1 **)
let rec fixpoint_rect_Type1 latt eqs h_mk_fixpoint x_18924 =
  let fix_lfp = x_18924 in h_mk_fixpoint fix_lfp __

(** val fixpoint_rect_Type0 :
    property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
    'a1 **)
let rec fixpoint_rect_Type0 latt eqs h_mk_fixpoint x_18926 =
  let fix_lfp = x_18926 in h_mk_fixpoint fix_lfp __

(** val fix_lfp : property_lattice -> equations -> fixpoint -> valuation **)
let rec fix_lfp latt eqs xxx =
  let yyy = xxx in yyy

(** val fixpoint_inv_rect_Type4 :
    property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ ->
    'a1) -> 'a1 **)
let fixpoint_inv_rect_Type4 x1 x2 hterm h1 =
  let hcut = fixpoint_rect_Type4 x1 x2 h1 hterm in hcut __

(** val fixpoint_inv_rect_Type3 :
    property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ ->
    'a1) -> 'a1 **)
let fixpoint_inv_rect_Type3 x1 x2 hterm h1 =
  let hcut = fixpoint_rect_Type3 x1 x2 h1 hterm in hcut __

(** val fixpoint_inv_rect_Type2 :
    property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ ->
    'a1) -> 'a1 **)
let fixpoint_inv_rect_Type2 x1 x2 hterm h1 =
  let hcut = fixpoint_rect_Type2 x1 x2 h1 hterm in hcut __

(** val fixpoint_inv_rect_Type1 :
    property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ ->
    'a1) -> 'a1 **)
let fixpoint_inv_rect_Type1 x1 x2 hterm h1 =
  let hcut = fixpoint_rect_Type1 x1 x2 h1 hterm in hcut __

(** val fixpoint_inv_rect_Type0 :
    property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ ->
    'a1) -> 'a1 **)
let fixpoint_inv_rect_Type0 x1 x2 hterm h1 =
  let hcut = fixpoint_rect_Type0 x1 x2 h1 hterm in hcut __

(** val fixpoint_discr :
    property_lattice -> equations -> fixpoint -> fixpoint -> __ **)
let fixpoint_discr a1 a2 x y =
  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y

(** val fixpoint_jmdiscr :
    property_lattice -> equations -> fixpoint -> fixpoint -> __ **)
let fixpoint_jmdiscr a1 a2 x y =
  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y

(** val dpi1__o__fix_lfp__o__inject :
    property_lattice -> equations -> (fixpoint, 'a1) Types.dPair -> valuation
    Types.sig0 **)
let dpi1__o__fix_lfp__o__inject x0 x2 x4 =
  fix_lfp x0 x2 x4.Types.dpi1

(** val eject__o__fix_lfp__o__inject :
    property_lattice -> equations -> fixpoint Types.sig0 -> valuation
    Types.sig0 **)
let eject__o__fix_lfp__o__inject x0 x2 x4 =
  fix_lfp x0 x2 (Types.pi1 x4)

(** val fix_lfp__o__inject :
    property_lattice -> equations -> fixpoint -> valuation Types.sig0 **)
let fix_lfp__o__inject x0 x2 x3 =
  fix_lfp x0 x2 x3

(** val dpi1__o__fix_lfp :
    property_lattice -> equations -> (fixpoint, 'a1) Types.dPair -> valuation **)
let dpi1__o__fix_lfp x0 x1 x3 =
  fix_lfp x0 x1 x3.Types.dpi1

(** val eject__o__fix_lfp :
    property_lattice -> equations -> fixpoint Types.sig0 -> valuation **)
let eject__o__fix_lfp x0 x1 x3 =
  fix_lfp x0 x1 (Types.pi1 x3)

type fixpoint_computer = property_lattice -> equations -> fixpoint

(** val dpi1__o__apply_fixpoint :
    property_lattice -> equations -> (fixpoint, 'a1) Types.dPair ->
    Graphs.label -> __ **)
let dpi1__o__apply_fixpoint x0 x1 x3 =
  let latt = x0 in
  let eqs = x1 in let f = x3.Types.dpi1 in (fun l -> fix_lfp latt eqs f l)

(** val eject__o__apply_fixpoint :
    property_lattice -> equations -> fixpoint Types.sig0 -> Graphs.label ->
    __ **)
let eject__o__apply_fixpoint x0 x1 x3 =
  let latt = x0 in
  let eqs = x1 in let f = Types.pi1 x3 in (fun l -> fix_lfp latt eqs f l)