# substitutions

Visibility
1. Public
2. All

### Type Members

1. #### class ComposeSubsts extends Substitution

Function composition for two substitutions

2. #### class ConstantSubst extends SimpleSubstitution

Replace a constant with an arbitrary term

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`.

9. #### 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.

10. #### 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`