Type Members

1.  class ComposeSubsts extends Substitution

   Function composition for two substitutions

2.  class ConstantSubst extends SimpleSubstitution

   Replace a constant with an arbitrary term

3.  class IdentitySubst extends Substitution
4.  class PseudoConstantSubst extends PseudoDivSubstitution

   Replace a constant with an arbitrary term

5.  abstract class PseudoDivSubstitution extends Substitution

   Trait for substitutions that can also replace constants or variables with coefficient, like n * c.

   Trait for substitutions that can also replace constants or variables with coefficient, like n * c. This is done through pseudo-division if necessary (and possible)

6.  abstract class SimpleSubstitution extends Substitution

   A substitution that works by simple replacement of constants or variables with arbitrary terms

7.  abstract class Substitution extends (TerFor) => TerFor with Sorted[Substitution]

   A substitution is a mapping from TerFor to TerFor that replaces variables and constants with arbitrary other terms.

   A substitution is a mapping from TerFor to TerFor that replaces variables and constants with arbitrary other terms. It is required that a substitution is only applied to terms/formulas that are sorted according to order. There are two more concrete sub-traits: SimpleSubstitution, which performs a simple replacement of constants or variables, and PseudoDivSubstitution, which can make use of pseudo-division in order to replace expressions n * c.

8.  class VariableShiftSubst extends SimpleSubstitution

   Substitution for renaming variables.

   Substitution for renaming variables. The arguments of the substitution is a pair (List[Int], Int) that describes how each variable should be shifted: (List(0, 2, -1), 1) specifies that variable 0 stays the same, variable 1 is increased by 2 (renamed to 3), variable 2 is renamed to 1, and all other variables n are renamed to n+1.

9.  class VariableSubst extends SimpleSubstitution

   Substitute the variable starting from index offset with the terms in replacements.

   Substitute the variable starting from index offset with the terms in replacements. I.e., VariableTerm(offset) is going to be replaced with replacements(0), etc. All other variables above offset+replacements.size are shifted downwards by replacements.size