Some of the rules of the analysis require that some identifiers are to be substituted with arithmetic expressions inside logic formulas
(an example is the rule for the assignment command).
Two cases arise:
If the arithmetic expression is composed of just the reading of an identifier, this can be freely substituted wherever it occurs.
If the arithmetic expression is more complex, this is put in equality with a fresh identifier, adding a clause in conjunction, and this fresh identifier is instead used for substitution.
Some of the rules of the analysis require that some identifiers are to be substituted with arithmetic expressions inside logic formulas (an example is the rule for the assignment command).
Two cases arise: