<output_expression> = add_x_to_both_sides( <feed value>, <input_expression> )
Applying the inference rule "add 2 to both sides of the expression" yields
The "add __ to both sides of the expression" inference rule essentially means transform input
LHS = RHS
to
LHS + __ = RHS + __
or, in terms of transforming an abstract syntax tree,
Claim: every inference rule can be written as a transform from one abstract syntax tree to another.