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

val property_lattice_rect_Type5 :
  (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
  Bool.bool) -> 'a1) -> property_lattice -> 'a1

val property_lattice_rect_Type3 :
  (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
  Bool.bool) -> 'a1) -> property_lattice -> 'a1

val property_lattice_rect_Type2 :
  (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
  Bool.bool) -> 'a1) -> property_lattice -> 'a1

val property_lattice_rect_Type1 :
  (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
  Bool.bool) -> 'a1) -> property_lattice -> 'a1

val property_lattice_rect_Type0 :
  (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
  Bool.bool) -> 'a1) -> property_lattice -> 'a1

type l_property 

val l_bottom : property_lattice -> __

val l_equal : property_lattice -> __ -> __ -> Bool.bool

val l_included : property_lattice -> __ -> __ -> Bool.bool

val l_is_maximal : property_lattice -> __ -> Bool.bool

val property_lattice_inv_rect_Type4 :
  property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
  Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1

val property_lattice_inv_rect_Type3 :
  property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
  Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1

val property_lattice_inv_rect_Type2 :
  property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
  Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1

val property_lattice_inv_rect_Type1 :
  property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
  Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1

val property_lattice_inv_rect_Type0 :
  property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
  Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1

val property_lattice_jmdiscr : property_lattice -> property_lattice -> __

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

val fixpoint_rect_Type5 :
  property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
  'a1

val fixpoint_rect_Type3 :
  property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
  'a1

val fixpoint_rect_Type2 :
  property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
  'a1

val fixpoint_rect_Type1 :
  property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
  'a1

val fixpoint_rect_Type0 :
  property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
  'a1

val fix_lfp : property_lattice -> equations -> fixpoint -> valuation

val fixpoint_inv_rect_Type4 :
  property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
  -> 'a1

val fixpoint_inv_rect_Type3 :
  property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
  -> 'a1

val fixpoint_inv_rect_Type2 :
  property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
  -> 'a1

val fixpoint_inv_rect_Type1 :
  property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
  -> 'a1

val fixpoint_inv_rect_Type0 :
  property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
  -> 'a1

val fixpoint_discr :
  property_lattice -> equations -> fixpoint -> fixpoint -> __

val fixpoint_jmdiscr :
  property_lattice -> equations -> fixpoint -> fixpoint -> __

val dpi1__o__fix_lfp__o__inject :
  property_lattice -> equations -> (fixpoint, 'a1) Types.dPair -> valuation
  Types.sig0

val eject__o__fix_lfp__o__inject :
  property_lattice -> equations -> fixpoint Types.sig0 -> valuation
  Types.sig0

val fix_lfp__o__inject :
  property_lattice -> equations -> fixpoint -> valuation Types.sig0

val dpi1__o__fix_lfp :
  property_lattice -> equations -> (fixpoint, 'a1) Types.dPair -> valuation

val eject__o__fix_lfp :
  property_lattice -> equations -> fixpoint Types.sig0 -> valuation

type fixpoint_computer = property_lattice -> equations -> fixpoint

val dpi1__o__apply_fixpoint :
  property_lattice -> equations -> (fixpoint, 'a1) Types.dPair ->
  Graphs.label -> __

val eject__o__apply_fixpoint :
  property_lattice -> equations -> fixpoint Types.sig0 -> Graphs.label -> __