is the primary mechanism for computation and for proof in algebraic systems.
In general, Wolfram’s *Mathematica* program demonstrates that practically all calculation, computation and symbolic demonstration can be achieved with Pattern Matching and *substitution* over strings of symbols.
~
**But,**
No need to appeal to Mathematica. Term Rewriting, the foundation of Mathematica, is Turing-complete. (Konrad Hinsen via matrix 
)
~
Furthermore, when a mathematical system can be encoded in symbolic form, computation and demonstration in that system can be fully automated.
Substitution has always been difficult to show in mathematical notation because the form being substituted into changes when the substitution is enacted. Below, double-struck tortoise shell brackets are used as a compromise notation for the substitute operation.
〘A C E〙 ☞ substitute A for C in E
Substitution is a ternary operation, involving three patterns that we have differentiated by their sequential position in the shell-bracket notation.
~
William Bricken Ph.D, Iconic Arithmetic Volume I: The Design of Mathematics for Human Understanding (Unary press, 2019), p. 47–48.
〘PUT FOR INTO〙 ☞ substitute PUT for FOR in INTO
- The INTO-form is the structure that is being changed by the substitution. - The PUT-form is the structure that is being substituted into the INTO-form, in the process changing the structure of the INTO-form. - The FOR-form is the sub-structure within the INTO-form being replaced by the PUT-form.
Implicit within the substitution operation is an ability to locate or match the FOR structure within the INTO structure. This mechanism is far from trivial. The match might fail, in which case the substitution returns the INTO-form unchanged. The match might succeed more than once within the same INTO-form. This then requires several delicate implementation decisions that are considered in Volume II. In particular, it is critical whether substitution is partial (only some matches are changed) or total (all matches must be changed). When substitutions are nested or sequenced, additional implementation decisions are needed to decide how they might interact. At times during the course of a computation, for example, it is desirable to delay implementation of some substitutions until specific conditions are met.
The form of substitution〘A C E〙is, like the √ symbol, an instruction rather than a result. With pattern-substitution, axioms depict a **before-and-after** picture.
before E = 〔X Y Z〕
during E ⇒ 〘Q Z E〙
after E = 〔X Y Q〕
An equal sign is usually bidirectional, it doesn’t matter which side of the equation we consider as before. In contrast, substitution shows us a specified before, the INTO form E. The result is the entire expression〘A C E〙. To maintain consistency, all C in E must be replaced by A. Substitution must be total, considering all content forms as well as their contents.
Substitution includes several structural identities that define its behavior in any algebra. […]