sig   module Z :     sig       type t = Integer.t       val zero : t       val one : t       val minus_one : t       val succ : t -> t       val pred : t -> t       val neg : t -> t       val add : t -> t -> t       val sub : t -> t -> t       val mul : t -> t -> t       val div : t -> t -> t       val rem : t -> t -> t       val div_rem : t -> t -> t * t       val equal : t -> t -> bool       val leq : t -> t -> bool       val lt : t -> t -> bool       val of_int : int -> t       val of_string : string -> t       val to_string : t -> string       val hash : t -> int       val compare : t -> t -> int     end   module ADT :     sig       type t = adt       val hash : t -> int       val equal : t -> t -> bool       val compare : t -> t -> int       val pretty : Format.formatter -> t -> unit       val debug : t -> string       val basename : t -> string     end   module Field :     sig       type t = field       val hash : t -> int       val equal : t -> t -> bool       val compare : t -> t -> int       val pretty : Format.formatter -> t -> unit       val debug : t -> string       val sort : t -> Qed.Logic.sort     end   module Fun :     sig       type t = lfun       val hash : t -> int       val equal : t -> t -> bool       val compare : t -> t -> int       val pretty : Format.formatter -> t -> unit       val debug : t -> string       val category : t -> t Qed.Logic.category       val params : t -> Qed.Logic.sort list       val sort : t -> Qed.Logic.sort     end   module Var : Qed.Logic.Variable   type term   type bind   type var = Var.t   type tau = (Field.t, ADT.t) Qed.Logic.datatype   type signature = (Field.t, ADT.t) Qed.Logic.funtype   module Tau :     sig       type t = tau       val hash : t -> int       val equal : t -> t -> bool       val compare : t -> t -> int       val pretty : Format.formatter -> t -> unit       val debug : t -> string       val basename : t -> string     end   module Vars :     sig       type elt = var       type t       val empty : t       val is_empty : t -> bool       val mem : elt -> t -> bool       val find : elt -> t -> elt       val add : elt -> t -> t       val singleton : elt -> t       val remove : elt -> t -> t       val union : t -> t -> t       val inter : t -> t -> t       val diff : t -> t -> t       val compare : t -> t -> int       val equal : t -> t -> bool       val subset : t -> t -> bool       val iter : (elt -> unit) -> t -> unit       val fold : (elt -> '-> 'a) -> t -> '-> 'a       val for_all : (elt -> bool) -> t -> bool       val exists : (elt -> bool) -> t -> bool       val filter : (elt -> bool) -> t -> t       val partition : (elt -> bool) -> t -> t * t       val cardinal : t -> int       val elements : t -> elt list       val map : (elt -> elt) -> t -> t       val mapf : (elt -> elt option) -> t -> t       val intersect : t -> t -> bool     end   module Vmap :     sig       type key = var       type 'a t       val is_empty : 'a t -> bool       val empty : 'a t       val add : key -> '-> 'a t -> 'a t       val mem : key -> 'a t -> bool       val find : key -> 'a t -> 'a       val remove : key -> 'a t -> 'a t       val compare : ('-> '-> int) -> 'a t -> 'a t -> int       val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool       val iter : (key -> '-> unit) -> 'a t -> unit       val map : (key -> '-> 'b) -> 'a t -> 'b t       val mapf : (key -> '-> 'b option) -> 'a t -> 'b t       val mapq : (key -> '-> 'a option) -> 'a t -> 'a t       val filter : (key -> '-> bool) -> 'a t -> 'a t       val partition : (key -> '-> bool) -> 'a t -> 'a t * 'a t       val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b       val union : (key -> '-> '-> 'a) -> 'a t -> 'a t -> 'a t       val inter : (key -> '-> '-> 'c) -> 'a t -> 'b t -> 'c t       val interf : (key -> '-> '-> 'c option) -> 'a t -> 'b t -> 'c t       val interq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t       val diffq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t       val merge :         (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t       val insert : (key -> '-> '-> 'a) -> key -> '-> 'a t -> 'a t       val change :         (key -> '-> 'a option -> 'a option) -> key -> '-> 'a t -> 'a t     end   type pool   val pool : ?copy:pool -> unit -> pool   val add_var : pool -> var -> unit   val add_vars : pool -> Vars.t -> unit   val add_term : pool -> term -> unit   val fresh : pool -> ?basename:string -> tau -> var   val alpha : pool -> var -> var   val tau_of_var : var -> tau   val sort_of_var : var -> Qed.Logic.sort   val base_of_var : var -> string   type 'a expression =       (Z.t, Field.t, ADT.t, Fun.t, var, bind, 'a) Qed.Logic.term_repr   type repr = term expression   type path = int list   type record = (Field.t * term) list   val decide : term -> bool   val is_true : term -> Qed.Logic.maybe   val is_false : term -> Qed.Logic.maybe   val is_prop : term -> bool   val is_int : term -> bool   val is_real : term -> bool   val is_arith : term -> bool   val are_equal : term -> term -> Qed.Logic.maybe   val eval_eq : term -> term -> bool   val eval_neq : term -> term -> bool   val eval_lt : term -> term -> bool   val eval_leq : term -> term -> bool   val repr : term -> repr   val sort : term -> Qed.Logic.sort   val vars : term -> Vars.t   val subterm : term -> path -> term   val change_subterm : term -> path -> term -> term   val e_true : term   val e_false : term   val e_bool : bool -> term   val e_literal : bool -> term -> term   val e_int : int -> term   val e_zint : Z.t -> term   val e_real : Qed.R.t -> term   val e_var : var -> term   val e_opp : term -> term   val e_times : Z.t -> term -> term   val e_sum : term list -> term   val e_prod : term list -> term   val e_add : term -> term -> term   val e_sub : term -> term -> term   val e_mul : term -> term -> term   val e_div : term -> term -> term   val e_mod : term -> term -> term   val e_eq : term -> term -> term   val e_neq : term -> term -> term   val e_leq : term -> term -> term   val e_lt : term -> term -> term   val e_imply : term list -> term -> term   val e_equiv : term -> term -> term   val e_and : term list -> term   val e_or : term list -> term   val e_not : term -> term   val e_if : term -> term -> term -> term   val e_get : term -> term -> term   val e_set : term -> term -> term -> term   val e_getfield : term -> Field.t -> term   val e_record : record -> term   val e_fun : Fun.t -> term list -> term   val e_repr : repr -> term   val e_forall : var list -> term -> term   val e_exists : var list -> term -> term   val e_lambda : var list -> term -> term   val e_bind : Qed.Logic.binder -> var -> term -> term   val e_apply : term -> term list -> term   type sigma   val sigma : unit -> sigma   val e_subst_var : var -> term -> term -> term   val lc_bind : var -> term -> bind   val lc_open : var -> bind -> term   val lc_open_term : term -> bind -> term   val lc_closed : term -> bool   val lc_closed_at : int -> term -> bool   val lc_vars : term -> Qed.Bvars.t   val lc_repr : bind -> term   val e_map : pool -> (term -> term) -> term -> term   val e_iter : pool -> (term -> unit) -> term -> unit   val f_map : (int -> term -> term) -> int -> term -> term   val f_iter : (int -> term -> unit) -> int -> term -> unit   val lc_map : (term -> term) -> term -> term   val lc_iter : (term -> unit) -> term -> unit   val set_builtin : Fun.t -> (term list -> term) -> unit   val set_builtin_eq : Fun.t -> (term -> term -> term) -> unit   val set_builtin_leq : Fun.t -> (term -> term -> term) -> unit   val consequence : term -> term -> term   val literal : term -> bool * term   val congruence_eq : term -> term -> (term * term) list option   val congruence_neq : term -> term -> (term * term) list option   val flattenable : term -> bool   val flattens : term -> term -> bool   val flatten : term -> term list   val affine : term -> (Z.t, term) Qed.Logic.affine   val record_with : record -> (term * record) option   type t = term   val id : t -> int   val hash : t -> int   val equal : t -> t -> bool   val compare : t -> t -> int   val pretty : Format.formatter -> t -> unit   val weigth : t -> int   val is_closed : t -> bool   val is_simple : t -> bool   val is_atomic : t -> bool   val is_primitive : t -> bool   val is_neutral : Fun.t -> t -> bool   val is_absorbant : Fun.t -> t -> bool   val size : t -> int   val basename : t -> string   val debug : Format.formatter -> t -> unit   val pp_id : Format.formatter -> t -> unit   val pp_rid : Format.formatter -> t -> unit   val pp_repr : Format.formatter -> repr -> unit   module Term :     sig       type t = term       val hash : t -> int       val equal : t -> t -> bool       val compare : t -> t -> int       val pretty : Format.formatter -> t -> unit       val debug : t -> string     end   module Tset :     sig       type elt = term       type t       val empty : t       val is_empty : t -> bool       val mem : elt -> t -> bool       val find : elt -> t -> elt       val add : elt -> t -> t       val singleton : elt -> t       val remove : elt -> t -> t       val union : t -> t -> t       val inter : t -> t -> t       val diff : t -> t -> t       val compare : t -> t -> int       val equal : t -> t -> bool       val subset : t -> t -> bool       val iter : (elt -> unit) -> t -> unit       val fold : (elt -> '-> 'a) -> t -> '-> 'a       val for_all : (elt -> bool) -> t -> bool       val exists : (elt -> bool) -> t -> bool       val filter : (elt -> bool) -> t -> t       val partition : (elt -> bool) -> t -> t * t       val cardinal : t -> int       val elements : t -> elt list       val map : (elt -> elt) -> t -> t       val mapf : (elt -> elt option) -> t -> t       val intersect : t -> t -> bool     end   module Tmap :     sig       type key = term       type 'a t       val is_empty : 'a t -> bool       val empty : 'a t       val add : key -> '-> 'a t -> 'a t       val mem : key -> 'a t -> bool       val find : key -> 'a t -> 'a       val remove : key -> 'a t -> 'a t       val compare : ('-> '-> int) -> 'a t -> 'a t -> int       val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool       val iter : (key -> '-> unit) -> 'a t -> unit       val map : (key -> '-> 'b) -> 'a t -> 'b t       val mapf : (key -> '-> 'b option) -> 'a t -> 'b t       val mapq : (key -> '-> 'a option) -> 'a t -> 'a t       val filter : (key -> '-> bool) -> 'a t -> 'a t       val partition : (key -> '-> bool) -> 'a t -> 'a t * 'a t       val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b       val union : (key -> '-> '-> 'a) -> 'a t -> 'a t -> 'a t       val inter : (key -> '-> '-> 'c) -> 'a t -> 'b t -> 'c t       val interf : (key -> '-> '-> 'c option) -> 'a t -> 'b t -> 'c t       val interq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t       val diffq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t       val merge :         (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t       val insert : (key -> '-> '-> 'a) -> key -> '-> 'a t -> 'a t       val change :         (key -> '-> 'a option -> 'a option) -> key -> '-> 'a t -> 'a t     end   val shared :     ?shared:(term -> bool) ->     ?shareable:(term -> bool) -> term list -> term list   type marks   val marks :     ?shared:(term -> bool) -> ?shareable:(term -> bool) -> unit -> marks   val mark : marks -> term -> unit   val share : marks -> term -> unit   val defs : marks -> term list   type unop = term -> term   type binop = term -> term -> term   val e_zero : term   val e_one : term   val e_minus_one : term   val e_one_real : term   val e_zero_real : term   val constant : term -> term   val e_fact : int -> term -> term   val e_int64 : int64 -> term   val e_bigint : Integer.t -> term   val e_mthfloat : float -> term   val e_hexfloat : float -> term   val e_setfield : term -> Lang.field -> term -> term   val e_range : term -> term -> term   val is_zero : term -> bool   type pred   type cmp = term -> term -> Lang.F.pred   val p_true : Lang.F.pred   val p_false : Lang.F.pred   val p_equal : term -> term -> Lang.F.pred   val p_neq : term -> term -> Lang.F.pred   val p_leq : term -> term -> Lang.F.pred   val p_lt : term -> term -> Lang.F.pred   val p_positive : term -> Lang.F.pred   val is_ptrue : Lang.F.pred -> Qed.Logic.maybe   val is_pfalse : Lang.F.pred -> Qed.Logic.maybe   val is_equal : term -> term -> Qed.Logic.maybe   val eqp : Lang.F.pred -> Lang.F.pred -> bool   val comparep : Lang.F.pred -> Lang.F.pred -> int   val p_bool : term -> Lang.F.pred   val e_prop : Lang.F.pred -> term   val p_bools : term list -> Lang.F.pred list   val e_props : Lang.F.pred list -> term list   val lift : (term -> term) -> Lang.F.pred -> Lang.F.pred   val p_not : Lang.F.pred -> Lang.F.pred   val p_and : Lang.F.pred -> Lang.F.pred -> Lang.F.pred   val p_or : Lang.F.pred -> Lang.F.pred -> Lang.F.pred   val p_imply : Lang.F.pred -> Lang.F.pred -> Lang.F.pred   val p_equiv : Lang.F.pred -> Lang.F.pred -> Lang.F.pred   val p_hyps : Lang.F.pred list -> Lang.F.pred -> Lang.F.pred   val p_if : Lang.F.pred -> Lang.F.pred -> Lang.F.pred -> Lang.F.pred   val p_conj : Lang.F.pred list -> Lang.F.pred   val p_disj : Lang.F.pred list -> Lang.F.pred   val p_any : ('-> Lang.F.pred) -> 'a list -> Lang.F.pred   val p_all : ('-> Lang.F.pred) -> 'a list -> Lang.F.pred   val p_call : Lang.lfun -> term list -> Lang.F.pred   val p_forall : var list -> Lang.F.pred -> Lang.F.pred   val p_exists : var list -> Lang.F.pred -> Lang.F.pred   val p_bind : Qed.Logic.binder -> var -> Lang.F.pred -> Lang.F.pred   val e_subst : ?sigma:sigma -> (term -> term) -> term -> term   val p_subst : ?sigma:sigma -> (term -> term) -> Lang.F.pred -> Lang.F.pred   val e_vars : term -> var list   val p_vars : Lang.F.pred -> var list   val p_close : Lang.F.pred -> Lang.F.pred   val idp : Lang.F.pred -> int   val varsp : Lang.F.pred -> Vars.t   val occurs : var -> term -> bool   val occursp : var -> Lang.F.pred -> bool   val intersect : term -> term -> bool   val intersectp : Lang.F.pred -> Lang.F.pred -> bool   val pp_tau : Format.formatter -> Lang.tau -> unit   val pp_var : Format.formatter -> var -> unit   val pp_vars : Format.formatter -> Vars.t -> unit   val pp_term : Format.formatter -> term -> unit   val pp_pred : Format.formatter -> Lang.F.pred -> unit   val debugp : Format.formatter -> Lang.F.pred -> unit   type env   val env : Vars.t -> Lang.F.env   val marker : Lang.F.env -> marks   val mark_e : marks -> term -> unit   val mark_p : marks -> Lang.F.pred -> unit   val define :     (Lang.F.env -> string -> term -> unit) ->     Lang.F.env -> marks -> Lang.F.env   val pp_eterm : Lang.F.env -> Format.formatter -> term -> unit   val pp_epred : Lang.F.env -> Format.formatter -> Lang.F.pred -> unit   val pred : Lang.F.pred -> Lang.F.pred expression   val epred : Lang.F.pred -> term expression   val p_iter : (Lang.F.pred -> unit) -> (term -> unit) -> Lang.F.pred -> unit   module Pmap :     sig       type key = pred       type 'a t       val is_empty : 'a t -> bool       val empty : 'a t       val add : key -> '-> 'a t -> 'a t       val mem : key -> 'a t -> bool       val find : key -> 'a t -> 'a       val remove : key -> 'a t -> 'a t       val compare : ('-> '-> int) -> 'a t -> 'a t -> int       val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool       val iter : (key -> '-> unit) -> 'a t -> unit       val map : (key -> '-> 'b) -> 'a t -> 'b t       val mapf : (key -> '-> 'b option) -> 'a t -> 'b t       val mapq : (key -> '-> 'a option) -> 'a t -> 'a t       val filter : (key -> '-> bool) -> 'a t -> 'a t       val partition : (key -> '-> bool) -> 'a t -> 'a t * 'a t       val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b       val union : (key -> '-> '-> 'a) -> 'a t -> 'a t -> 'a t       val inter : (key -> '-> '-> 'c) -> 'a t -> 'b t -> 'c t       val interf : (key -> '-> '-> 'c option) -> 'a t -> 'b t -> 'c t       val interq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t       val diffq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t       val merge :         (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t       val insert : (key -> '-> '-> 'a) -> key -> '-> 'a t -> 'a t       val change :         (key -> '-> 'a option -> 'a option) -> key -> '-> 'a t -> 'a t     end   module Pset :     sig       type elt = pred       type t       val empty : t       val is_empty : t -> bool       val mem : elt -> t -> bool       val find : elt -> t -> elt       val add : elt -> t -> t       val singleton : elt -> t       val remove : elt -> t -> t       val union : t -> t -> t       val inter : t -> t -> t       val diff : t -> t -> t       val compare : t -> t -> int       val equal : t -> t -> bool       val subset : t -> t -> bool       val iter : (elt -> unit) -> t -> unit       val fold : (elt -> '-> 'a) -> t -> '-> 'a       val for_all : (elt -> bool) -> t -> bool       val exists : (elt -> bool) -> t -> bool       val filter : (elt -> bool) -> t -> t       val partition : (elt -> bool) -> t -> t * t       val cardinal : t -> int       val elements : t -> elt list       val map : (elt -> elt) -> t -> t       val mapf : (elt -> elt option) -> t -> t       val intersect : t -> t -> bool     end   val release : unit -> unit   val set_builtin_1 : Lang.lfun -> (term -> term) -> unit   val set_builtin_2 : Lang.lfun -> (term -> term -> term) -> unit   val set_builtin_eqp : Lang.lfun -> (term -> term -> Lang.F.pred) -> unit   module Check :     sig       val reset : unit -> unit       val set : string -> unit       val is_set : unit -> bool       val iter : (qed:term -> raw:term -> goal:Lang.F.pred -> unit) -> unit     end end