There is a complication with negative integer literals; they are not implemented.
Although in theory (i.e., the theory in terms of which the semantics of the system is defined) each integer is represented as an atomic literal, we did not in fact implement negative literals. This complicates the rules for calculating with negative valued results somewhat.
The theoretical explanation of how to execute, e.g.,
Execute the expressions
If the results are (atomic) integer literals, then return the integer literal corresponding to the sum.
The actual method of computation employed in proofs employs the non-canonical