plus

Creates a new Substitution that is the composition (a.k.a. union) of this and other. The composition is not guaranteed to be a Substitution.Unifier, even if both arguments are. In fact, the composition algorithm performs the following checks:

• If one of arguments is of type Substitution.Fail, the result is of type Substitution.Fail

• If the set of assignments attained by composing the two substitutions is contradictory -- i.e., if the same Var is assigned to different Terms --, the result is of type Substitution.Fail

• Otherwise, the result is an instance of Substitution.Unifier

Regardless of its type, the resulting Substitution will contain the tags of both input Substitutions.

Creates a new Substitution that is the composition (a.k.a. union) of this and other. The composition is not guaranteed to be a Substitution.Unifier, even if both arguments are. In fact, the composition algorithm performs the following checks:

• If one of arguments is of type Substitution.Fail, the result is of type Substitution.Fail

• If the set of assignments attained by composing the two substitutions is contradictory -- i.e., if the same Var is assigned to different Terms --, the result is of type Substitution.Fail

• Otherwise, the result is an instance of Substitution.Unifier

Regardless of its type, the resulting Substitution will contain the tags attained by merging the input Substitutions' tags via tagsMerger.