sig
  module Mode :
    sig
      type t = No | Dep
      val of_string : string -> Jst.Mode.t
      val to_string : Jst.Mode.t -> string
      val is_none : unit -> bool
      val get : unit -> Jst.Mode.t
      val set : Jst.Mode.t -> unit
    end
  type t
  val pp : Jst.t Pretty.printer
  val axioms_of : Jst.t -> Atom.Set.t
  val of_axioms : Atom.Set.t -> Jst.t
  exception Inconsistent of Jst.t
  val axiom : Atom.t -> Jst.t
  val dep0 : Jst.t
  val dep1 : Jst.t -> Jst.t
  val dep2 : Jst.t -> Jst.t -> Jst.t
  val dep3 : Jst.t -> Jst.t -> Jst.t -> Jst.t
  val dep4 : Jst.t -> Jst.t -> Jst.t -> Jst.t -> Jst.t
  val dep5 : Jst.t -> Jst.t -> Jst.t -> Jst.t -> Jst.t -> Jst.t
  val dep : Jst.t list -> Jst.t
  type jst = Jst.t
  module Three :
    sig
      type t = Yes of Jst.jst | No of Jst.jst | X
      val to_three :
        Jst.jst list Pervasives.ref ->
        ('a -> 'b -> Jst.Three.t) -> 'a -> 'b -> Three.t
      val of_three : ('a -> Three.t) -> 'a -> Jst.Three.t
    end
  module Eqtrans :
    sig
      type t = Term.t -> Term.t * Jst.jst
      val id : Jst.Eqtrans.t
      val compose : Jst.Eqtrans.t -> Jst.Eqtrans.t -> Jst.Eqtrans.t
      val compose3 :
        Jst.Eqtrans.t -> Jst.Eqtrans.t -> Jst.Eqtrans.t -> Jst.Eqtrans.t
      val totalize : Jst.Eqtrans.t -> Jst.Eqtrans.t
      val compose_partial1 : Jst.Eqtrans.t -> Jst.Eqtrans.t -> Jst.Eqtrans.t
      val replace : Term.map -> Jst.Eqtrans.t -> Jst.Eqtrans.t
      val apply : Term.apply -> (Term.t * Term.t) * Jst.jst -> Jst.Eqtrans.t
      val pointwise : Jst.Eqtrans.t -> Term.t list -> Term.t list * Jst.jst
      val mapargs :
        (Sym.t -> Term.t list -> Term.t * Jst.jst) ->
        (Sym.t -> Jst.Eqtrans.t) -> Jst.Eqtrans.t
      val trace : Trace.level -> string -> Jst.Eqtrans.t -> Jst.Eqtrans.t
    end
  module Pred :
    sig
      type t = Term.t -> Jst.jst option
      val disj : Jst.Pred.t -> Jst.Pred.t -> Jst.Pred.t
      val apply : Jst.Eqtrans.t -> Jst.Pred.t -> Jst.Pred.t
      val trace : Trace.level -> string -> Jst.Pred.t -> Jst.Pred.t
    end
  module Pred2 :
    sig
      type t = Term.t -> Term.t -> Jst.jst option
      val apply : Jst.Eqtrans.t -> Jst.Pred2.t -> Jst.Pred2.t
      val orelse : Jst.Pred2.t -> Jst.Pred2.t -> Jst.Pred2.t
      val inj : (Term.t -> Term.t -> bool) -> Jst.Pred2.t
      val trace : Trace.level -> string -> Jst.Pred2.t -> Jst.Pred2.t
    end
  module Rel1 :
    sig
      type t = Term.t -> Jst.Three.t
      val apply : Jst.Eqtrans.t -> Jst.Rel1.t -> Jst.Rel1.t
      val orelse : Jst.Rel1.t -> Jst.Rel1.t -> Jst.Rel1.t
      val yes_or_no : Jst.Pred.t -> Jst.Pred.t -> Jst.Rel1.t
      val trace : Trace.level -> string -> Jst.Rel1.t -> Jst.Rel1.t
    end
  module Rel2 :
    sig
      type t = Term.t -> Term.t -> Jst.Three.t
      val apply : Jst.Eqtrans.t -> Jst.Rel2.t -> Jst.Rel2.t
      val orelse : Jst.Rel2.t -> Jst.Rel2.t -> Jst.Rel2.t
      val yes : Jst.Pred2.t -> Jst.Rel2.t
      val no : Jst.Pred2.t -> Jst.Rel2.t
      val yes_or_no : Jst.Pred2.t -> Jst.Pred2.t -> Jst.Rel2.t
      val trace : Trace.level -> string -> Jst.Rel2.t -> Jst.Rel2.t
    end
end