module T: functor (Sig : SIG) -> Can.T
Specification of a theory with a single AC symbol by
means of canonizers and ground completion functions.
The canonizers are obtained from
Make(Sig) and the
completion functions perform forward chaining on
x' = z*u, y = x*v, x =v x' ==> y = z*u*v.
val th : Th.t
val map : (Term.t -> Term.t) -> Term.t -> Term.t
val sigma : Sym.t -> Term.t list -> Term.t
val of_equal : Fact.Equal.t -> Can.config -> Fact.Equal.t list
val of_var_equal : Fact.Equal.t -> Can.config -> Fact.Equal.t list
val of_var_diseq : Fact.Diseq.t -> Can.config -> Fact.Equal.t list
val disjunction : Can.config -> Clause.t