validating equivalent and transformed expressions

To check whether a step was implemented correctly, the question is, "given the input expressions (and feeds), do the output expressions conform to the transform prescribed by the inference rule?"

For example, suppose we start with "A=B" and operate on this with the inference rule "add X to both sides," where X=2. If the output is "A+2 = B+2," was the step implemented correctly?

The inference rule can be described by an abstract syntax tree (AST):

    =                      =
  /   \        -->      /     \
LHS   RHS              +        +
                     /   \    /   \ 
                   LHS   x   RHS   x


https://blog.plover.com/math/24-puzzle-2.html
https://news.ycombinator.com/item?id=15075110