sig
  module type ORDERED =
    sig
      type t
      module E : LogtkIndex.EQUATION
      val empty : ord:LogtkOrdering.t -> LogtkRewriting.ORDERED.t
      val add : LogtkRewriting.ORDERED.t -> E.t -> LogtkRewriting.ORDERED.t
      val add_seq :
        LogtkRewriting.ORDERED.t ->
        E.t Sequence.t -> LogtkRewriting.ORDERED.t
      val add_list :
        LogtkRewriting.ORDERED.t -> E.t list -> LogtkRewriting.ORDERED.t
      val to_seq : LogtkRewriting.ORDERED.t -> E.t Sequence.t
      val size : LogtkRewriting.ORDERED.t -> int
      val mk_rewrite :
        LogtkRewriting.ORDERED.t ->
        size:int -> LogtkFOTerm.t -> LogtkFOTerm.t
    end
  module MakeOrdered :
    functor
      (E : sig
             type t
             type rhs = LogtkFOTerm.t
             val compare : t -> t -> int
             val extract : t -> LogtkIndex.term * rhs * bool
             val priority : t -> int
           end->
      sig
        type t
        module E :
          sig
            type t = E.t
            type rhs = LogtkFOTerm.t
            val compare : t -> t -> int
            val extract : t -> LogtkIndex.term * rhs * bool
            val priority : t -> int
          end
        val empty : ord:LogtkOrdering.t -> t
        val add : t -> E.t -> t
        val add_seq : t -> E.t Sequence.t -> t
        val add_list : t -> E.t list -> t
        val to_seq : t -> E.t Sequence.t
        val size : t -> int
        val mk_rewrite : t -> size:int -> LogtkFOTerm.t -> LogtkFOTerm.t
      end
  module type SIG_TRS =
    sig
      type t
      type rule = LogtkFOTerm.t * LogtkFOTerm.t
      val empty : unit -> LogtkRewriting.SIG_TRS.t
      val add :
        LogtkRewriting.SIG_TRS.t ->
        LogtkRewriting.SIG_TRS.rule -> LogtkRewriting.SIG_TRS.t
      val add_seq :
        LogtkRewriting.SIG_TRS.t ->
        LogtkRewriting.SIG_TRS.rule Sequence.t -> LogtkRewriting.SIG_TRS.t
      val add_list :
        LogtkRewriting.SIG_TRS.t ->
        LogtkRewriting.SIG_TRS.rule list -> LogtkRewriting.SIG_TRS.t
      val to_seq :
        LogtkRewriting.SIG_TRS.t -> LogtkRewriting.SIG_TRS.rule Sequence.t
      val of_seq :
        LogtkRewriting.SIG_TRS.rule Sequence.t -> LogtkRewriting.SIG_TRS.t
      val of_list :
        LogtkRewriting.SIG_TRS.rule list -> LogtkRewriting.SIG_TRS.t
      val size : LogtkRewriting.SIG_TRS.t -> int
      val iter :
        LogtkRewriting.SIG_TRS.t ->
        (LogtkRewriting.SIG_TRS.rule -> unit) -> unit
      val rule_to_form : LogtkRewriting.SIG_TRS.rule -> LogtkFormula.FO.t
      val rewrite_collect :
        LogtkRewriting.SIG_TRS.t ->
        LogtkFOTerm.t -> LogtkFOTerm.t * LogtkRewriting.SIG_TRS.rule list
      val rewrite :
        LogtkRewriting.SIG_TRS.t -> LogtkFOTerm.t -> LogtkFOTerm.t
    end
  module MakeTRS :
    functor
      (I : functor (E : LogtkIndex.EQUATION->
             sig
               type t
               module E :
                 sig
                   type t = E.t
                   type rhs = E.rhs
                   val compare : t -> t -> int
                   val extract : t -> LogtkIndex.term * rhs * bool
                   val priority : t -> int
                 end
               type rhs = E.rhs
               val empty : unit -> t
               val is_empty : t -> bool
               val add : t -> E.t -> t
               val add_seq : t -> E.t Sequence.t -> t
               val remove : t -> E.t -> t
               val remove_seq : t -> E.t Sequence.t -> t
               val size : t -> int
               val iter : t -> (LogtkIndex.term -> E.t -> unit) -> unit
               val retrieve :
                 ?allow_open:bool ->
                 ?subst:LogtkIndex.subst ->
                 sign:bool ->
                 t ->
                 LogtkIndex.scope ->
                 LogtkIndex.term ->
                 LogtkIndex.scope ->
                 '->
                 ('->
                  LogtkIndex.term -> rhs -> E.t -> LogtkIndex.subst -> 'a) ->
                 'a
               val to_dot : Buffer.t -> t -> unit
             end->
      SIG_TRS
  module TRS : SIG_TRS
  module FormRW :
    sig
      type t
      type form = LogtkFormula.FO.t
      type rule = LogtkFOTerm.t * LogtkRewriting.FormRW.form
      val empty : unit -> LogtkRewriting.FormRW.t
      val add :
        LogtkRewriting.FormRW.t ->
        LogtkRewriting.FormRW.rule -> LogtkRewriting.FormRW.t
      val add_seq :
        LogtkRewriting.FormRW.t ->
        LogtkRewriting.FormRW.rule Sequence.t -> LogtkRewriting.FormRW.t
      val add_list :
        LogtkRewriting.FormRW.t ->
        LogtkRewriting.FormRW.rule list -> LogtkRewriting.FormRW.t
      val add_term_rule :
        LogtkRewriting.FormRW.t ->
        LogtkFOTerm.t * LogtkFOTerm.t -> LogtkRewriting.FormRW.t
      val add_term_rules :
        LogtkRewriting.FormRW.t ->
        (LogtkFOTerm.t * LogtkFOTerm.t) list -> LogtkRewriting.FormRW.t
      val to_seq :
        LogtkRewriting.FormRW.t -> LogtkRewriting.FormRW.rule Sequence.t
      val of_seq :
        LogtkRewriting.FormRW.rule Sequence.t -> LogtkRewriting.FormRW.t
      val of_list :
        LogtkRewriting.FormRW.rule list -> LogtkRewriting.FormRW.t
      val size : LogtkRewriting.FormRW.t -> int
      val iter :
        LogtkRewriting.FormRW.t ->
        (LogtkRewriting.FormRW.rule -> unit) -> unit
      val rule_to_form :
        LogtkRewriting.FormRW.rule -> LogtkRewriting.FormRW.form
      val rewrite_collect :
        LogtkRewriting.FormRW.t ->
        LogtkRewriting.FormRW.form ->
        LogtkRewriting.FormRW.form * LogtkRewriting.FormRW.rule list
      val rewrite :
        LogtkRewriting.FormRW.t ->
        LogtkRewriting.FormRW.form -> LogtkRewriting.FormRW.form
    end
end