I have an assignment, $b, e, n := b+8, e+7, n+1$.
I also have two invariants of this assignment.
$E: b - 8 * n$
$F: e - 7 * n$
As per the title of the post, any combination of these invariants will produce another invariant. But I don't know how to combine them. I've never come across the $\oplus$ symbol, and from what I've been able to find it relates to the Cartesian product, which wouldn't really work here.
How can I combine two expressions to produce a new invariant?
The text book offers one combination as an example, but I can't see how they got there:
$$7 * (b - 8n) - 8 * (e - 7n)$$
This simplifies to
$$7 * b - 8 * e$$
I could get to the above expression just by making either original expression equal to 0, rearranging to get n in terms of b or e, and then substituting for n into one of the original expressions. But that seems like the wrong method to me, and I still don't know how the author got to the intermediate result.
Define the transformation $$ (b,e,n)\mapsto (b',e',n') \qquad\;\;\;\;\; $$ by $$ \begin{cases} b'=b+8 \qquad\qquad\qquad\;\;\;\;\;\; \\[4pt] e'=e+7\\[4pt] n'=n+1\\[4pt] \end{cases} $$ To say that $E=b-8n$ is an invariant means that, identically $$ b'-8n' = b-8n \qquad\qquad\;\;\;\;\, $$ which is verified by \begin{align*} b'-8n' &= (b+8)-8(n+1)\\[4pt] &= b + 8 - 8n - 8\\[4pt] &= b - 8n\\[4pt] \end{align*} Similarly, to say that $F=e-7n$ is an invariant means that, identically $$ e'-7n' = e-7n \qquad\qquad\;\;\;\;\, $$ which is verified by \begin{align*} e'-7n' &= (e+7)-7(n+1)\\[4pt] &= e + 7 - 7n - 7\\[4pt] &= e - 7n\\[4pt] \end{align*} Any function of one or more invariants is an invariant.
In particular, invariants can be added, subtracted, multiplied and divided (provided the denominator is nonzero), and the result will be an invariant.
Constants are automatically invariant, so any constant multiple of an invariant is an invariant.
More generally, any linear combinations of invariants is an invariant.
Returning to the earlier example, since $b - 8n$ and $e-7n$ are invariants, any linear combination of $b-8n$ and $e-7n$ is an invariant. In particular, $7(b-8n)-8(e-7n)$ is invariant, which yields the invariant $7b-8e$.
As regards the notation $E\oplus F$, the symbol $\oplus$ is just a placeholder for an arbitrary binary operation, whose inputs are two states of the system, and whose output is a state of the system. Recall that a binary operation on a set $S$ is just a function from $S{\times}S$ to $S$ In this context, $S$ will the set of possible states of the system being analyzed. Hence since a function of one or more invariants is an invariant, it's automatic that if $E,F$ are invariants, so is $E\oplus F$.